diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 797036119ec8343dbbb2ab33c695b11982eab9a5..9321f0f5a8d863065f3ed19c1ae5b9f884a67f5e 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -65,6 +65,7 @@ SRC_PROJECT_INITIALIZER:=\
# code generator
SRC_CODE_GENERATOR:= \
+ constructor \
gmp \
label \
env \
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 371c3b8dfbf8f81e55b0f76b0403b40bbff700ff..b34e97b17b4aeed7d54557a162005a38fec68a6c 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,10 @@ 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 =
- Misc.mk_call ~loc ~result:(Cil.var vi) "malloc" [e_size]
+ Constructor.mk_lib_call ~loc
+ ~result:(Cil.var vi)
+ "malloc"
+ [e_size]
in
malloc_stmt
| Typing.(C_integer _ | C_float _ | Gmpz) ->
@@ -270,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 = Misc.mk_call ~loc "free" [e] 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].
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0e72a6f1e6fa0098dab2d40552685ae992a8cf7f
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/constructor.ml
@@ -0,0 +1,165 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2018 *)
+(* 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
+
+(* ********************************************************************** *)
+(* Expressions *)
+(* ********************************************************************** *)
+
+let mk_deref ~loc lv = Cil.new_exp ~loc (Lval(Mem(lv), NoOffset))
+
+(* ********************************************************************** *)
+(* Statements *)
+(* ********************************************************************** *)
+
+let mk_stmt sk = Cil.mkStmt ~valid_sid:true sk
+let mk_instr i = mk_stmt (Instr i)
+let mk_call ~loc ?result e args = mk_instr (Call(result, e, args, loc))
+
+type annotation_kind =
+ | Assertion
+ | Precondition
+ | Postcondition
+ | Invariant
+ | RTE
+
+let kind_to_string loc k =
+ Cil.mkString
+ ~loc
+ (match k with
+ | Assertion -> "Assertion"
+ | Precondition -> "Precondition"
+ | Postcondition -> "Postcondition"
+ | Invariant -> "Invariant"
+ | RTE -> "RTE")
+
+let mk_block stmt b = match b.bstmts with
+ | [] ->
+ (match stmt.skind with
+ | Instr(Skip _) -> stmt
+ | _ -> assert false)
+ | [ s ] -> s
+ | _ :: _ -> mk_stmt (Block b)
+
+(* ********************************************************************** *)
+(* E-ACSL specific code *)
+(* ********************************************************************** *)
+
+let mk_lib_call ~loc ?result fname args =
+ let vi = Misc.get_lib_fun_vi fname in
+ let f = Cil.evar ~loc vi in
+ vi.vreferenced <- true;
+ let make_args args ty_params =
+ List.map2
+ (fun (_, ty, _) arg ->
+ let e =
+ match ty, Cil.unrollType (Cil.typeOf arg), arg.enode with
+ | TPtr _, TArray _, Lval lv -> Cil.new_exp ~loc (StartOf lv)
+ | TPtr _, TArray _, _ -> assert false
+ | _, _, _ -> arg
+ in
+ Cil.mkCast ~force:false ~newt:ty ~e)
+ ty_params
+ args
+ in
+ let args = match vi.vtype with
+ | TFun(_, Some params, _, _) -> make_args args params
+ | TFun(_, None, _, _) -> []
+ | _ -> assert false
+ in
+ mk_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
+
+(* ************************************************************************** *)
+(** {2 Handling the E-ACSL's C-libraries, part II} *)
+(* ************************************************************************** *)
+
+let mk_full_init_stmt ?(addr=true) vi =
+ let loc = vi.vdecl in
+ let mk = mk_rtl_call ~loc "full_init" in
+ match addr, Cil.unrollType vi.vtype with
+ | _, TArray(_,Some _, _, _) | false, _ -> mk [ Cil.evar ~loc vi ]
+ | _ -> mk [ Cil.mkAddrOfVi vi ]
+
+let mk_initialize ~loc (host, offset as lv) = match host, offset with
+ | Var _, NoOffset ->
+ mk_rtl_call ~loc "full_init" [ Cil.mkAddrOf ~loc lv ]
+ | _ ->
+ let typ = Cil.typeOfLval lv in
+ mk_rtl_call ~loc
+ "initialize"
+ [ Cil.mkAddrOf ~loc lv; Cil.new_exp loc (SizeOf typ) ]
+
+let mk_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
+ match ty, str_size with
+ | TArray(_, Some _,_,_), None ->
+ store [ Cil.evar ~loc vi ; Cil.sizeOf ~loc ty ]
+ | TPtr(TInt(IChar, _), _), Some size -> store [ Cil.evar ~loc vi ; size ]
+ | _, None -> store [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
+ | _, Some _ -> assert false
+
+let mk_store_stmt ?str_size vi =
+ mk_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 mk_delete_stmt vi =
+ let loc = vi.vdecl in
+ let mk = mk_rtl_call ~loc "delete_block" in
+ match Cil.unrollType vi.vtype with
+ | TArray(_, Some _, _, _) -> mk [ Cil.evar ~loc vi ]
+ | _ -> mk [ Cil.mkAddrOfVi vi ]
+
+let mk_mark_readonly vi =
+ let loc = vi.vdecl in
+ mk_rtl_call ~loc "mark_readonly" [ Cil.evar ~loc vi ]
+
+let mk_runtime_check ?(reverse=false) kind kf e p =
+ let loc = p.pred_loc in
+ let msg =
+ Kernel.Unicode.without_unicode
+ (Format.asprintf "%a@?" Printer.pp_predicate) p
+ in
+ let line = (fst loc).Filepath.pos_lnum in
+ let e =
+ if reverse then e else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
+ in
+ mk_rtl_call ~loc
+ "assert"
+ [ e;
+ kind_to_string loc kind;
+ Cil.mkString ~loc (Functions.RTL.get_original_name kf);
+ Cil.mkString ~loc msg;
+ Cil.integer loc line ]
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/constructor.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5e5955934719abddc1df496c2c8e597f1fed0e96
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/constructor.mli
@@ -0,0 +1,69 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Smart constructors for building C code. *)
+
+open Cil_types
+open Cil_datatype
+
+val mk_deref: loc:Location.t -> exp -> exp
+(** Make a dereference of an expression *)
+
+val mk_block: stmt -> block -> stmt
+
+(* ********************************************************************** *)
+(* E-ACSL specific code *)
+(* ********************************************************************** *)
+
+val mk_lib_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
+(** Call of a library function.
+ @raise Unregistered_library_function if the given string does not represent
+ such a function or if these 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 mk_store_stmt: ?str_size:exp -> varinfo -> stmt
+val mk_duplicate_store_stmt: ?str_size:exp -> varinfo -> stmt
+val mk_delete_stmt: varinfo -> stmt
+val mk_full_init_stmt: ?addr:bool -> varinfo -> stmt
+val mk_initialize: loc:location -> lval -> stmt
+val mk_mark_readonly: varinfo -> stmt
+
+type annotation_kind =
+ | Assertion
+ | Precondition
+ | Postcondition
+ | Invariant
+ | RTE
+
+val mk_runtime_check:
+ ?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate ->
+ stmt
+(** Generate a runtime check of the given expression. *)
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 1042770c680c09015d363bdb5eb04e2bbd8b685e..9c0be44c094927cd44edf3d1666ede2592be004e 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: Misc.annotation_kind;
+ annotation_kind: Constructor.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 = Misc.Assertion;
+ annotation_kind = Constructor.Assertion;
new_global_vars = [];
global_mp_tbl = empty_mp_tbl;
env_stack = [];
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 489a6907275b71b32cb6b5b14c5133d4866a97c6..a9dfd21d381adff8855b2c11c5c9dbf635af85c5 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -139,8 +139,8 @@ end
(** {2 Current annotation kind} *)
(* ************************************************************************** *)
-val annotation_kind: t -> Misc.annotation_kind
-val set_annotation_kind: t -> Misc.annotation_kind -> t
+val annotation_kind: t -> Constructor.annotation_kind
+val set_annotation_kind: t -> Constructor.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 d4ad9545a6450780007943b9567b1488cd4d220f..aaf25ead522ae9486524b18d1f17daf77143f597 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.ml
@@ -112,8 +112,8 @@ let mk_init_function env =
Varinfo.Hashtbl.fold_sorted
(fun vi _ stmts ->
(* a global is both allocated and initialized *)
- Misc.mk_store_stmt vi
- :: Misc.mk_initialize ~loc:Location.unknown (Cil.var vi)
+ Constructor.mk_store_stmt vi
+ :: Constructor.mk_initialize ~loc:Location.unknown (Cil.var vi)
:: stmts)
tbl
stmts
@@ -126,9 +126,9 @@ let mk_init_function env =
let e = Cil.new_exp ~loc:loc (Const (CStr s)) in
let str_size = Cil.new_exp loc (SizeOfStr s) in
Cil.mkStmtOneInstr ~valid_sid:true (Set(Cil.var vi, e, loc))
- :: Misc.mk_store_stmt ~str_size vi
- :: Misc.mk_full_init_stmt ~addr:false vi
- :: Misc.mk_mark_readonly vi
+ :: Constructor.mk_store_stmt ~str_size vi
+ :: Constructor.mk_full_init_stmt ~addr:false vi
+ :: Constructor.mk_mark_readonly vi
:: stmts)
stmts
in
@@ -172,8 +172,7 @@ let mk_init_function env =
let mk_delete_stmts stmts =
Varinfo.Hashtbl.fold_sorted
- (fun vi _l acc ->
- Misc.mk_delete_stmt vi :: acc)
+ (fun vi _l acc -> Constructor.mk_delete_stmt vi :: acc)
tbl
stmts
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index ace7bc933c209463b1f177d99debd34bb4b20d1b..2d20463bc3c6693d80458fb28f69f312e5a2646c 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
- Misc.mk_call ~loc (prefix ^ funname) [ e ]
+ Constructor.mk_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
@@ -72,7 +72,7 @@ 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 e in
- Misc.mk_call ~loc (fname ^ suf) (ev :: args)
+ Constructor.mk_lib_call ~loc (fname ^ suf) (ev :: args)
end else
Cil.mkStmtOneInstr ~valid_sid:true (Set(lv, e, e.eloc))
@@ -92,8 +92,8 @@ let init_set ~loc lv ev e =
(match e.enode with
| Lval elv ->
assert (Gmp_types.Z.is_t (Cil.typeOf ev));
- let call = Misc.mk_call
- ~loc
+ let call =
+ Constructor.mk_lib_call ~loc
"__gmpz_import"
[ ev;
Cil.one ~loc;
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index a4503120fd679521759deba4890bcadfa59decf7..43ea6d2192fe0e4bc32ea29db6a396bcb6de1d6e 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -84,7 +84,7 @@ let replace_literal_string_in_exp ~is_global_init env kf e =
if is_global_init then e, env else Literal_observer.exp_in_depth env kf e
let inject_in_local_init loc env kf vi = function
- | ConsInit (fvi, sz :: _, _) as init
+ | ConsInit (fvi, _sz :: _, _) as init
when Functions.Libc.is_vla_alloc_name fvi.vname ->
(* handle variable-length array allocation via [__fc_vla_alloc]. Here each
instance of [__fc_vla_alloc] is rewritten to [alloca] (that is used to
@@ -97,8 +97,7 @@ let inject_in_local_init loc env kf vi = function
fvi.vname <- Functions.Libc.actual_alloca;
(* Since we need to pass [vi] by value, cannot use [Misc.mk_store_stmt]
here. Do it manually. *)
- let sname = Functions.RTL.mk_api_name "store_block" in
- let store = Misc.mk_call ~loc sname [ Cil.evar vi ; sz ] in
+ let store = Constructor.mk_store_stmt vi in
let env = Env.add_stmt ~post:true env kf store in
init, env
@@ -173,15 +172,14 @@ let add_initializer loc ?vi lv ?(post=false) stmt env kf =
let new_stmt =
(* bitfields are not yet supported ==> no initializer.
a [not_yet] will be raised in [Translate]. *)
- if Cil.isBitfield lv
- then Cil.mkEmptyStmt ()
- else Misc.mk_initialize ~loc lv
+ if Cil.isBitfield lv then Cil.mkEmptyStmt ()
+ else Constructor.mk_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 = Misc.mk_store_stmt vi in
+ let new_stmt = Constructor.mk_store_stmt vi in
Env.add_stmt ~post ~before env kf new_stmt
in
env
@@ -291,17 +289,17 @@ let add_new_block_in_stmt env kf stmt =
if is_main kf && Mmodel_analysis.use_model () then begin
let stmts = b.bstmts in
let l = List.rev stmts in
- let mclean = (Functions.RTL.mk_api_name "memory_clean") in
match l with
| [] -> assert false (* at least the 'return' stmt *)
| ret :: l ->
let loc = Stmt.loc stmt in
let delete_stmts =
- Global_observer.mk_delete_stmts [ Misc.mk_call ~loc mclean []; ret ]
+ Global_observer.mk_delete_stmts
+ [ Constructor.mk_rtl_call ~loc "memory_clean" []; ret ]
in
b.bstmts <- List.rev l @ delete_stmts
end;
- let new_stmt = Misc.mk_block stmt b in
+ let new_stmt = Constructor.mk_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. *)
@@ -331,7 +329,7 @@ let add_new_block_in_stmt env kf stmt =
let post_block, env =
Env.pop_and_get
env
- (Misc.mk_block new_stmt pre_block)
+ (Constructor.mk_block new_stmt pre_block)
~global_clear:false
Env.Before
in
@@ -340,7 +338,7 @@ let add_new_block_in_stmt env kf stmt =
then Cil.transient_block post_block
else post_block
in
- let res = Misc.mk_block new_stmt post_block in
+ let res = Constructor.mk_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
@@ -512,10 +510,9 @@ and inject_in_block (env: Env.t) kf blk =
if Functions.instrument kf then
List.fold_left
(fun acc vi ->
- if Mmodel_analysis.must_model_vi ~kf vi then
- Misc.mk_delete_stmt vi :: acc
- else
- acc)
+ if Mmodel_analysis.must_model_vi ~kf vi
+ then Constructor.mk_delete_stmt vi :: acc
+ else acc)
stmts
blk.blocals
else
@@ -548,7 +545,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 Misc.mk_store_stmt vi :: acc
+ then Constructor.mk_store_stmt vi :: acc
else acc)
blk.bstmts
blk.blocals;
@@ -735,8 +732,7 @@ let inject_mmodel_initializer main =
in
let ptr_size = Cil.sizeOf loc Cil.voidPtrType in
let args = args @ [ ptr_size ] in
- let name = Functions.RTL.mk_api_name "memory_init" in
- let init = Misc.mk_call loc name args in
+ let init = Constructor.mk_rtl_call loc "memory_init" args in
main.sbody.bstmts <- init :: main.sbody.bstmts
in
Extlib.may handle_main main
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 7adcd834c2c3c59b2c1a97912d5c86384330586a..eb4b4dd749380fbc85e19a4cad20d61bc09a2a7b 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -81,10 +81,10 @@ 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
- Misc.mk_block last blk :: stmts, env, invariants != []
+ Constructor.mk_block last blk :: stmts, env, invariants != []
| s :: tl -> handle_invariants (s :: stmts, env, false) tl
in
- let env = Env.set_annotation_kind env Misc.Invariant in
+ let env = Env.set_annotation_kind env Constructor.Invariant in
let stmts, env, has_loop = handle_invariants ([], env, false) stmts in
let new_blk = { blk with bstmts = List.rev stmts } in
{ stmt with skind = Loop([], new_blk, loc, cont, break) },
@@ -274,7 +274,7 @@ 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 =
- Misc.mk_e_acsl_guard ~reverse:true Misc.RTE kf e p, env
+ Constructor.mk_runtime_check ~reverse:true Constructor.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 = Cil.mkStmt ~valid_sid:true (Block b) 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 f3a3805994a544b5666125dbd82367ff25a66cdd..cba197a5cc4d079ed1acb79523f79417d774380a 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 *)
- Misc.mk_store_stmt
+ Constructor.mk_store_stmt
env
kf
vars
@@ -48,7 +48,7 @@ let duplicate_store ?before env kf vars =
tracking_stmt
?before
Varinfo.Set.fold
- Misc.mk_duplicate_store_stmt
+ Constructor.mk_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 *)
- Misc.mk_delete_stmt
+ Constructor.mk_delete_stmt
env
kf
vars
@@ -66,7 +66,7 @@ let delete_from_set ?before env kf vars =
tracking_stmt
?before
Varinfo.Set.fold
- Misc.mk_delete_stmt
+ Constructor.mk_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 4d80c4d8cc2f49c4a8426775e530a87bc44b5604..e3f17959d0851e8bb896257de8917188c6274088 100644
--- a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
@@ -126,7 +126,7 @@ let call ~loc kf name ctx env t =
ctx
(fun v _ ->
let name = Functions.RTL.mk_api_name name in
- [ Misc.mk_call ~loc ~result:(Cil.var v) name [ e ] ])
+ [ Constructor.mk_lib_call ~loc ~result:(Cil.var v) name [ e ] ])
in
res, env
@@ -159,8 +159,11 @@ let gmp_to_sizet ~loc kf env size p =
None
sizet
(fun vi _ ->
- [ Misc.mk_e_acsl_guard ~reverse:true Misc.RTE kf guard p;
- Misc.mk_call ~loc ~result:(Cil.var vi) "__gmpz_get_ui" [ size ] ])
+ [ Constructor.mk_runtime_check ~reverse:true Constructor.RTE kf guard p;
+ Constructor.mk_lib_call ~loc
+ ~result:(Cil.var vi)
+ "__gmpz_get_ui"
+ [ size ] ])
in
e, env
@@ -242,7 +245,7 @@ let call_memory_block ~loc kf name ctx env ptr r p =
| "initialized" -> [ ptr; size ]
| _ -> Error.not_yet ("builtin " ^ name)
in
- [ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
+ [ Constructor.mk_lib_call ~loc ~result:(Cil.var v) fname args ])
in
e, env
@@ -346,8 +349,10 @@ let call_with_size ~loc kf name ctx env t p =
(fun v _ ->
let ty = Misc.cty t.term_type in
let sizeof = Misc.mk_ptr_sizeof ty loc in
- let fname = Functions.RTL.mk_api_name name in
- [ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e; sizeof ] ])
+ [ Constructor.mk_rtl_call ~loc
+ ~result:(Cil.var v)
+ name
+ [ e; sizeof ] ])
in
res, env
in
@@ -384,9 +389,8 @@ let call_valid ~loc kf name ctx env t p =
(fun v _ ->
let ty = Misc.cty t.term_type in
let sizeof = Misc.mk_ptr_sizeof ty loc in
- let fname = Functions.RTL.mk_api_name name in
let args = [ e; sizeof; base; base_addr ] in
- [ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
+ [ Constructor.mk_rtl_call ~loc ~result:(Cil.var v) name args ])
in
res, env
in
diff --git a/src/plugins/e-acsl/src/code_generator/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
index 8145541f8c04c5bd1869aa124730dd24509beadd..9218ce231196bb1ae155d14968daeb25a44537dd 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -154,7 +154,10 @@ let add_cast ~loc ?name e env kf ty =
None
Cil.doubleType
(fun v _ ->
- [ Misc.mk_call ~loc ~result:(Cil.var v) "__gmpq_get_d" [ e ] ])
+ [ Constructor.mk_lib_call ~loc
+ ~result:(Cil.var v)
+ "__gmpq_get_d"
+ [ e ] ])
in
e, env
in
@@ -199,7 +202,8 @@ let cmp ~loc bop e1 e2 env kf t_opt =
t_opt
~name
Cil.intType
- (fun v _ -> [ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e1; e2 ] ])
+ (fun v _ ->
+ [ Constructor.mk_lib_call ~loc ~result:(Cil.var v) fname [ e1; e2 ] ])
in
Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
@@ -228,7 +232,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 = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
+ let mk_stmts _ e = [ Constructor.mk_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 9e49453af8a927e8eae4b332dfab62a87398760e..24d3bc62e2bbc1dc966e1c1c7cc70be81e08e0d4 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
- Misc.mk_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs ]
+ Constructor.mk_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
- Misc.mk_call ~loc fname [ lhs ; Cil.integer ~loc pos ]
+ Constructor.mk_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
- Misc.mk_call ~loc fname [ exp ; Cil.integer ~loc pos ; sz ]
+ Constructor.mk_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");
- Misc.mk_call ~loc (RTL.mk_temporal_name fname) [ lhs ]
+ Constructor.mk_lib_call ~loc (RTL.mk_temporal_name fname) [ lhs ]
let reset_return_referent ~loc =
- Misc.mk_call ~loc (RTL.mk_temporal_name "reset_return") []
+ Constructor.mk_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
- Misc.mk_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs; size ]
+ Constructor.mk_lib_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs; size ]
end
(* }}} *)
@@ -283,7 +283,7 @@ end = struct
Extlib.may_map
(fun (lhs, rhs, flow) ->
let flow, rhs = match flow with
- | Indirect when alloc -> Direct, (Misc.mk_deref ~loc rhs)
+ | Indirect when alloc -> Direct, (Constructor.mk_deref ~loc rhs)
| _ -> flow, rhs
in
let stmt =
@@ -304,7 +304,9 @@ end = struct
| Lval(Var vi, _) -> vi.vname
| _ -> Options.fatal "[Temporal.call_memxxx] not a left-value"
in
- let stmt = Misc.mk_call ~loc (RTL.mk_temporal_name name) args in
+ let stmt =
+ Constructor.mk_lib_call ~loc (RTL.mk_temporal_name name) args
+ in
Env.add_stmt ~before:current_stmt ~post:false env kf stmt
else
env
@@ -318,7 +320,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 = Misc.mk_call ~loc name [] in
+ let stmt = Constructor.mk_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 b87da402318bb6e13171e6734d5e8e77da87756d..4dc449d7fce91d3aec6aa0250f8dc8068b414338 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -135,7 +135,8 @@ let add_cast ~loc ?name env kf ctx strnum t_opt e =
kf
None
new_ty
- (fun v _ -> [ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e ] ])
+ (fun v _ ->
+ [ Constructor.mk_lib_call ~loc ~result:(Cil.var v) fname [ e ] ])
in
e, env
else if Gmp_types.Q.is_t ty || strnum = Str_R then
@@ -297,7 +298,7 @@ and context_insensitive_term_to_exp kf env t =
kf
~name:vname
(Some t)
- (fun _ ev -> [ Misc.mk_call ~loc name [ ev; e ] ])
+ (fun _ ev -> [ Constructor.mk_lib_call ~loc name [ ev; e ] ])
in
e, env, C_number, ""
else if Gmp_types.Q.is_t ty then
@@ -326,7 +327,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 = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
+ let mk_stmts _ e = [ Constructor.mk_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
@@ -363,14 +364,14 @@ and context_insensitive_term_to_exp kf env t =
let mk_stmts _v e =
assert (Gmp_types.Z.is_t ty);
let cond =
- Misc.mk_e_acsl_guard
+ Constructor.mk_runtime_check
(Env.annotation_kind env)
kf
guard
(Logic_const.prel ~loc (Req, t2, zero))
in
Env.add_assert kf cond (Logic_const.prel (Rneq, t2, zero));
- let instr = Misc.mk_call ~loc name [ e; e1; e2 ] in
+ let instr = Constructor.mk_lib_call ~loc name [ e; e1; e2 ] in
[ cond; instr ]
in
let name = Misc.name_of_binop bop in
@@ -481,7 +482,7 @@ and context_insensitive_term_to_exp kf env t =
(Some t)
(Misc.cty (Extlib.the li.l_type))
(fun vi _ ->
- [ Misc.mk_call ~loc ~result:(Cil.var vi) fname args ])
+ [ Constructor.mk_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 =
@@ -610,7 +611,10 @@ and comparison_to_exp
~name
Cil.intType
(fun v _ ->
- [ Misc.mk_call ~loc ~result:(Cil.var v) "__gmpz_cmp" [ e1; e2 ] ])
+ [ Constructor.mk_lib_call ~loc
+ ~result:(Cil.var v)
+ "__gmpz_cmp"
+ [ e1; e2 ] ])
in
Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
| Typing.Rational ->
@@ -850,7 +854,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 Misc.RTE in
+ let env = Env.set_annotation_kind env Constructor.RTE in
let env =
List.fold_left
(fun env a -> match a.annot_content with
@@ -890,7 +894,12 @@ and translate_named_predicate kf env p =
Env.add_stmt
env
kf
- (Misc.mk_e_acsl_guard ~reverse:true (Env.annotation_kind env) kf e p)
+ (Constructor.mk_runtime_check
+ ~reverse:true
+ (Env.annotation_kind env)
+ kf
+ e
+ p)
let named_predicate_to_exp ?name kf env p =
named_predicate_to_exp ?name kf env p (* forget optional argument ?rte *)
@@ -958,7 +967,7 @@ let assumes_predicate bhv =
bhv.b_assumes
let translate_preconditions kf env behaviors =
- let env = Env.set_annotation_kind env Misc.Precondition in
+ let env = Env.set_annotation_kind env Constructor.Precondition in
let do_behavior env b =
let assumes_pred = assumes_predicate b in
List.fold_left
@@ -983,7 +992,7 @@ let translate_preconditions kf env behaviors =
List.fold_left do_behavior env behaviors
let translate_postconditions kf env behaviors =
- let env = Env.set_annotation_kind env Misc.Postcondition in
+ let env = Env.set_annotation_kind env Constructor.Postcondition in
(* generate one guard by postcondition of each behavior *)
let do_behavior env b =
let env =
@@ -1077,25 +1086,25 @@ let translate_pre_code_annotation kf env annot =
let convert env = match annot.annot_content with
| AAssert(l, _, p) ->
if Keep_status.must_translate kf Keep_status.K_Assert then
- let env = Env.set_annotation_kind env Misc.Assertion in
- if l <> [] then
- not_yet env "@[assertion applied only on some behaviors@]";
- translate_named_predicate kf env p
+ let env = Env.set_annotation_kind env Constructor.Assertion in
+ if l <> [] then
+ not_yet env "@[assertion applied only on some behaviors@]";
+ translate_named_predicate kf env p
else
- env
+ env
| AStmtSpec(l, spec) ->
if l <> [] then
not_yet env "@[statement contract applied only on some behaviors@]";
translate_pre_spec kf env spec ;
| AInvariant(l, loop_invariant, p) ->
if Keep_status.must_translate kf Keep_status.K_Invariant then
- let env = Env.set_annotation_kind env Misc.Invariant in
- if l <> [] then
- not_yet env "@[invariant applied only on some behaviors@]";
- let env = translate_named_predicate kf env p in
- if loop_invariant then Env.add_loop_invariant env p else env
+ let env = Env.set_annotation_kind env Constructor.Invariant in
+ if l <> [] then
+ not_yet env "@[invariant applied only on some behaviors@]";
+ let env = translate_named_predicate kf env p in
+ if loop_invariant then Env.add_loop_invariant env p else env
else
- env
+ env
| AVariant _ ->
if Keep_status.must_translate kf Keep_status.K_Variant
then not_yet env "variant"
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 876b77dd686dc3be39d54280b1705db5e5ea5ce5..cbc9e16e284ace3ea2b3c1ae17346bc18689a2a2 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -60,78 +60,6 @@ let get_lib_fun_vi fname =
used as a library *)
raise (Unregistered_library_function fname)
-let mk_call ~loc ?result fname args =
- let vi = get_lib_fun_vi fname in
- let f = Cil.evar ~loc vi in
- vi.vreferenced <- true;
- let make_args args ty_params =
- List.map2
- (fun (_, ty, _) arg ->
- let e =
- match ty, Cil.unrollType (Cil.typeOf arg), arg.enode with
- | TPtr _, TArray _, Lval lv -> Cil.new_exp ~loc (StartOf lv)
- | TPtr _, TArray _, _ -> assert false
- | _, _, _ -> arg
- in
- Cil.mkCast ~force:false ~newt:ty ~e)
- ty_params
- args
- in
- let args = match vi.vtype with
- | TFun(_, Some params, _, _) -> make_args args params
- | TFun(_, None, _, _) -> []
- | _ -> assert false
- in
- Cil.mkStmtOneInstr ~valid_sid:true (Call(result, f, args, loc))
-
-let mk_deref ~loc lv =
- Cil.new_exp ~loc (Lval(Mem(lv), NoOffset))
-
-type annotation_kind =
- | Assertion
- | Precondition
- | Postcondition
- | Invariant
- | RTE
-
-let kind_to_string loc k =
- Cil.mkString
- ~loc
- (match k with
- | Assertion -> "Assertion"
- | Precondition -> "Precondition"
- | Postcondition -> "Postcondition"
- | Invariant -> "Invariant"
- | RTE -> "RTE")
-
-(* Build a C conditional doing a runtime assertion check. *)
-let mk_e_acsl_guard ?(reverse=false) kind kf e p =
- let loc = p.pred_loc in
- let msg =
- Kernel.Unicode.without_unicode
- (Format.asprintf "%a@?" Printer.pp_predicate) p
- in
- let line = (fst loc).Filepath.pos_lnum in
- let e =
- if reverse then e else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
- in
- mk_call
- ~loc
- (RTL.mk_api_name "assert")
- [ e;
- kind_to_string loc kind;
- Cil.mkString ~loc (RTL.get_original_name kf);
- Cil.mkString ~loc msg;
- Cil.integer loc line ]
-
-let mk_block stmt b = match b.bstmts with
- | [] ->
- (match stmt.skind with
- | Instr(Skip _) -> stmt
- | _ -> assert false)
- | [ s ] -> s
- | _ :: _ -> Cil.mkStmt ~valid_sid:true (Block b)
-
(* ************************************************************************** *)
(** {2 Handling \result} *)
(* ************************************************************************** *)
@@ -149,55 +77,6 @@ let result_vi kf = match result_lhost kf with
| Var vi -> vi
| Mem _ -> assert false
-(* ************************************************************************** *)
-(** {2 Handling the E-ACSL's C-libraries, part II} *)
-(* ************************************************************************** *)
-
-let mk_full_init_stmt ?(addr=true) vi =
- let loc = vi.vdecl in
- let mk = mk_call ~loc (RTL.mk_api_name "full_init") in
- match addr, Cil.unrollType vi.vtype with
- | _, TArray(_,Some _, _, _) | false, _ -> mk [ Cil.evar ~loc vi ]
- | _ -> mk [ Cil.mkAddrOfVi vi ]
-
-let mk_initialize ~loc (host, offset as lv) = match host, offset with
- | Var _, NoOffset -> mk_call ~loc
- (RTL.mk_api_name "full_init")
- [ Cil.mkAddrOf ~loc lv ]
- | _ ->
- let typ = Cil.typeOfLval lv in
- mk_call ~loc
- (RTL.mk_api_name "initialize")
- [ Cil.mkAddrOf ~loc lv; Cil.new_exp loc (SizeOf typ) ]
-
-let mk_named_store_stmt name ?str_size vi =
- let ty = Cil.unrollType vi.vtype in
- let loc = vi.vdecl in
- let store = mk_call ~loc (RTL.mk_api_name name) in
- match ty, str_size with
- | TArray(_, Some _,_,_), None ->
- store [ Cil.evar ~loc vi ; Cil.sizeOf ~loc ty ]
- | TPtr(TInt(IChar, _), _), Some size -> store [ Cil.evar ~loc vi ; size ]
- | _, None -> store [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
- | _, Some _ -> assert false
-
-let mk_store_stmt ?str_size vi =
- mk_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 mk_delete_stmt vi =
- let loc = vi.vdecl in
- let mk = mk_call ~loc (RTL.mk_api_name "delete_block") in
- match Cil.unrollType vi.vtype with
- | TArray(_, Some _, _, _) -> mk [ Cil.evar ~loc vi ]
- | _ -> mk [ Cil.mkAddrOfVi vi ]
-
-let mk_mark_readonly vi =
- let loc = vi.vdecl in
- mk_call ~loc (RTL.mk_api_name "mark_readonly") [ Cil.evar ~loc vi ]
-
(* ************************************************************************** *)
(** {2 Other stuff} *)
(* ************************************************************************** *)
@@ -336,6 +215,6 @@ let name_of_binop = function
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index fb335a7e8927a67ed1eaa3b009f7f8407f45b4a5..c1dafb633c93cd4db90b15f161772c00b4c35f29 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -23,7 +23,6 @@
(** Utilities for E-ACSL. *)
open Cil_types
-open Cil_datatype
(* ************************************************************************** *)
(** {2 Builders} *)
@@ -33,28 +32,6 @@ exception Unregistered_library_function of string
val get_lib_fun_vi: string -> varinfo
(** Return varinfo corresponding to a name of a given library function *)
-val mk_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
-(** Call an E-ACSL library function or an E-ACSL built-in.
- @raise Unregistered_library_function if the given string does not represent
- such a function or if these functions were never registered (only possible
- when using E-ACSL through its API. *)
-
-val mk_deref: loc:Location.t -> exp -> exp
-(** Make a dereference of an expression *)
-
-type annotation_kind =
- | Assertion
- | Precondition
- | Postcondition
- | Invariant
- | RTE
-
-val mk_e_acsl_guard:
- ?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate
- -> stmt
-
-val mk_block: stmt -> block -> stmt
-
(* ************************************************************************** *)
(** {2 Handling \result} *)
(* ************************************************************************** *)
@@ -74,13 +51,6 @@ val is_library_loc: location -> bool
val register_library_function: varinfo -> unit
val reset: unit -> unit
-val mk_store_stmt: ?str_size:exp -> varinfo -> stmt
-val mk_duplicate_store_stmt: ?str_size:exp -> varinfo -> stmt
-val mk_delete_stmt: varinfo -> stmt
-val mk_full_init_stmt: ?addr:bool -> varinfo -> stmt
-val mk_initialize: loc:location -> lval -> stmt
-val mk_mark_readonly: varinfo -> stmt
-
(* ************************************************************************** *)
(** {2 Other stuff} *)
(* ************************************************************************** *)
@@ -132,6 +102,6 @@ val finite_min_and_max: Ival.t -> Integer.t * Integer.t
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)