[eacsl] Breakup `Constructor` into smaller files

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/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/code_generator/smart_exp.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+let lval ~loc lv =
+  Cil.new_exp ~loc (Lval lv)
+
+let deref ~loc lv = lval ~loc (Mem lv, NoOffset)
+
+let subscript ~loc array idx =
+  match Misc.extract_uncoerced_lval array with
+  | Some { enode = Lval lv } ->
+    let subscript_lval = Cil.addOffsetLval (Index(idx, NoOffset)) lv in
+    lval ~loc subscript_lval
+  | Some _ | None ->
+    Options.fatal
+      ~current:true
+      "Trying to create a subscript on an array that is not an Lval: %a"
+      Cil_types_debug.pp_exp
+      array
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)

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

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+(* ********************************************************************** *)
+(* Helper functions to build expressions *)
+(* ********************************************************************** *)
+
+val lval: loc:location -> lval -> exp
+(** Construct an lval expression from an lval. *)
+
+val deref: loc:location -> exp -> exp
+(** Construct a dereference of an expression. *)
+
+val subscript: loc:location -> exp -> exp -> exp
+(** [mk_subscript ~loc array idx] Create an expression to access the [idx]'th
+    element of the [array]. *)
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)

src/plugins/e-acsl/src/code_generator/constructor.ml → src/plugins/e-acsl/src/code_generator/smart_stmt.ml

@@ -22,51 +22,21 @@
 
 open Cil_types
 
-(* ********************************************************************** *)
-(* Expressions *)
-(* ********************************************************************** *)
-
-let extract_uncoerced_lval e =
-  let rec aux e =
-    match e.enode with
-    | Lval _ -> Some e
-    | CastE (_, e) -> aux e
-    | _ -> None
-  in
-  aux e
-
-let mk_lval ~loc lval =
-  Cil.new_exp ~loc (Lval lval)
-
-let mk_deref ~loc lv = mk_lval ~loc (Mem lv, NoOffset)
-
-let mk_subscript ~loc array idx =
-  match extract_uncoerced_lval array with
-  | Some { enode = Lval lval } ->
-    let subscript_lval = Cil.addOffsetLval (Index(idx, NoOffset)) lval in
-    mk_lval ~loc subscript_lval
-  | Some _ | None ->
-    Options.fatal
-      ~current:true
-      "Trying to create a subscript on an array that is not an Lval: %a"
-      Cil_types_debug.pp_exp
-      array
-
 (* ********************************************************************** *)
 (* Statements *)
 (* ********************************************************************** *)
 
-let mk_stmt sk = Cil.mkStmt ~valid_sid:true sk
-let mk_instr i = mk_stmt (Instr i)
-let mk_block_stmt blk = mk_stmt (Block blk)
-let mk_call ~loc ?result e args = mk_instr (Call(result, e, args, loc))
+let stmt sk = Cil.mkStmt ~valid_sid:true sk
+let instr i = stmt (Instr i)
+let block_stmt blk = stmt (Block blk)
+let call ~loc ?result e args = instr (Call(result, e, args, loc))
 
-let mk_assigns ~loc ~result e = mk_instr (Set(result, e, loc))
+let assigns ~loc ~result e = instr (Set(result, e, loc))
 
-let mk_if ~loc ~cond ?(else_blk=Cil.mkBlock []) then_blk =
-  mk_stmt (If (cond, then_blk, else_blk, loc))
+let if_stmt ~loc ~cond ?(else_blk=Cil.mkBlock []) then_blk =
+  stmt (If (cond, then_blk, else_blk, loc))
 
-let mk_break ~loc = mk_stmt (Break loc)
+let break ~loc = stmt (Break loc)
 
 type annotation_kind =
   | Assertion
@@ -85,19 +55,19 @@ let kind_to_string loc k =
      | Invariant -> "Invariant"
      | RTE -> "RTE")
 
-let mk_block stmt b = match b.bstmts with
+let block stmt b = match b.bstmts with
   | [] ->
     (match stmt.skind with
      | Instr(Skip _) -> stmt
      | _ -> assert false)
   | [ s ] -> s
