diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
index fe974d215cdb73c995e57566dcef15d5b076da11..671ea306b1f641e8cacba62184345c3256d526fd 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
@@ -260,7 +260,7 @@ let to_exp ~loc kf env pot label =
let e_size, _ = term_to_exp kf env t_size in
let e_size = Cil.constFold false e_size in
let malloc_stmt =
- Constructor.mk_lib_call ~loc
+ Smart_stmt.lib_call ~loc
~result:(Cil.var vi)
"malloc"
[ e_size ]
@@ -273,7 +273,7 @@ let to_exp ~loc kf env pot label =
| Typing.(Rational | Real | Nan) ->
Error.not_yet "quantification over non-integer type"
in
- let free_stmt = Constructor.mk_lib_call ~loc "free" [e] in
+ let free_stmt = Smart_stmt.lib_call ~loc "free" [e] in
(* The list of stmts returned by the current closure are inserted
LOCALLY to the block where the new var is FIRST used, whatever scope
is indicated to [Env.new_var].
@@ -296,14 +296,14 @@ let to_exp ~loc kf env pot label =
let e, env = named_predicate_to_exp kf env p in
let e = Cil.constFold false e in
let storing_stmt =
- Constructor.mk_assigns ~loc ~result:lval e
+ Smart_stmt.assigns ~loc ~result:lval e
in
let block, env =
Env.pop_and_get env storing_stmt ~global_clear:false Env.After
in
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
- [ Constructor.mk_block_stmt block ], env
+ [ Smart_stmt.block_stmt block ], env
| Lscope.PoT_term t ->
begin match Typing.get_number_ty t with
| Typing.(C_integer _ | C_float _ | Nan) ->
@@ -312,14 +312,14 @@ let to_exp ~loc kf env pot label =
let e, env = term_to_exp kf env t in
let e = Cil.constFold false e in
let storing_stmt =
- Constructor.mk_assigns ~loc ~result:lval e
+ Smart_stmt.assigns ~loc ~result:lval e
in
let block, env =
Env.pop_and_get env storing_stmt ~global_clear:false Env.After
in
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
- [ Constructor.mk_block_stmt block ], env
+ [ Smart_stmt.block_stmt block ], env
| Typing.(Rational | Real) ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
@@ -335,7 +335,7 @@ let to_exp ~loc kf env pot label =
let storing_loops_block = Cil.mkBlock storing_loops_stmts in
let storing_loops_block, env = Env.pop_and_get
env
- (Constructor.mk_block_stmt storing_loops_block)
+ (Smart_stmt.block_stmt storing_loops_block)
~global_clear:false
Env.After
in
@@ -343,7 +343,7 @@ let to_exp ~loc kf env pot label =
let env = put_block_at_label env kf storing_loops_block label in
(* Returning *)
let lval_at_index, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
- let e = Constructor.mk_lval ~loc lval_at_index in
+ let e = Smart_exp.lval ~loc lval_at_index in
e, env
(*
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index e457ac5c2264548399b60b7ed77206f49cd6973e..cfdbe5fdda47bb9b3ea0aab39423b7e26bf8c5c6 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -56,7 +56,7 @@ type local_env = {
type t = {
lscope: Lscope.t;
lscope_reset: bool;
- annotation_kind: Constructor.annotation_kind;
+ annotation_kind: Smart_stmt.annotation_kind;
new_global_vars: (varinfo * localized_scope) list;
(* generated variables. The scope indicates the level where the variable
should be added. *)
@@ -88,7 +88,7 @@ let empty_local_env =
let empty =
{ lscope = Lscope.empty;
lscope_reset = true;
- annotation_kind = Constructor.Assertion;
+ annotation_kind = Smart_stmt.Assertion;
new_global_vars = [];
global_mp_tbl = empty_mp_tbl;
env_stack = [];
@@ -257,7 +257,7 @@ let rtl_call_to_new_var ~loc ?scope ?name env kf t ty func_name args =
t
ty
(fun v _ ->
- [ Constructor.mk_rtl_call ~loc ~result:(Cil.var v) func_name args ])
+ [ Smart_stmt.rtl_call ~loc ~result:(Cil.var v) func_name args ])
in
exp, env
@@ -351,9 +351,9 @@ let add_stmt ?(post=false) ?before env kf stmt =
{ env with env_stack = local_env :: tl }
let extend_stmt_in_place env stmt ~label block =
- let new_stmt = Constructor.mk_block_stmt block in
+ let new_stmt = Smart_stmt.block_stmt block in
let sk = stmt.skind in
- stmt.skind <- Block (Cil.mkBlock [ new_stmt; Constructor.mk_stmt sk ]);
+ stmt.skind <- Block (Cil.mkBlock [ new_stmt; Smart_stmt.stmt sk ]);
let pre = match label with
| BuiltinLabel(Here | Post) -> true
| BuiltinLabel(Old | Pre | LoopEntry | LoopCurrent | Init)
@@ -447,7 +447,7 @@ let pop_and_get ?(split=false) env stmt ~global_clear where =
add the given [stmt] afterwards. This way, we have the guarantee that
the final block does not contain any local, so may be transient. *)
if split then
- let sblock = Constructor.mk_block_stmt b in
+ let sblock = Smart_stmt.block_stmt b in
Cil.transient_block (Cil.mkBlock [ sblock; stmt ])
else
b
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 847b551cacb7222e4efdf9f1448012bcc655496a..94c11335f1c96bbcee2a1def0150be956bb81435 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -148,8 +148,8 @@ end
(** {2 Current annotation kind} *)
(* ************************************************************************** *)
-val annotation_kind: t -> Constructor.annotation_kind
-val set_annotation_kind: t -> Constructor.annotation_kind -> t
+val annotation_kind: t -> Smart_stmt.annotation_kind
+val set_annotation_kind: t -> Smart_stmt.annotation_kind -> t
(* ************************************************************************** *)
(** {2 Loop invariants} *)
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.ml b/src/plugins/e-acsl/src/code_generator/global_observer.ml
index ab1d0ed88db4408e4dd14635e8291350f6666ba8..0e6a3ac2302a17cae489c61671fb46e4f7946ecc 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.ml
@@ -123,8 +123,8 @@ let mk_init_function () =
if Misc.is_fc_or_compiler_builtin vi then stmts
else
(* a global is both allocated and initialized *)
- Constructor.mk_store_stmt vi
- :: Constructor.mk_initialize ~loc:Location.unknown (Cil.var vi)
+ Smart_stmt.store_stmt vi
+ :: Smart_stmt.initialize ~loc:Location.unknown (Cil.var vi)
:: stmts)
tbl
stmts
@@ -136,10 +136,10 @@ let mk_init_function () =
let loc = Location.unknown in
let e = Cil.new_exp ~loc:loc (Const (CStr s)) in
let str_size = Cil.new_exp loc (SizeOfStr s) in
- Constructor.mk_assigns ~loc ~result:(Cil.var vi) e
- :: Constructor.mk_store_stmt ~str_size vi
- :: Constructor.mk_full_init_stmt vi
- :: Constructor.mk_mark_readonly vi
+ Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
+ :: Smart_stmt.store_stmt ~str_size vi
+ :: Smart_stmt.full_init_stmt vi
+ :: Smart_stmt.mark_readonly vi
:: stmts)
stmts
in
@@ -150,7 +150,7 @@ let mk_init_function () =
let b, _env = Env.pop_and_get env stmt ~global_clear:true Env.Before in
b, stmts
in
- let stmts = Constructor.mk_block_stmt b :: stmts in
+ let stmts = Smart_stmt.block_stmt b :: stmts in
(* prevent multiple calls to [__e_acsl_globals_init] *)
let loc = Location.unknown in
let vi_already_run =
@@ -168,14 +168,14 @@ let mk_init_function () =
(Local_init (vi_already_run, init, loc))
in
let already_run =
- Constructor.mk_assigns
+ Smart_stmt.assigns
~loc
~result:(Cil.var vi_already_run)
(Cil.one ~loc)
in
let stmts = already_run :: stmts in
let guard =
- Constructor.mk_if
+ Smart_stmt.if_stmt
~loc
~cond:(Cil.evar vi_already_run)
(Cil.mkBlock [])
@@ -195,7 +195,7 @@ let mk_delete_function () =
Varinfo.Hashtbl.fold_sorted
(fun vi _l acc ->
if Misc.is_fc_or_compiler_builtin vi then acc
- else Constructor.mk_delete_stmt vi :: acc)
+ else Smart_stmt.delete_stmt vi :: acc)
tbl
[]
in
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index 8c28ac5e32e0267754723bd1a0042f492fb6cb17..8a2b5385f1cb1830a92ff5272cb14bd0cd3d7c69 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -33,7 +33,7 @@ let apply_on_var ~loc funname e =
else if Gmp_types.Q.is_t ty then "__gmpq_"
else assert false
in
- Constructor.mk_lib_call ~loc (prefix ^ funname) [ e ]
+ Smart_stmt.lib_call ~loc (prefix ^ funname) [ e ]
let init ~loc e = apply_on_var "init" ~loc e
let clear ~loc e = apply_on_var "clear" ~loc e
@@ -90,9 +90,9 @@ let generic_affect ~loc fname lv ev e =
let ty = Cil.typeOf ev in
if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then begin
let suf, args = get_set_suffix_and_arg ty e in
- Constructor.mk_lib_call ~loc (fname ^ suf) (ev :: args)
+ Smart_stmt.lib_call ~loc (fname ^ suf) (ev :: args)
end else
- Constructor.mk_assigns ~loc:e.eloc ~result:lv e
+ Smart_stmt.assigns ~loc:e.eloc ~result:lv e
let init_set ~loc lv ev e =
let fname =
@@ -111,7 +111,7 @@ let init_set ~loc lv ev e =
| Lval elv ->
assert (Gmp_types.Z.is_t (Cil.typeOf ev));
let call =
- Constructor.mk_lib_call ~loc
+ Smart_stmt.lib_call ~loc
"__gmpz_import"
[ ev;
Cil.one ~loc;
@@ -121,7 +121,7 @@ let init_set ~loc lv ev e =
Cil.zero ~loc;
Cil.mkAddrOf ~loc elv ]
in
- Constructor.mk_block_stmt (Cil.mkBlock [ init ~loc ev; call ])
+ Smart_stmt.block_stmt (Cil.mkBlock [ init ~loc ev; call ])
| _ ->
Error.not_yet "unsigned long long expression requiring GMP")
| Longlong ILongLong ->
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index dd1222051d790f8757da083c9f9628ac3be4d877..cdc6486702d1fbcc234a0f0f7bf19b1f616e74c9 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -60,7 +60,7 @@ let inject_in_local_init loc env kf vi = function
| ConsInit (fvi, sz :: _, _) as init
when Functions.Libc.is_vla_alloc_name fvi.vname ->
(* add a store statement when creating a variable length array *)
- let store = Constructor.mk_store_stmt ~str_size:sz vi in
+ let store = Smart_stmt.store_stmt ~str_size:sz vi in
let env = Env.add_stmt ~post:true env kf store in
init, env
@@ -145,13 +145,13 @@ let add_initializer loc ?vi lv ?(post=false) stmt env kf =
(* bitfields are not yet supported ==> no initializer.
a [not_yet] will be raised in [Translate]. *)
if Cil.isBitfield lv then Cil.mkEmptyStmt ()
- else Constructor.mk_initialize ~loc lv
+ else Smart_stmt.initialize ~loc lv
in
let env = Env.add_stmt ~post ~before env kf new_stmt in
let env = match vi with
| None -> env
| Some vi ->
- let new_stmt = Constructor.mk_store_stmt vi in
+ let new_stmt = Smart_stmt.store_stmt vi in
Env.add_stmt ~post ~before env kf new_stmt
in
env
@@ -189,7 +189,7 @@ let inject_in_instr env kf stmt = function
if Functions.Libc.is_vla_free caller then
match args with
| [ { enode = CastE (_, { enode = Lval (Var vi, NoOffset) }) } ] ->
- let delete_block = Constructor.mk_delete_stmt ~is_addr:true vi in
+ let delete_block = Smart_stmt.delete_stmt ~is_addr:true vi in
Env.add_stmt env kf delete_block
| _ -> Options.fatal "The normalization of __fc_vla_free() has changed"
else
@@ -263,7 +263,7 @@ let add_new_block_in_stmt env kf stmt =
let b, env =
Env.pop_and_get env new_stmt ~global_clear:true Env.After
in
- let new_stmt = Constructor.mk_block stmt b in
+ let new_stmt = Smart_stmt.block stmt b in
if not (Cil_datatype.Stmt.equal stmt new_stmt) then begin
(* move the labels of the return to the new block in order to
evaluate the postcondition when jumping to them. *)
@@ -293,7 +293,7 @@ let add_new_block_in_stmt env kf stmt =
let post_block, env =
Env.pop_and_get
env
- (Constructor.mk_block new_stmt pre_block)
+ (Smart_stmt.block new_stmt pre_block)
~global_clear:false
Env.Before
in
@@ -302,7 +302,7 @@ let add_new_block_in_stmt env kf stmt =
then Cil.transient_block post_block
else post_block
in
- let res = Constructor.mk_block new_stmt post_block in
+ let res = Smart_stmt.block new_stmt post_block in
if not (Cil_datatype.Stmt.equal new_stmt res) then
E_acsl_label.move kf new_stmt res;
res, env
@@ -337,7 +337,7 @@ let insert_as_last_stmts_in_innermost_block ~last_stmts kf outer_block =
match return_stmt with
| Some return_stmt ->
let b = Cil.mkBlock new_stmts in
- let new_stmt = Constructor.mk_block return_stmt b in
+ let new_stmt = Smart_stmt.block return_stmt b in
E_acsl_label.move kf return_stmt new_stmt;
[ new_stmt ]
| None -> new_stmts
@@ -516,7 +516,7 @@ and inject_in_block (env: Env.t) kf blk =
List.fold_left
(fun acc vi ->
if Mmodel_analysis.must_model_vi ~kf vi
- then Constructor.mk_delete_stmt vi :: acc
+ then Smart_stmt.delete_stmt vi :: acc
else acc)
stmts
blk.blocals
@@ -531,7 +531,7 @@ and inject_in_block (env: Env.t) kf blk =
List.fold_left
(fun acc vi ->
if Mmodel_analysis.must_model_vi vi && not vi.vdefined
- then Constructor.mk_store_stmt vi :: acc
+ then Smart_stmt.store_stmt vi :: acc
else acc)
blk.bstmts
blk.blocals;
@@ -821,8 +821,8 @@ let inject_mmodel_handler main =
in
let ptr_size = Cil.sizeOf loc Cil.voidPtrType in
let args = args @ [ ptr_size ] in
- let init = Constructor.mk_rtl_call loc "memory_init" args in
- let clean = Constructor.mk_rtl_call loc "memory_clean" [] in
+ let init = Smart_stmt.rtl_call loc "memory_init" args in
+ let clean = Smart_stmt.rtl_call loc "memory_clean" [] in
surround_function_with main fundec init (Some clean)
in
Extlib.may handle_main main
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml
index af522479dc6c22f7926c9edfee20c28821c1ce1a..08e9eda66c45e2f5e0967f4cd49c3a9340a85703 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_array.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml
@@ -95,7 +95,7 @@ let length_exp ~loc kf env ~name array =
~name
Cil.theMachine.typeOfSizeOf
(fun v _ -> [
- Constructor.mk_assigns
+ Smart_stmt.assigns
~loc
~result:(Cil.var v)
(Cil.mkBinOp
@@ -168,7 +168,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
None
~name
Cil.intType
- (fun v _ -> [ Constructor.mk_assigns ~loc ~result:(Cil.var v) (res_value ()) ])
+ (fun v _ -> [ Smart_stmt.assigns ~loc ~result:(Cil.var v) (res_value ()) ])
in
(* Retrieve the length of the arrays *)
@@ -193,8 +193,8 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
arrays. This env will enable us to also check RTEs *)
let env = Env.push env in
(* Create the access to the arrays *)
- let array1_iter_e = Constructor.mk_subscript ~loc array1 iter_e in
- let array2_iter_e = Constructor.mk_subscript ~loc array2 iter_e in
+ let array1_iter_e = Smart_exp.subscript ~loc array1 iter_e in
+ let array2_iter_e = Smart_exp.subscript ~loc array2 iter_e in
(* Check RTE on the arrays, filtering out bounding checks since the accesses
are built already in bounds *)
let filter a =
@@ -212,12 +212,12 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
let cond = Cil.mkBinOp ~loc Ne array1_iter_e array2_iter_e in
(* Create the statement representing the body of the for loop *)
let body =
- Constructor.mk_if
+ Smart_stmt.if_stmt
~loc
~cond
(Cil.mkBlock [
- Constructor.mk_assigns ~loc ~result:(Cil.var comparison_vi) (res_value ~flip:true ());
- Constructor.mk_break ~loc
+ Smart_stmt.assigns ~loc ~result:(Cil.var comparison_vi) (res_value ~flip:true ());
+ Smart_stmt.break ~loc
])
in
(* Pop the env to build the body of the for loop *)
@@ -225,14 +225,14 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
(* Create the statement representing the full for loop *)
let for_loop =
- (Constructor.mk_block_stmt
+ (Smart_stmt.block_stmt
(Cil.mkBlock
(Cil.mkForIncr
~iter
~first:(Cil.zero ~loc)
~stopat:len1_exp
~incr:(Cil.one ~loc)
- ~body:[ Constructor.mk_block_stmt body_blk ]
+ ~body:[ Smart_stmt.block_stmt body_blk ]
)
)
)
@@ -244,7 +244,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
(* Add the check for the length before the for loop *)
let prepend_coercion_check ~name env stmts array len =
- let array_orig = Option.get (Constructor.extract_uncoerced_lval array) in
+ let array_orig = Option.get (Misc.extract_uncoerced_lval array) in
if array_orig == array then
stmts, env
else
@@ -259,7 +259,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
in
let p = { p with pred_name = "array_coercion" :: p.pred_name } in
let stmt =
- Constructor.mk_runtime_check Constructor.RTE kf e p
+ Smart_stmt.runtime_check Smart_stmt.RTE kf e p
in
stmt :: stmts, env
in
@@ -272,17 +272,17 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
(* Pop the env to build the full then block *)
let then_blk, env =
- pop_and_get_env env (Constructor.mk_block_stmt (Cil.mkBlock then_stmts))
+ pop_and_get_env env (Smart_stmt.block_stmt (Cil.mkBlock then_stmts))
in
(* Create the statement representing the whole generated code *)
let stmt =
- Constructor.mk_if
+ Smart_stmt.if_stmt
~loc
~cond:(Cil.mkBinOp ~loc Eq len1_exp len2_exp)
then_blk
~else_blk:(Cil.mkBlock
- [ Constructor.mk_assigns
+ [ Smart_stmt.assigns
~loc
~result:(Cil.var comparison_vi)
(res_value ~flip:true ()) ])
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index d5bf1c4da99b052ef55ba976adb9eba5c4929ff7..97c6523575a25720e3316e1fd0a532bf7331894a 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -98,7 +98,7 @@ let term_to_block ~loc kf env ret_ty ret_vi t =
function (by reference). *)
let set =
let lv_star_ret = Cil.mkMem ~addr:(Cil.evar ~loc ret_vi) ~off:NoOffset in
- let star_ret = Constructor.mk_lval ~loc lv_star_ret in
+ let star_ret = Smart_exp.lval ~loc lv_star_ret in
Gmp.init_set ~loc lv_star_ret star_ret e
in
let return_void = Cil.mkStmt ~valid_sid:true (Return (None, loc)) in
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index bca60ec4f2cd8197f440f38a15241dd03c70761e..c8a5f714ddc2b23fab8a20edded2bd7ea2b6d663 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -59,11 +59,11 @@ let preserve_invariant env kf stmt = match stmt.skind with
let blk, env =
Env.pop_and_get env last ~global_clear:false Env.Before
in
- Constructor.mk_block last blk :: stmts, env
+ Smart_stmt.block last blk :: stmts, env
| s :: tl ->
handle_invariants (s :: stmts, env) tl
in
- let env = Env.set_annotation_kind env Constructor.Invariant in
+ let env = Env.set_annotation_kind env Smart_stmt.Invariant in
let stmts, env = handle_invariants ([], env) stmts in
let new_blk = { blk with bstmts = List.rev stmts } in
{ stmt with skind = Loop([], new_blk, loc, cont, break) },
@@ -212,7 +212,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
Env.Middle
in
(* generate the guard [x bop t2] *)
- let block_to_stmt b = Constructor.mk_block_stmt b in
+ let block_to_stmt b = Smart_stmt.block_stmt b in
let tlv = Logic_const.tvar ~loc logic_x in
let guard =
(* must copy [t2] to force being typed again *)
@@ -221,10 +221,10 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
in
Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
let guard_exp, env = term_to_exp kf (Env.push env) guard in
- let break_stmt = Constructor.mk_break ~loc:guard_exp.eloc in
+ let break_stmt = Smart_stmt.break ~loc:guard_exp.eloc in
let guard_blk, env = Env.pop_and_get
env
- (Constructor.mk_if
+ (Smart_stmt.if_stmt
~loc:guard_exp.eloc
~cond:guard_exp
(mkBlock [ mkEmptyStmt ~loc () ])
@@ -251,10 +251,10 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
| Some p ->
let e, env = !named_predicate_ref kf (Env.push env) p in
let stmt, env =
- Constructor.mk_runtime_check Constructor.RTE kf e p, env
+ Smart_stmt.runtime_check Smart_stmt.RTE kf e p, env
in
let b, env = Env.pop_and_get env stmt ~global_clear:false Env.After in
- let guard_for_small_type = Constructor.mk_block_stmt b in
+ let guard_for_small_type = Smart_stmt.block_stmt b in
guard_for_small_type :: guard :: body @ [ next ], env
in
let start = block_to_stmt init_blk in
diff --git a/src/plugins/e-acsl/src/code_generator/memory_observer.ml b/src/plugins/e-acsl/src/code_generator/memory_observer.ml
index 0ec5cda04ef5f39be1210766ebaca866b748dd37..629e30432278b7a6912f33453939a7476c31632e 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_observer.ml
@@ -39,7 +39,7 @@ let store ?before env kf vars =
tracking_stmt
?before
List.fold_right (* small list *)
- Constructor.mk_store_stmt
+ Smart_stmt.store_stmt
env
kf
vars
@@ -48,7 +48,7 @@ let duplicate_store ?before env kf vars =
tracking_stmt
?before
Varinfo.Set.fold
- Constructor.mk_duplicate_store_stmt
+ Smart_stmt.duplicate_store_stmt
env
kf
vars
@@ -57,7 +57,7 @@ let delete_from_list ?before env kf vars =
tracking_stmt
?before
List.fold_right (* small list *)
- Constructor.mk_delete_stmt
+ Smart_stmt.delete_stmt
env
kf
vars
@@ -66,7 +66,7 @@ let delete_from_set ?before env kf vars =
tracking_stmt
?before
Varinfo.Set.fold
- Constructor.mk_delete_stmt
+ Smart_stmt.delete_stmt
env
kf
vars
diff --git a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
index f5cae16eb0bdb82fc8330038a5c218c6c79f50f7..654433624a3147fc868f052b6d16ab13c9adfaa1 100644
--- a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
@@ -155,8 +155,8 @@ let gmp_to_sizet ~loc kf env size p =
None
sizet
(fun vi _ ->
- [ Constructor.mk_runtime_check Constructor.RTE kf guard p;
- Constructor.mk_lib_call ~loc
+ [ Smart_stmt.runtime_check Smart_stmt.RTE kf guard p;
+ Smart_stmt.lib_call ~loc
~result:(Cil.var vi)
"__gmpz_get_ui"
[ size ] ])
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index b6114f25cd132102a8ccd4e606ca1ad303c2047a..b32d939f05d87cf39e1b798480a59e53a44b6d52 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -174,7 +174,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
intType
(fun v _ ->
let lv = var v in
- [ Constructor.mk_assigns ~loc ~result:lv init_val ])
+ [ Smart_stmt.assigns ~loc ~result:lv init_val ])
in
let end_loop_ref = ref dummyStmt in
(* innermost block *)
@@ -188,23 +188,23 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
(* use a 'goto', not a simple 'break' in order to handle 'forall' with
multiple binders (leading to imbricated loops) *)
mkBlock
- [ Constructor.mk_assigns ~loc ~result:(var var_res) found_val;
+ [ Smart_stmt.assigns ~loc ~result:(var var_res) found_val;
mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ]
in
let blk, env = Env.pop_and_get
env
- (Constructor.mk_if ~loc ~cond:(mk_guard test) then_blk ~else_blk)
+ (Smart_stmt.if_stmt ~loc ~cond:(mk_guard test) then_blk ~else_blk)
~global_clear:false
Env.After
in
let blk = Cil.flatten_transient_sub_blocks blk in
- [ Constructor.mk_block_stmt blk ], env
+ [ Smart_stmt.block_stmt blk ], env
in
let stmts, env =
Loops.mk_nested_loops ~loc mk_innermost_block kf env lvs_guards
in
let env =
- Env.add_stmt env kf (Constructor.mk_block_stmt (mkBlock stmts))
+ Env.add_stmt env kf (Smart_stmt.block_stmt (mkBlock stmts))
in
(* where to jump to go out of the loop *)
let end_loop = mkEmptyStmt ~loc () in
diff --git a/src/plugins/e-acsl/src/code_generator/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
index 3a0da53951b3b4f569e7f55bc2ea3d4849e1fcc4..2f4417b0191213b6730879074147a5f66f68fe43 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -24,7 +24,7 @@ open Cil_types
(* No init_set for GMPQ: init then set separately *)
let init_set ~loc lval vi_e e =
- Constructor.mk_block_stmt
+ Smart_stmt.block_stmt
(Cil.mkBlock
[ Gmp.init ~loc vi_e ;
Gmp.affect ~loc lval vi_e e ])
@@ -148,7 +148,7 @@ let add_cast ~loc ?name e env kf ty =
None
Cil.doubleType
(fun v _ ->
- [ Constructor.mk_lib_call ~loc
+ [ Smart_stmt.lib_call ~loc
~result:(Cil.var v)
"__gmpq_get_d"
[ e ] ])
@@ -197,7 +197,7 @@ let cmp ~loc bop e1 e2 env kf t_opt =
~name
Cil.intType
(fun v _ ->
- [ Constructor.mk_lib_call ~loc ~result:(Cil.var v) fname [ e1; e2 ] ])
+ [ Smart_stmt.lib_call ~loc ~result:(Cil.var v) fname [ e1; e2 ] ])
in
Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
@@ -226,7 +226,7 @@ let binop ~loc bop e1 e2 env kf t_opt =
[e2] *)
let e1, env = create ~loc e1 env kf None in
let e2, env = create ~loc e2 env kf None in
- let mk_stmts _ e = [ Constructor.mk_lib_call ~loc name [ e; e1; e2 ] ] in
+ let mk_stmts _ e = [ Smart_stmt.lib_call ~loc name [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
let _, e, env = new_var_and_init ~loc ~name env kf t_opt mk_stmts in
e, env
diff --git a/src/plugins/e-acsl/src/code_generator/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml
index e57b894f4283dbb6519a963a929d53bc37672180..96f5c22ee29764fd99bded8ea64abf265fabb0d0 100644
--- a/src/plugins/e-acsl/src/code_generator/temporal.ml
+++ b/src/plugins/e-acsl/src/code_generator/temporal.ml
@@ -81,7 +81,7 @@ end = struct
| Copy -> Options.fatal "Copy flow type in store_reference"
in
let fname = RTL.mk_temporal_name fname in
- Constructor.mk_lib_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs ]
+ Smart_stmt.lib_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs ]
let save_param ~loc flow lhs pos =
let infix = match flow with
@@ -91,13 +91,13 @@ end = struct
in
let fname = "save_" ^ infix ^ "_parameter" in
let fname = RTL.mk_temporal_name fname in
- Constructor.mk_lib_call ~loc fname [ lhs ; Cil.integer ~loc pos ]
+ Smart_stmt.lib_call ~loc fname [ lhs ; Cil.integer ~loc pos ]
let pull_param ~loc vi pos =
let exp = Cil.mkAddrOfVi vi in
let fname = RTL.mk_temporal_name "pull_parameter" in
let sz = Cil.kinteger ~loc IULong (Cil.bytesSizeOf vi.vtype) in
- Constructor.mk_lib_call ~loc fname [ exp ; Cil.integer ~loc pos ; sz ]
+ Smart_stmt.lib_call ~loc fname [ exp ; Cil.integer ~loc pos ; sz ]
let handle_return_referent ~save ~loc lhs =
let fname = match save with
@@ -108,15 +108,15 @@ end = struct
(match (Cil.typeOf lhs) with
| TPtr _ -> ()
| _ -> Error.not_yet "Struct in return");
- Constructor.mk_lib_call ~loc (RTL.mk_temporal_name fname) [ lhs ]
+ Smart_stmt.lib_call ~loc (RTL.mk_temporal_name fname) [ lhs ]
let reset_return_referent ~loc =
- Constructor.mk_lib_call ~loc (RTL.mk_temporal_name "reset_return") []
+ Smart_stmt.lib_call ~loc (RTL.mk_temporal_name "reset_return") []
let temporal_memcpy_struct ~loc lhs rhs =
let fname = RTL.mk_temporal_name "memcpy" in
let size = Cil.sizeOf ~loc (Cil.typeOfLval lhs) in
- Constructor.mk_lib_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs; size ]
+ Smart_stmt.lib_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs; size ]
end
(* }}} *)
@@ -263,7 +263,7 @@ end = struct
(* Update local environment with a statement tracking temporal metadata
associated with assignment [ret] = [func(args)]. *)
let call_with_ret ?(alloc=false) current_stmt loc ret env kf =
- let rhs = Constructor.mk_lval ~loc ret in
+ let rhs = Smart_exp.lval ~loc ret in
let vals = assign ret rhs loc in
(* Track referent numbers of assignments via function calls.
Library functions (i.e., with no source code available) that return
@@ -284,7 +284,7 @@ end = struct
Extlib.may_map
(fun (lhs, rhs, flow) ->
let flow, rhs = match flow with
- | Indirect when alloc -> Direct, (Constructor.mk_deref ~loc rhs)
+ | Indirect when alloc -> Direct, (Smart_exp.deref ~loc rhs)
| _ -> flow, rhs
in
let stmt =
@@ -306,7 +306,7 @@ end = struct
| _ -> Options.fatal "[Temporal.call_memxxx] not a left-value"
in
let stmt =
- Constructor.mk_lib_call ~loc (RTL.mk_temporal_name name) args
+ Smart_stmt.lib_call ~loc (RTL.mk_temporal_name name) args
in
Env.add_stmt ~before:current_stmt ~post:false env kf stmt
else
@@ -321,7 +321,7 @@ end = struct
the implementation of the function should be empty and compiler should
be able to optimize that code out. *)
let name = (RTL.mk_temporal_name "reset_parameters") in
- let stmt = Constructor.mk_lib_call ~loc name [] in
+ let stmt = Smart_stmt.lib_call ~loc name [] in
let env = Env.add_stmt ~before:current_stmt ~post:false env kf stmt in
let stmt = Mk.reset_return_referent ~loc in
let env = Env.add_stmt ~before:current_stmt ~post:false env kf stmt in
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 009763c7931d6f8d47f548698052917a7551ed21..2df14a6f11f222d8a098245d820b8623e232d83d 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -141,7 +141,7 @@ let add_cast ~loc ?name env kf ctx strnum t_opt e =
None
new_ty
(fun v _ ->
- [ Constructor.mk_lib_call ~loc ~result:(Cil.var v) fname [ e ] ])
+ [ Smart_stmt.lib_call ~loc ~result:(Cil.var v) fname [ e ] ])
in
e, env
else if Gmp_types.Q.is_t ty || strnum = Str_R then
@@ -229,7 +229,7 @@ let conditional_to_exp ?(name="if") loc kf t_opt e1 (e2, env2) (e3, env3) =
let s = affect e3 in
Env.pop_and_get env3 s ~global_clear:false Env.Middle
in
- [ Constructor.mk_if ~loc ~cond:e1 then_blk ~else_blk ])
+ [ Smart_stmt.if_stmt ~loc ~cond:e1 then_blk ~else_blk ])
in
e, env
@@ -276,7 +276,7 @@ and context_insensitive_term_to_exp kf env t =
c, env, strnum, ""
| TLval lv ->
let lv, env, name = tlval_to_lval kf env lv in
- Constructor.mk_lval ~loc lv, env, C_number, name
+ Smart_exp.lval ~loc lv, env, C_number, name
| TSizeOf ty -> Cil.sizeOf ~loc ty, env, C_number, "sizeof"
| TSizeOfE t ->
let e, env = term_to_exp kf env t in
@@ -303,7 +303,7 @@ and context_insensitive_term_to_exp kf env t =
kf
~name:vname
(Some t)
- (fun _ ev -> [ Constructor.mk_lib_call ~loc name [ ev; e ] ])
+ (fun _ ev -> [ Smart_stmt.lib_call ~loc name [ ev; e ] ])
in
e, env, C_number, ""
else if Gmp_types.Q.is_t ty then
@@ -332,7 +332,7 @@ and context_insensitive_term_to_exp kf env t =
let e2, env = term_to_exp kf env t2 in
if Gmp_types.Z.is_t ty then
let name = name_of_mpz_arith_bop bop in
- let mk_stmts _ e = [ Constructor.mk_lib_call ~loc name [ e; e1; e2 ] ] in
+ let mk_stmts _ e = [ Smart_stmt.lib_call ~loc name [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
let _, e, env =
Env.new_var_and_mpz_init ~loc ~name env kf (Some t) mk_stmts
@@ -370,14 +370,14 @@ and context_insensitive_term_to_exp kf env t =
let mk_stmts _v e =
assert (Gmp_types.Z.is_t ty);
let cond =
- Constructor.mk_runtime_check
+ Smart_stmt.runtime_check
(Env.annotation_kind env)
kf
guard
p
in
Env.add_assert kf cond p;
- let instr = Constructor.mk_lib_call ~loc name [ e; e1; e2 ] in
+ let instr = Smart_stmt.lib_call ~loc name [ e; e1; e2 ] in
[ cond; instr ]
in
let name = Misc.name_of_binop bop in
@@ -435,7 +435,7 @@ and context_insensitive_term_to_exp kf env t =
(fun vi _e ->
let result = Cil.var vi in
let fname = "__gmpz_fits_ulong_p" in
- [ Constructor.mk_lib_call ~loc ~result fname [ e2 ] ])
+ [ Smart_stmt.lib_call ~loc ~result fname [ e2 ] ])
in
e, env
in
@@ -454,8 +454,8 @@ and context_insensitive_term_to_exp kf env t =
in
let pname = bop_name ^ "_rhs_fits_in_mp_bitcnt_t" in
let pred = { pred with pred_name = pname :: pred.pred_name } in
- let cond = Constructor.mk_runtime_check
- Constructor.RTE
+ let cond = Smart_stmt.runtime_check
+ Smart_stmt.RTE
kf
coerce_guard
pred
@@ -465,7 +465,7 @@ and context_insensitive_term_to_exp kf env t =
in
let result = Cil.var vi in
let name = "__gmpz_get_ui" in
- let instr = Constructor.mk_lib_call ~loc ~result name [ e2 ] in
+ let instr = Smart_stmt.lib_call ~loc ~result name [ e2 ] in
[ coerce_guard_cond; instr ]
in
let name = e2_name ^ bop_name ^ "_coerced" in
@@ -484,7 +484,7 @@ and context_insensitive_term_to_exp kf env t =
(* Create the shift instruction *)
let mk_shift_instr result_e =
let name = name_of_mpz_arith_bop bop in
- Constructor.mk_lib_call ~loc name [ result_e; e1; e2_as_bitcnt_e ]
+ Smart_stmt.lib_call ~loc name [ result_e; e1; e2_as_bitcnt_e ]
in
(* Put t in an option to use with comparison_to_exp and
@@ -515,8 +515,8 @@ and context_insensitive_term_to_exp kf env t =
in
let e1_guard_cond =
let pred = Logic_const.prel ~loc (Rge, t1, zero) in
- let cond = Constructor.mk_runtime_check
- Constructor.RTE
+ let cond = Smart_stmt.runtime_check
+ Smart_stmt.RTE
kf
e1_guard
pred
@@ -568,7 +568,7 @@ and context_insensitive_term_to_exp kf env t =
if Gmp_types.Z.is_t ty then
let mk_stmts _v e =
let name = name_of_mpz_arith_bop bop in
- let instr = Constructor.mk_lib_call ~loc name [ e; e1; e2 ] in
+ let instr = Smart_stmt.lib_call ~loc name [ e; e1; e2 ] in
[ instr ]
in
let name = Misc.name_of_binop bop in
@@ -646,7 +646,7 @@ and context_insensitive_term_to_exp kf env t =
(Some t)
(Misc.cty (Extlib.the li.l_type))
(fun vi _ ->
- [ Constructor.mk_lib_call ~loc ~result:(Cil.var vi) fname args ])
+ [ Smart_stmt.lib_call ~loc ~result:(Cil.var vi) fname args ])
else
(* build the arguments and compute the integer_ty of the parameters *)
let params_ty, args, env =
@@ -788,7 +788,7 @@ and comparison_to_exp
~name
Cil.intType
(fun v _ ->
- [ Constructor.mk_lib_call ~loc
+ [ Smart_stmt.lib_call ~loc
~result:(Cil.var v)
"__gmpz_cmp"
[ e1; e2 ] ])
@@ -855,7 +855,7 @@ and env_of_li li kf env loc =
let e, env = term_to_exp kf env t in
let stmt = match Typing.get_number_ty t with
| Typing.(C_integer _ | C_float _ | Nan) ->
- Constructor.mk_assigns ~loc ~result:(Cil.var vi) e
+ Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
| Typing.Gmpz ->
Gmp.init_set ~loc (Cil.var vi) vi_e e
| Typing.Rational ->
@@ -1033,7 +1033,7 @@ and translate_rte_annots:
fun pp elt kf env l ->
let old_valid = !is_visiting_valid in
let old_kind = Env.annotation_kind env in
- let env = Env.set_annotation_kind env Constructor.RTE in
+ let env = Env.set_annotation_kind env Smart_stmt.RTE in
let env =
List.fold_left
(fun env a -> match a.annot_content with
@@ -1078,7 +1078,7 @@ and translate_named_predicate kf env p =
Env.add_stmt
env
kf
- (Constructor.mk_runtime_check
+ (Smart_stmt.runtime_check
(Env.annotation_kind env)
kf
e
@@ -1168,7 +1168,7 @@ let assumes_predicate bhv =
bhv.b_assumes
let translate_preconditions kf kinstr env behaviors =
- let env = Env.set_annotation_kind env Constructor.Precondition in
+ let env = Env.set_annotation_kind env Smart_stmt.Precondition in
let do_behavior env b =
let assumes_pred = assumes_predicate b in
List.fold_left
@@ -1193,7 +1193,7 @@ let translate_preconditions kf kinstr env behaviors =
List.fold_left do_behavior env behaviors
let translate_postconditions kf kinstr env behaviors =
- let env = Env.set_annotation_kind env Constructor.Postcondition in
+ let env = Env.set_annotation_kind env Smart_stmt.Postcondition in
(* generate one guard by postcondition of each behavior *)
let do_behavior env b =
let env =
@@ -1284,7 +1284,7 @@ let translate_pre_code_annotation kf stmt env annot =
let convert env = match annot.annot_content with
| AAssert(l, _, p) ->
if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
- let env = Env.set_annotation_kind env Constructor.Assertion in
+ let env = Env.set_annotation_kind env Smart_stmt.Assertion in
if l <> [] then
not_yet env "@[assertion applied only on some behaviors@]";
translate_named_predicate kf env p
@@ -1296,7 +1296,7 @@ let translate_pre_code_annotation kf stmt env annot =
translate_pre_spec kf (Kstmt stmt) env spec ;
| AInvariant(l, loop_invariant, p) ->
if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
- let env = Env.set_annotation_kind env Constructor.Invariant in
+ let env = Env.set_annotation_kind env Smart_stmt.Invariant in
if l <> [] then
not_yet env "@[invariant applied only on some behaviors@]";
let env = translate_named_predicate kf env p in