diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index a44d27242911d78ca3342a8cac5779d96a85f5d7..06edca935965881a93c24f23401dc0211922ed8e 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/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 \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 41708b793a5ad7c2b97a1cf4fb703068e7457a1f..f5d1c3fe39a487370af0db226395887366102ade 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.ml b/src/plugins/e-acsl/src/code_generator/smart_exp.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f3dac85ffd20bd197d046e874ae3a7a40f68e207
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/smart_exp.ml
@@ -0,0 +1,46 @@
+(**************************************************************************)
+(* *)
+(* 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:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.mli b/src/plugins/e-acsl/src/code_generator/smart_exp.mli
new file mode 100644
index 0000000000000000000000000000000000000000..566702f1e8012f361cfb3beaf9e3683bf50f94a4
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/smart_exp.mli
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(* *)
+(* 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:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
similarity index 70%
rename from src/plugins/e-acsl/src/code_generator/constructor.ml
rename to src/plugins/e-acsl/src/code_generator/smart_stmt.ml
index a38f36ce70e425255853780dbbf358bef43cc0ab..dec6438762f3afb494812fa1799af9bb3557ebc6 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.ml
+++ b/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:
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
similarity index 64%
rename from src/plugins/e-acsl/src/code_generator/constructor.mli
rename to src/plugins/e-acsl/src/code_generator/smart_stmt.mli
index d21c71e53a434f9905a89fc1ca49ab31df10a781..e0c919a7f8847b7c23e71d536b619837ed59a2f5 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.mli
+++ b/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
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 0b2cd0d3ad79f9a6f08f442da392e7013fd38041..284d57621d5e2f242f8ada787f1acc8c0d8648af 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/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 ../../../../.."
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index f9c92c19e8097a872a37edc83fa83301a79dd645..6ea105fd88a00e4e4c3621fc90511f9eb943bdc0 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/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 ../../../../.."