-  |  _ :: _ -> mk_block_stmt b
+  |  _ :: _ -> block_stmt b
 
 (* ********************************************************************** *)
 (* E-ACSL specific code *)
 (* ********************************************************************** *)
 
-let mk_lib_call ~loc ?result fname args =
+let lib_call ~loc ?result fname args =
   let vi =
     try Rtl.Symbols.find_vi fname
     with Rtl.Symbols.Unregistered _ as exn ->
@@ -133,32 +103,32 @@ let mk_lib_call ~loc ?result fname args =
     | TFun(_, None, _, _) -> []
     | _ -> assert false
   in
-  mk_call ~loc ?result f args
+  call ~loc ?result f args
 
-let mk_rtl_call ~loc ?result fname args =
-  mk_lib_call ~loc ?result (Functions.RTL.mk_api_name fname) args
+let rtl_call ~loc ?result fname args =
+  lib_call ~loc ?result (Functions.RTL.mk_api_name fname) args
 
 (* ************************************************************************** *)
 (** {2 Handling the E-ACSL's C-libraries, part II} *)
 (* ************************************************************************** *)
 
-let mk_full_init_stmt vi =
+let full_init_stmt vi =
   let loc = vi.vdecl in
-  mk_rtl_call ~loc "full_init" [ Cil.evar ~loc vi ]
+  rtl_call ~loc "full_init" [ Cil.evar ~loc vi ]
 
-let mk_initialize ~loc (host, offset as lv) = match host, offset with
+let initialize ~loc (host, offset as lv) = match host, offset with
   | Var _, NoOffset ->
-    mk_rtl_call ~loc "full_init" [ Cil.mkAddrOf ~loc lv ]
+    rtl_call ~loc "full_init" [ Cil.mkAddrOf ~loc lv ]
   | _ ->
     let typ = Cil.typeOfLval lv in
-    mk_rtl_call ~loc
+    rtl_call ~loc
       "initialize"
       [ Cil.mkAddrOf ~loc lv; Cil.new_exp loc (SizeOf typ) ]
 
-let mk_named_store_stmt name ?str_size vi =
+let named_store_stmt name ?str_size vi =
   let ty = Cil.unrollType vi.vtype in
   let loc = vi.vdecl in
-  let store = mk_rtl_call ~loc name in
+  let store = rtl_call ~loc name in
   match ty, str_size with
   | TArray(_, Some _,_,_), None ->
     store [ Cil.evar ~loc vi; Cil.sizeOf ~loc ty ]
@@ -178,27 +148,27 @@ let mk_named_store_stmt name ?str_size vi =
       Printer.pp_typ ty
       Printer.pp_exp size
 
-let mk_store_stmt ?str_size vi =
-  mk_named_store_stmt "store_block" ?str_size vi
+let store_stmt ?str_size vi =
+  named_store_stmt "store_block" ?str_size vi
 
-let mk_duplicate_store_stmt ?str_size vi =
-  mk_named_store_stmt "store_block_duplicate" ?str_size vi
+let duplicate_store_stmt ?str_size vi =
+  named_store_stmt "store_block_duplicate" ?str_size vi
 
-let mk_delete_stmt ?(is_addr=false) vi =
+let delete_stmt ?(is_addr=false) vi =
   let loc = vi.vdecl in
-  let mk = mk_rtl_call ~loc "delete_block" in
+  let mk = rtl_call ~loc "delete_block" in
   match is_addr, Cil.unrollType vi.vtype with
   | _, TArray(_, Some _, _, _) | true, _ -> mk [ Cil.evar ~loc vi ]
   | _ -> mk [ Cil.mkAddrOfVi vi ]
 
-let mk_mark_readonly vi =
+let mark_readonly vi =
   let loc = vi.vdecl in
-  mk_rtl_call ~loc "mark_readonly" [ Cil.evar ~loc vi ]
+  rtl_call ~loc "mark_readonly" [ Cil.evar ~loc vi ]
 
-let mk_runtime_check_with_msg ~loc msg kind kf e =
+let runtime_check_with_msg ~loc msg kind kf e =
   let file = (fst loc).Filepath.pos_path in
   let line = (fst loc).Filepath.pos_lnum in
-  mk_rtl_call ~loc
+  rtl_call ~loc
     "assert"
     [ e;
       kind_to_string loc kind;
@@ -207,13 +177,13 @@ let mk_runtime_check_with_msg ~loc msg kind kf e =
       Cil.mkString ~loc (Filepath.Normalized.to_pretty_string file);
       Cil.integer loc line ]
 
-let mk_runtime_check kind kf e p =
+let runtime_check kind kf e p =
   let loc = p.pred_loc in
   let msg =
     Kernel.Unicode.without_unicode
       (Format.asprintf "%a@?" Printer.pp_predicate) p
   in
-  mk_runtime_check_with_msg ~loc msg kind kf e
+  runtime_check_with_msg ~loc msg kind kf e
 
 (*
 Local Variables:

src/plugins/e-acsl/src/code_generator/constructor.mli → src/plugins/e-acsl/src/code_generator/smart_stmt.mli

@@ -20,97 +20,73 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Smart constructors for building C code. *)
-
 open Cil_types
-open Cil_datatype
-
-(* ********************************************************************** *)
-(* Expressions *)
-(* ********************************************************************** *)
-
-val extract_uncoerced_lval: exp -> exp option
-(** Unroll the [CastE] part of the expression until an [Lval] is found, and
-    return it.
-
-    If at some point the expression is neither a [CastE] nor an [Lval], then
-    return [None]. *)
-
-val mk_lval: loc:location -> lval -> exp
-(** Construct an lval expression from an lval. *)
-
-val mk_deref: loc:Location.t -> exp -> exp
-(** Construct a dereference of an expression. *)
-
-val mk_subscript: loc:location -> exp -> exp -> exp
-(** [mk_subscript ~loc array idx] Create an expression to access the [idx]'th
-    element of the [array]. *)
 
 (* ********************************************************************** *)
-(* Statements *)
+(* Helper functions to build statements *)
 (* ********************************************************************** *)
 
-val mk_stmt: stmtkind -> stmt
+val stmt: stmtkind -> stmt
 (** Create a statement from a statement kind. *)
 
-val mk_block: stmt -> block -> stmt
+val block: stmt -> block -> stmt
 (** Create a block statement from a block to replace a given statement.
     Requires that (1) the block is not empty, or (2) the statement is a skip. *)
 
-val mk_block_stmt: block -> stmt
+val block_stmt: block -> stmt
 (** Create a block statement from a block *)
 
-val mk_assigns: loc:location -> result:lval -> exp -> stmt
-(** [mk_assigns ~loc ~result value] create a statement to assign the [value]
+val assigns: loc:location -> result:lval -> exp -> stmt
+(** [assigns ~loc ~result value] create a statement to assign the [value]
     expression to the [result] lval. *)
 
-val mk_if:
+val if_stmt:
   loc:location -> cond:exp -> ?else_blk:block -> block -> stmt
-(** [mk_if ~loc ~cond ~then_blk ~else_blk] create an if statement with [cond]
+(** [if ~loc ~cond ~then_blk ~else_blk] create an if statement with [cond]
     as condition and [then_blk] and [else_blk] as respectively "then" block and
     "else" block. *)
 
-val mk_break: loc:location -> stmt
+val break: loc:location -> stmt
 (** Create a break statement *)
 
 (* ********************************************************************** *)
 (* E-ACSL specific code: build calls to its RTL API *)
 (* ********************************************************************** *)
 
-val mk_lib_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
+val lib_call: loc:location -> ?result:lval -> string -> exp list -> stmt
 (** Construct a call to a library function with the given name.
     @raise Rtl.Symbols.Unregistered if the given string does not represent
     such a function or if library functions were never registered (only possible
     when using E-ACSL through its API). *)
 
-val mk_rtl_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
-(** Special version of [mk_lib_call] for E-ACSL's RTL functions. *)
+val rtl_call: loc:location -> ?result:lval -> string -> exp list -> stmt
+(** Special version of [lib_call] for E-ACSL's RTL functions. *)
 
-val mk_store_stmt: ?str_size:exp -> varinfo -> stmt
+val store_stmt: ?str_size:exp -> varinfo -> stmt
 (** Construct a call to [__e_acsl_store_block] that observes the allocation of
     the given varinfo. See [share/e-acsl/e_acsl.h] for details about this
     function. *)
 
-val mk_duplicate_store_stmt: ?str_size:exp -> varinfo -> stmt
-(** Same as [mk_store_stmt] for [__e_acsl_duplicate_store_block] that first
+val duplicate_store_stmt: ?str_size:exp -> varinfo -> stmt
+(** Same as [store_stmt] for [__e_acsl_duplicate_store_block] that first
     checks for a previous allocation of the given varinfo. *)
 
-val mk_delete_stmt: ?is_addr:bool -> varinfo -> stmt
-(** Same as [mk_store_stmt] for [__e_acsl_delete_block] that observes the
+val delete_stmt: ?is_addr:bool -> varinfo -> stmt
+(** Same as [store_stmt] for [__e_acsl_delete_block] that observes the
     de-allocation of the given varinfo.
     If [is_addr] is false (default), take the address of varinfo. *)
 
-val mk_full_init_stmt: varinfo -> stmt
-(** Same as [mk_store_stmt] for [__e_acsl_full_init] that observes the
+val full_init_stmt: varinfo -> stmt
+(** Same as [store_stmt] for [__e_acsl_full_init] that observes the
     initialization of the given varinfo. The varinfo is the address to fully
     initialize, no [addrOf] is taken. *)
 
-val mk_initialize: loc:location -> lval -> stmt
-(** Same as [mk_store_stmt] for [__e_acsl_initialize] that observes the
+val initialize: loc:location -> lval -> stmt
+(** Same as [store_stmt] for [__e_acsl_initialize] that observes the
     initialization of the given left-value. *)
 
-val mk_mark_readonly: varinfo -> stmt
-(** Same as [mk_store_stmt] for [__e_acsl_markreadonly] that observes the
+val mark_readonly: varinfo -> stmt
+(** Same as [store_stmt] for [__e_acsl_markreadonly] that observes the
     read-onlyness of the given varinfo. *)
 
 type annotation_kind =
@@ -120,16 +96,16 @@ type annotation_kind =
   | Invariant
   | RTE
 
-val mk_runtime_check:
+val runtime_check:
   annotation_kind -> kernel_function -> exp -> predicate -> stmt
-(** [mk_runtime_check kind kf e p] generates a runtime check for predicate [p]
+(** [runtime_check kind kf e p] generates a runtime check for predicate [p]
     by building a call to [__e_acsl_assert]. [e] (or [!e] if [reverse] is set to
     [true]) is the C translation of [p], [kf] is the current kernel_function and
     [kind] is the annotation kind of [p]. *)
 
-val mk_runtime_check_with_msg:
+val runtime_check_with_msg:
   loc:location -> string -> annotation_kind -> kernel_function -> exp -> stmt
-(** [mk_runtime_check_with_msg kind kf e msg] generates a runtime check for [e]
+(** [runtime_check_with_msg kind kf e msg] generates a runtime check for [e]
     (or [!e] if [reverse] is [true]) by building a call to [__e_acsl_assert].
     [msg] is the message printed if the runtime check fails. [loc] is the
     location printed in the message if the runtime check fails. [kf] is the

src/plugins/e-acsl/src/libraries/misc.ml

@@ -189,6 +189,15 @@ module Id_term =
       let mem_project = Datatype.never_any_project
     end)
 
+let extract_uncoerced_lval e =
+  let rec aux e =
+    match e.enode with
+    | Lval _ -> Some e
+    | CastE (_, e) -> aux e
+    | _ -> None
+  in
+  aux e
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

src/plugins/e-acsl/src/libraries/misc.mli

@@ -81,6 +81,13 @@ val finite_min_and_max: Ival.t -> Integer.t * Integer.t
 module Id_term: Datatype.S_with_collections with type t = term
 (** Datatype for terms that relies on physical equality. *)
 
+val extract_uncoerced_lval: exp -> exp option
+(** Unroll the [CastE] part of the expression until an [Lval] is found, and
+    return it.
+
+    If at some point the expression is neither a [CastE] nor an [Lval], then
+    return [None]. *)
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."