Commit 64843c5f authored by Rodolphe Lepigre's avatar Rodolphe Lepigre

Fix after Cerberus API change.

parent ea5c3527
......@@ -584,6 +584,8 @@ let rec translate_expr : bool -> op_type option -> ail_expr -> expr * calls =
| _ ->
not_impl loc "expr function_decay (not an ident)"
in res
| AilEgcc_statement ->
not_impl loc "expr gcc_statement (partial Cerberus support)"
in
match (goal_ty, res_ty) with
| (None , _ )
......@@ -857,12 +859,12 @@ let warn_ignored_attrs so attrs =
| AilSskip -> "a skip"
| AilSexpr(_) -> "an expression"
| AilSif(_,_,_) -> "an if statement"
| AilSwhile(_,_) -> "a while loop"
| AilSdo(_,_) -> "a do-while loop"
| AilSwhile(_,_,_) -> "a while loop"
| AilSdo(_,_,_) -> "a do-while loop"
| AilSswitch(_,_) -> "a switch statement"
| AilScase(_,_) -> "a case statement"
| AilSdefault(_) -> "a default statement"
| AilSlabel(_,_) -> "a label"
| AilSlabel(_,_,_) -> "a label"
| AilSdeclaration(_) -> "a declaration"
| AilSpar(_) -> "a par statement"
| AilSreg_store(_,_) -> "a register store statement"
......@@ -1071,7 +1073,7 @@ let translate_block stmts blocks ret_ty =
(blocks, mkloc (Goto(id_else)) s.loc)
in
translate_bool_expr then_goto else_goto blocks e
| AilSwhile(e,s) ->
| AilSwhile(e,s,_) ->
let attrs = extra_attrs @ attrs in
let id_cond = fresh_block_id () in
let id_body = fresh_block_id () in
......@@ -1104,7 +1106,7 @@ let translate_block stmts blocks ret_ty =
add_block ~annots id_cond s blocks
in
(locate (Goto(id_cond)), blocks)
| AilSdo(s,e) ->
| AilSdo(s,e,_) ->
let attrs = extra_attrs @ attrs in
let id_cond = fresh_block_id () in
let id_body = fresh_block_id () in
......@@ -1241,7 +1243,7 @@ let translate_block stmts blocks ret_ty =
(* Update the default ref. *)
default_ref := Some(default_s);
(default_s, blocks)
| AilSlabel(l,s) ->
| AilSlabel(l,s,_) ->
let (s, blocks) = trans extra_attrs swstk ks (s :: stmts) blocks in
let blocks = add_block (sym_to_str l) s blocks in
(locate (Goto(sym_to_str l)), blocks)
......
open Cerb_frontend
open Cerb_backend
open Global_ocaml
open Pipeline
type cpp_config =
......@@ -33,7 +34,7 @@ let frontend cpp_cmd filename =
; typecheck_core = false ; rewrite_core = false
; sequentialise_core = false ; cpp_cmd ; cpp_stderr = true }
in
Global_ocaml.(set_cerb_conf false Random false Basic false false false);
set_cerb_conf false Random false Basic false true false false;
Ocaml_implementation.(set (HafniumImpl.impl));
load_core_stdlib () >>= fun stdlib ->
load_core_impl stdlib impl_name >>= fun impl ->
......@@ -45,7 +46,7 @@ let run_cpp cpp_cmd filename =
; typecheck_core = false ; rewrite_core = false
; sequentialise_core = false ; cpp_cmd ; cpp_stderr = true }
in
Global_ocaml.(set_cerb_conf false Random false Basic false false false);
set_cerb_conf false Random false Basic false true false false;
cpp (conf, io) ~filename
let cpp_cmd config =
......
......@@ -276,6 +276,8 @@ let points_to classify expr =
[]
| AilEunion (_, _, e_opt) ->
[]
| AilEgcc_statement ->
[]
in
aux expr
......@@ -411,6 +413,8 @@ let rec taint_expr points_to (AnnotatedExpression (_, _, loc, expr_)) =
merge_pointsto (List.map (function (_, Some e) -> self e | (_, None) -> []) xs)
| AilEva_copy (e1, e2) ->
merge_pointsto [self e1; self e2]
| AilEgcc_statement ->
[]
let taints_of_functions sigm =
......@@ -454,13 +458,13 @@ let taints_of_functions sigm =
merge_pointsto (List.map (fold_stmt env') ss)
| AilSif (e, s1, s2) ->
merge_pointsto [taint_expr e; fold_stmt env s1; fold_stmt env s2]
| AilSwhile (e, s)
| AilSdo (s, e)
| AilSwhile (e, s, _)
| AilSdo (s, e, _)
| AilSswitch (e, s) ->
merge_pointsto [taint_expr e; fold_stmt env s]
| AilScase (_, s)
| AilSdefault s
| AilSlabel (_, s) ->
| AilSlabel (_, s, _) ->
fold_stmt env s
| AilSdeclaration xs ->
merge_pointsto (List.map (fun (_, e) -> taint_expr e) xs)
......@@ -526,6 +530,7 @@ let warn_unseq taints_map expr =
| AilEsizeof _
| AilEalignof _
| AilEreg_load _
| AilEgcc_statement
| AilEunion (_, _, None) ->
NO_CALL
......@@ -608,6 +613,7 @@ let warn_file (_, sigm) =
| AilEident _
| AilEsizeof _
| AilEalignof _
| AilEgcc_statement
| AilEreg_load _ ->
()
......@@ -736,11 +742,11 @@ let warn_file (_, sigm) =
warn_unseq e;
self s1;
self s2
| AilSwhile (e, s) ->
| AilSwhile (e, s, _) ->
self s;
aux_expr env e;
warn_unseq e
| AilSdo (s, e) ->
| AilSdo (s, e, _) ->
aux_expr env e;
warn_unseq e;
self s
......@@ -754,7 +760,7 @@ let warn_file (_, sigm) =
self s
| AilScase (_, s)
| AilSdefault s
| AilSlabel (_, s) ->
| AilSlabel (_, s, _) ->
self s
| AilSgoto _ ->
()
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment