Merge branch 'feature/basile/constructor-breakup' into 'master'

[eacsl] Breakup `Constructor` into smaller files

See merge request frama-c/frama-c!2799

.Makefile.lint

@@ -344,10 +344,3 @@ ML_LINT_KO+=src/plugins/variadic/standard.ml
 ML_LINT_KO+=src/plugins/variadic/translate.ml
 ML_LINT_KO+=src/plugins/variadic/va_build.ml
 ML_LINT_KO+=src/plugins/variadic/va_types.mli
-ML_LINT_KO+=src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
-ML_LINT_KO+=src/plugins/e-acsl/src/analyses/rte.ml
-ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
-ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
-ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/temporal.ml
-ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/temporal.mli
-

src/plugins/e-acsl/Makefile.in

@@ -64,7 +64,8 @@ SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
 
 # code generator
 SRC_CODE_GENERATOR:= \
-	constructor \
+	smart_exp \
+	smart_stmt \
 	gmp \
 	label \
 	env \

src/plugins/e-acsl/doc/Changelog

@@ -26,8 +26,8 @@ Plugin E-ACSL <next-release>
 ############################
 
 -* E-ACSL       [2020-08-28] Fix crash that may occur when translating
-	        properties that have been proved valid by another plug-in
-	        (frama-c/e-acsl#106).
+                properties that have been proved valid by another plug-in
+                (frama-c/e-acsl#106).
 -! E-ACSL       [2020-08-28] Remove option -e-acsl-prepare-ast.
 -! E-ACSL       [2020-08-28] Remove option -e-acsl-check.
 -  E-ACSL       [2020-08-07] Add support for logical array comparison

src/plugins/e-acsl/headers/header_spec.txt

@@ -52,8 +52,6 @@ src/analyses/typing.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/typing.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/at_with_lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/at_with_lscope.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/constructor.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/constructor.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/env.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/env.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/global_observer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
@@ -80,6 +78,10 @@ src/code_generator/quantif.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/quantif.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/rational.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/rational.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/smart_exp.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/smart_exp.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/smart_stmt.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/smart_stmt.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/temporal.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/temporal.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/translate.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL

src/plugins/e-acsl/src/analyses/rte.ml

@@ -27,7 +27,7 @@
 let warn_rte warn exn =
   if warn then
     Options.warning "@[@[cannot run RTE:@ %s.@]@ \
-Ignoring potential runtime errors in annotations." 
+                     Ignoring potential runtime errors in annotations."
       (Printexc.to_string exn)
 
 (* ************************************************************************** *)
@@ -45,8 +45,8 @@ let stmt ?(warn=true) =
          (let module L = Datatype.List(Code_annotation) in L.ty))
   with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
     ->
-      warn_rte warn exn;
-      fun _ _ -> []
+    warn_rte warn exn;
+    fun _ _ -> []
 
 let exp ?(warn=true) =
   try
@@ -57,8 +57,8 @@ let exp ?(warn=true) =
          (let module L = Datatype.List(Code_annotation) in L.ty))
   with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
     ->
-      warn_rte warn exn;
-      fun _ _ _ -> []
+    warn_rte warn exn;
+    fun _ _ _ -> []
 
 (*
 Local Variables:

src/plugins/e-acsl/src/code_generator/at_with_lscope.ml

@@ -39,8 +39,8 @@ let term_to_exp_ref
 (*****************************************************************************)
 
 (* Remove all the bindings for [kf]. [Cil_datatype.Kf.Hashtbl] does not
-  provide the [remove_all] function. Thus we need to keep calling [remove]
-  until all entries are removed. *)
+   provide the [remove_all] function. Thus we need to keep calling [remove]
+   until all entries are removed. *)
 let rec remove_all tbl kf =
   if Cil_datatype.Kf.Hashtbl.mem tbl kf then begin
     Cil_datatype.Kf.Hashtbl.remove tbl kf;
@@ -66,10 +66,10 @@ end
 (**************************************************************************)
 
 (* Builds the terms [t_size] and [t_shifted] from each
-  [Lvs_quantif(tmin, lv, tmax)] from [lscope]
-  where [t_size = tmax - tmin + (-1|0|1)] depending on whether the
+   [Lvs_quantif(tmin, lv, tmax)] from [lscope]
+   where [t_size = tmax - tmin + (-1|0|1)] depending on whether the
                                           inequalities are strict or large
-  and [t_shifted = lv - tmin + (-1|0)] (so that we start indexing at 0) *)
+   and [t_shifted = lv - tmin + (-1|0)] (so that we start indexing at 0) *)
 let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
   match lscope with
   | [] ->
@@ -97,29 +97,29 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
     in
     let iv = Interval.(extract_ival (infer t_size)) in
     (* The EXACT amount of memory that is needed can be known at runtime. This
-      is because the tightest bounds for the variables can be known at runtime.
-      Example: In the following predicate
+       is because the tightest bounds for the variables can be known at runtime.
+       Example: In the following predicate
         [\exists integer u; 9 <= u <= 13 &&
          \forall integer v; -5 < v <= (u <= 11 ? u + 6 : u - 9) ==>
            \at(u + v > 0, K)]
         the upper bound [M] for [v] depends on [u].
         In chronological order, [M] equals to 15, 16, 17, 3 and 4.
         Thus the tightest upper bound for [v] is [max(M)=17].
-      HOWEVER, computing that exact information requires extra nested loops,
-      prior to the [malloc] stmts, that will try all the possible values of the
-      variables involved in the bounds.
-      Instead of sacrificing time over memory (by performing these extra
-      computations), we consider that sacrificing memory over time is more
-      beneficial. In particular, though we may allocate more memory than
-      needed, the number of reads/writes into it is the same in both cases.
-      Conclusion: over-approximate [t_size] *)
+       HOWEVER, computing that exact information requires extra nested loops,
+       prior to the [malloc] stmts, that will try all the possible values of the
+       variables involved in the bounds.
+       Instead of sacrificing time over memory (by performing these extra
+       computations), we consider that sacrificing memory over time is more
+       beneficial. In particular, though we may allocate more memory than
+       needed, the number of reads/writes into it is the same in both cases.
+       Conclusion: over-approximate [t_size] *)
     let t_size = match Ival.min_and_max iv with
       | _, Some max ->
         Logic_const.tint ~loc max
       | _, None ->
         Error.not_yet
           "\\at on purely logic variables and with quantifier that uses \
-            too complex bound (E-ACSL cannot infer a finite upper bound to it)"
+           too complex bound (E-ACSL cannot infer a finite upper bound to it)"
     in
     (* Index *)
     let t_lv = Logic_const.tvar ~loc lv in
@@ -148,13 +148,13 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
 let size_from_sizes_and_shifts ~loc = function
   | [] ->
     (* No quantified variable. But still need to allocate [1*sizeof(_)] amount
-      of memory to store purely logic variables that are NOT quantified
-      (example: from \let). *)
+       of memory to store purely logic variables that are NOT quantified
+       (example: from \let). *)
     Cil.lone ~loc ()
   | (size, _) :: sizes_and_shifts ->
     List.fold_left
       (fun t_size (t_s, _) ->
-        Logic_const.term ~loc (TBinOp(Mult, t_size, t_s)) Linteger)
+         Logic_const.term ~loc (TBinOp(Mult, t_size, t_s)) Linteger)
       size
       sizes_and_shifts
 
@@ -171,35 +171,35 @@ let lval_at_index ~loc kf env (e_at, vi_at, t_index) =
   lval_at_index, env
 
 (* Associate to each possible tuple of quantifiers
-  a unique index from the set {n | 0 <= n < n_max}.
-  That index will serve to identify the memory location where the evaluation
-  of the term/predicate is stored for the given tuple of quantifier.
-  The following gives the smallest set of such indexes (hence we use the
-  smallest amount of memory in some respect):
-  To (t_shifted_n, t_shifted_n-1, ..., t_shifted_1)
-  where 0 <= t_shifted_i < beta_i
-  corresponds: \sum_{i=1}^n( t_shifted_i * \pi_{j=1}^{i-1}(beta_j) ) *)
+   a unique index from the set {n | 0 <= n < n_max}.
+   That index will serve to identify the memory location where the evaluation
+   of the term/predicate is stored for the given tuple of quantifier.
+   The following gives the smallest set of such indexes (hence we use the
+   smallest amount of memory in some respect):
+   To (t_shifted_n, t_shifted_n-1, ..., t_shifted_1)
+   where 0 <= t_shifted_i < beta_i
+   corresponds: \sum_{i=1}^n( t_shifted_i * \pi_{j=1}^{i-1}(beta_j) ) *)
 let index_from_sizes_and_shifts ~loc sizes_and_shifts =
   let product terms = List.fold_left
-    (fun product t ->
-      Logic_const.term ~loc (TBinOp(Mult, product, t)) Linteger)
-    (Cil.lone ~loc ())
-    terms
+      (fun product t ->
+         Logic_const.term ~loc (TBinOp(Mult, product, t)) Linteger)
+      (Cil.lone ~loc ())
+      terms
   in
   let sum, _ = List.fold_left
-    (fun (index, sizes) (t_size, t_shifted) ->
-      let pi_beta_j = product sizes in
-      let bi_mult_pi_beta_j =
-        Logic_const.term ~loc (TBinOp(Mult, t_shifted, pi_beta_j)) Linteger
-      in
-      let sum = Logic_const.term
-        ~loc
-        (TBinOp(PlusA, bi_mult_pi_beta_j, index))
-        Linteger
-      in
-      sum, t_size :: sizes)
-    (Cil.lzero ~loc (), [])
-    sizes_and_shifts
+      (fun (index, sizes) (t_size, t_shifted) ->
+         let pi_beta_j = product sizes in
+         let bi_mult_pi_beta_j =
+           Logic_const.term ~loc (TBinOp(Mult, t_shifted, pi_beta_j)) Linteger
+         in
+         let sum = Logic_const.term
+             ~loc
+             (TBinOp(PlusA, bi_mult_pi_beta_j, index))
+             Linteger
+         in
+         sum, t_size :: sizes)
+      (Cil.lzero ~loc (), [])
+      sizes_and_shifts
   in
   sum
 
@@ -225,62 +225,63 @@ let to_exp ~loc kf env pot label =
   in
   (* Creating the pointer *)
   let ty = match pot with
-  | Lscope.PoT_pred _ ->
-    Cil.intType
-  | Lscope.PoT_term t ->
-    begin match Typing.get_number_ty t with
-    | Typing.(C_integer _ | C_float _ | Nan) ->
-      Typing.get_typ t
-    | Typing.(Rational | Real) ->
-      Error.not_yet "\\at on purely logic variables and over real type"
-    | Typing.Gmpz ->
-      Error.not_yet "\\at on purely logic variables and over gmp type"
-    end
+    | Lscope.PoT_pred _ ->
+      Cil.intType
+    | Lscope.PoT_term t ->
+      begin match Typing.get_number_ty t with
+        | Typing.(C_integer _ | C_float _ | Nan) ->
+          Typing.get_typ t
+        | Typing.(Rational | Real) ->
+          Error.not_yet "\\at on purely logic variables and over real type"
+        | Typing.Gmpz ->
+          Error.not_yet "\\at on purely logic variables and over gmp type"
+      end
   in
   let ty_ptr = TPtr(ty, []) in
   let vi_at, e_at, env = Env.new_var
-    ~loc
-    ~name:"at"
-    ~scope:Varname.Function
-    env
-    kf
-    None
-    ty_ptr
-    (fun vi e ->
-      (* Handle [malloc] and [free] stmts *)
-      let lty_sizeof = Ctype Cil.(theMachine.typeOfSizeOf) in
-      let t_sizeof = Logic_const.term ~loc (TSizeOf ty) lty_sizeof in
-      let t_size = size_from_sizes_and_shifts ~loc sizes_and_shifts in
-      let t_size =
-        Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
-      in
-      Typing.type_term ~use_gmp_opt:false t_size;
-      let malloc_stmt = match Typing.get_number_ty t_size with
-      | Typing.C_integer IInt ->
-        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
-            ~result:(Cil.var vi)
-            "malloc"
-            [ e_size ]
-        in
-        malloc_stmt
-      | Typing.(C_integer _ | C_float _ | Gmpz) ->
-        Error.not_yet
-          "\\at on purely logic variables that needs to allocate \
-           too much memory (bigger than int_max bytes)"
-      | Typing.(Rational | Real | Nan) ->
-        Error.not_yet "quantification over non-integer type"
-      in
-      let free_stmt = Constructor.mk_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].
-        Thus we need to add [malloc] and [free] through dedicated functions. *)
-      Malloc.add kf malloc_stmt;
-      Free.add kf free_stmt;
-      [])
+      ~loc
+      ~name:"at"
+      ~scope:Varname.Function
+      env
+      kf
+      None
+      ty_ptr
+      (fun vi e ->
+         (* Handle [malloc] and [free] stmts *)
+         let lty_sizeof = Ctype Cil.(theMachine.typeOfSizeOf) in
+         let t_sizeof = Logic_const.term ~loc (TSizeOf ty) lty_sizeof in
+         let t_size = size_from_sizes_and_shifts ~loc sizes_and_shifts in
+         let t_size =
+           Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
+         in
+         Typing.type_term ~use_gmp_opt:false t_size;
+         let malloc_stmt = match Typing.get_number_ty t_size with
+           | Typing.C_integer IInt ->
+             let e_size, _ = term_to_exp kf env t_size in
+             let e_size = Cil.constFold false e_size in
+             let malloc_stmt =
+               Smart_stmt.lib_call ~loc
+                 ~result:(Cil.var vi)
+                 "malloc"
+                 [ e_size ]
+             in
+             malloc_stmt
+           | Typing.(C_integer _ | C_float _ | Gmpz) ->
+             Error.not_yet
+               "\\at on purely logic variables that needs to allocate \
+                too much memory (bigger than int_max bytes)"
+           | Typing.(Rational | Real | Nan) ->
+             Error.not_yet "quantification over non-integer type"
+         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].
+            Thus we need to add [malloc] and [free] through dedicated functions.
+         *)
+         Malloc.add kf malloc_stmt;
+         Free.add kf free_stmt;
+         [])
   in
   (* Index *)
   let t_index = index_from_sizes_and_shifts ~loc sizes_and_shifts in
@@ -295,34 +296,34 @@ 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
+         variable declarations. *)
+      [ Smart_stmt.block_stmt block ], env
     | Lscope.PoT_term t ->
       begin match Typing.get_number_ty t with
-      | Typing.(C_integer _ | C_float _ | Nan) ->
-        let env = Env.push env in
-        let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
-        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
-        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
-      | Typing.(Rational | Real) ->
-        Error.not_yet "\\at on purely logic variables and over real type"
-      | Typing.Gmpz ->
-        Error.not_yet "\\at on purely logic variables and over gmp type"
+        | Typing.(C_integer _ | C_float _ | Nan) ->
+          let env = Env.push env in
+          let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
+          let e, env = term_to_exp kf env t in
+          let e = Cil.constFold false e in
+          let storing_stmt =
+            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. *)
+          [ Smart_stmt.block_stmt block ], env
+        | Typing.(Rational | Real) ->
+          Error.not_yet "\\at on purely logic variables and over real type"
+        | Typing.Gmpz ->
+          Error.not_yet "\\at on purely logic variables and over gmp type"
       end
   in
   (* Storing loops *)
@@ -333,16 +334,16 @@ let to_exp ~loc kf env pot label =
   in
   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)
-    ~global_clear:false
-    Env.After
+      env
+      (Smart_stmt.block_stmt storing_loops_block)
+      ~global_clear:false
+      Env.After
   in
   (* Put at 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
 
 (*

src/plugins/e-acsl/src/code_generator/at_with_lscope.mli

@@ -24,7 +24,7 @@ open Cil_types
 open Cil_datatype
 
 (* Convert \at on terms or predicates in which we can find purely
-  logic variable. *)
+   logic variable. *)
 
 (**************************************************************************)
 (*************************** Translation **********************************)
@@ -39,8 +39,8 @@ val to_exp:
 (*****************************************************************************)
 
 (* The different possible evaluations of the [\at] under study are
-  stored in a memory location that needs to be alloted then freed.
-  This part is designed for that purpose. *)
+   stored in a memory location that needs to be alloted then freed.
+   This part is designed for that purpose. *)
 
 module Malloc: sig
   val find_all: kernel_function -> stmt list

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

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} *)

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

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 ->

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

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 ()) ])

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

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

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

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 ] ])

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

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