diff --git a/.Makefile.lint b/.Makefile.lint
index 80fb691a8370490eea2a7db9b60c1fae64ab498a..06c49f05b54e16d5f35a24cb731e80fef8f5784f 100644
--- a/.Makefile.lint
+++ b/.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
-
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/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index caec156e2bce6ce838c1bb9d1c4957685e808264..541d6252e8d8b64cc742d235bc164582829e1afc 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/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
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/analyses/mmodel_analysis.ml b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
index c480e318b764410dc8acfd272b8c28d27d3f75f6..db85a8c4c96a1d183f0b84ae424531901996fb3d 100644
--- a/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
+++ b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
@@ -138,11 +138,11 @@ end = struct
try
Kernel_function.Hashtbl.iter
(fun _ h ->
- Stmt.Hashtbl.iter
- (fun _ set -> match set with
- | None -> ()
- | Some s -> if not (Varinfo.Hptset.is_empty s) then raise Exit)
- h)
+ Stmt.Hashtbl.iter
+ (fun _ set -> match set with
+ | None -> ()
+ | Some s -> if not (Varinfo.Hptset.is_empty s) then raise Exit)
+ h)
tbl;
true
with Exit ->
@@ -162,7 +162,7 @@ let reset () =
module rec Transfer
: Dataflow.BackwardsTransfer with type t = Varinfo.Hptset.t option
- = struct
+= struct
let name = "E_ACSL.Pre_analysis"
@@ -217,8 +217,8 @@ module rec Transfer
let rec base_addr_node = function
| Lval lv | AddrOf lv | StartOf lv ->
(match lv with
- | Var vi, _ -> Some vi
- | Mem e, _ -> base_addr e)
+ | Var vi, _ -> Some vi
+ | Mem e, _ -> base_addr e)
| BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
if is_ptr_or_array_exp e1 then base_addr e1
else begin
@@ -227,7 +227,7 @@ module rec Transfer
end
| Info(e, _) | CastE(_, e) -> base_addr e
| BinOp((MinusPP | PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt
- | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr),
+ | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr),
_, _, _)
| UnOp _ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _
| AlignOfE _ ->
@@ -314,20 +314,20 @@ module rec Transfer
register_term kf varinfos t2
| TBinOp((PlusPI | IndexPI | MinusPI), t1, t2) ->
(match t1.term_type with
- | Ctype ty when is_ptr_or_array ty -> register_term kf varinfos t1
- | _ ->
- match t2.term_type with
- | Ctype ty when is_ptr_or_array ty -> register_term kf varinfos t2
- | _ ->
- if Misc.is_set_of_ptr_or_array t1.term_type ||
- Misc.is_set_of_ptr_or_array t2.term_type then
- (* Occurs for example from:
- \valid(&multi_dynamic[2..4][1..7])
- where multi_dynamic has been dynamically allocated *)
- let varinfos = register_term kf varinfos t1 in
- register_term kf varinfos t2
- else
- assert false)
+ | Ctype ty when is_ptr_or_array ty -> register_term kf varinfos t1
+ | _ ->
+ match t2.term_type with
+ | Ctype ty when is_ptr_or_array ty -> register_term kf varinfos t2
+ | _ ->
+ if Misc.is_set_of_ptr_or_array t1.term_type ||
+ Misc.is_set_of_ptr_or_array t2.term_type then
+ (* Occurs for example from:
+ \valid(&multi_dynamic[2..4][1..7])
+ where multi_dynamic has been dynamically allocated *)
+ let varinfos = register_term kf varinfos t1 in
+ register_term kf varinfos t2
+ else
+ assert false)
| TConst _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
| TAlignOfE _ | Tnull | Ttype _ | TUnOp _ | TBinOp _ ->
varinfos
@@ -359,73 +359,73 @@ module rec Transfer
let register_object kf state_ref = object
inherit Visitor.frama_c_inplace
method !vpredicate_node = function
- | Pvalid(_, t) | Pvalid_read(_, t)
- | Pobject_pointer(_, t) | Pvalid_function t
- | Pinitialized(_, t) | Pfreeable(_, t) ->
- (* Options.feedback "REGISTER %a" Cil.d_term t;*)
- state_ref := register_term kf !state_ref t;
- Cil.DoChildren
- | Pallocable _ -> Error.not_yet "\\allocable"
- | Pfresh _ -> Error.not_yet "\\fresh"
- | Pseparated _ -> Error.not_yet "\\separated"
- | Pdangling _ -> Error.not_yet "\\dangling"
- | Ptrue | Pfalse | Papp _ | Prel _
- | Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _
- | Pforall _ | Pexists _ | Pat _ ->
- Cil.DoChildren
- | Plet(li, _) ->
- if may_alias li then Error.not_yet "let-binding on array or pointer"
- else begin
- state_ref := register_term kf !state_ref (Misc.term_of_li li);
+ | Pvalid(_, t) | Pvalid_read(_, t)
+ | Pobject_pointer(_, t) | Pvalid_function t
+ | Pinitialized(_, t) | Pfreeable(_, t) ->
+ (* Options.feedback "REGISTER %a" Cil.d_term t;*)
+ state_ref := register_term kf !state_ref t;
Cil.DoChildren
- end
+ | Pallocable _ -> Error.not_yet "\\allocable"
+ | Pfresh _ -> Error.not_yet "\\fresh"
+ | Pseparated _ -> Error.not_yet "\\separated"
+ | Pdangling _ -> Error.not_yet "\\dangling"
+ | Ptrue | Pfalse | Papp _ | Prel _
+ | Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _
+ | Pforall _ | Pexists _ | Pat _ ->
+ Cil.DoChildren
+ | Plet(li, _) ->
+ if may_alias li then Error.not_yet "let-binding on array or pointer"
+ else begin
+ state_ref := register_term kf !state_ref (Misc.term_of_li li);
+ Cil.DoChildren
+ end
method !vterm term = match term.term_node with
- | Tbase_addr(_, t) | Toffset(_, t) | Tblock_length(_, t) | Tlet(_, t) ->
- state_ref := register_term kf !state_ref t;
- Cil.DoChildren
- | TConst _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _ | Tnull | Ttype _
- | Tempty_set ->
- (* no left-value inside inside: skip for efficiency *)
- Cil.SkipChildren
- | TUnOp _ | TBinOp _ | Ttypeof _ | TSizeOfE _
- | TLval _ | TAlignOfE _ | TCastE _ | TAddrOf _
- | TStartOf _ | Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _
- | TUpdate _ | Tunion _ | Tinter _
- | Tcomprehension _ | Trange _ | TLogic_coerce _ ->
- (* potential sub-term inside *)
- Cil.DoChildren
+ | Tbase_addr(_, t) | Toffset(_, t) | Tblock_length(_, t) | Tlet(_, t) ->
+ state_ref := register_term kf !state_ref t;
+ Cil.DoChildren
+ | TConst _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _ | Tnull | Ttype _
+ | Tempty_set ->
+ (* no left-value inside inside: skip for efficiency *)
+ Cil.SkipChildren
+ | TUnOp _ | TBinOp _ | Ttypeof _ | TSizeOfE _
+ | TLval _ | TAlignOfE _ | TCastE _ | TAddrOf _
+ | TStartOf _ | Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _
+ | TUpdate _ | Tunion _ | Tinter _
+ | Tcomprehension _ | Trange _ | TLogic_coerce _ ->
+ (* potential sub-term inside *)
+ Cil.DoChildren
method !vlogic_label _ = Cil.SkipChildren
method !vterm_lhost = function
- | TMem t ->
- (* potential RTE *)
- state_ref := register_term kf !state_ref t;
- Cil.DoChildren
- | TVar _ | TResult _ ->
- Cil.SkipChildren
+ | TMem t ->
+ (* potential RTE *)
+ state_ref := register_term kf !state_ref t;
+ Cil.DoChildren
+ | TVar _ | TResult _ ->
+ Cil.SkipChildren
end
-let register_predicate kf pred state =
- let state_ref = ref state in
- Error.handle
- (fun () ->
- ignore
- (Visitor.visitFramacIdPredicate (register_object kf state_ref) pred))
- ();
- !state_ref
+ let register_predicate kf pred state =
+ let state_ref = ref state in
+ Error.handle
+ (fun () ->
+ ignore
+ (Visitor.visitFramacIdPredicate (register_object kf state_ref) pred))
+ ();
+ !state_ref
let register_code_annot kf a state =
let state_ref = ref state in
Error.handle
(fun () ->
- ignore
- (Visitor.visitFramacCodeAnnotation (register_object kf state_ref) a))
+ ignore
+ (Visitor.visitFramacCodeAnnotation (register_object kf state_ref) a))
();
!state_ref
- let rec do_init vi init state = match init with
- | SingleInit e -> handle_assignment state (Var vi, NoOffset) e
- | CompoundInit(_, l) ->
- List.fold_left (fun state (_, init) -> do_init vi init state) state l
+ let rec do_init vi init state = match init with
+ | SingleInit e -> handle_assignment state (Var vi, NoOffset) e
+ | CompoundInit(_, l) ->
+ List.fold_left (fun state (_, init) -> do_init vi init state) state l
let register_initializers state =
let do_one vi init state = match init.init with
@@ -433,9 +433,9 @@ let register_predicate kf pred state =
| Some init -> do_init vi init state
in
Globals.Vars.fold_in_file_rev_order do_one state
-(* below: compatibility with Fluorine *)
-(* let l = Globals.Vars.fold_in_file_order (fun v i l -> (v, i) :: l) [] in
- List.fold_left (fun state (v, i) -> do_one v i state) state l*)
+ (* below: compatibility with Fluorine *)
+ (* let l = Globals.Vars.fold_in_file_order (fun v i l -> (v, i) :: l) [] in
+ List.fold_left (fun state (v, i) -> do_one v i state) state l*)
(** The (backwards) transfer function for a branch. The [(Cil.CurrentLoc.get
())] is set before calling this. If it returns None, then we have some
@@ -447,59 +447,63 @@ let register_predicate kf pred state =
let is_last = Kernel_function.is_return_stmt kf stmt in
Dataflow.Post
(fun state ->
- let state = Env.default_varinfos state in
- let state =
- if Functions.check kf then
- let state =
- if (is_first || is_last) && Functions.RTL.is_generated_kf kf then
- Annotations.fold_behaviors
- (fun _ bhv s ->
- let handle_annot test f s =
- if test then
- f
- (fun _ p s -> register_predicate kf p s)
- kf
- bhv.b_name
+ let state = Env.default_varinfos state in
+ let state =
+ if Functions.check kf then
+ let state =
+ if (is_first || is_last) && Functions.RTL.is_generated_kf kf then
+ Annotations.fold_behaviors
+ (fun _ bhv s ->
+ let handle_annot test f s =
+ if test then
+ f
+ (fun _ p s -> register_predicate kf p s)
+ kf
+ bhv.b_name
+ s
+ else
s
- else
- s
- in
- let s = handle_annot is_first Annotations.fold_requires s in
- let s = handle_annot is_first Annotations.fold_assumes s in
- handle_annot
- is_last
- (fun f ->
- Annotations.fold_ensures (fun e (_, p) -> f e p)) s)
- kf
- state
- else
- state
- in
- let state =
- Annotations.fold_code_annot
- (fun _ -> register_code_annot kf) stmt state
- in
- if stmt.ghost then
- let rtes = Rte.stmt kf stmt in
- List.fold_left
- (fun state a -> register_code_annot kf a state) state rtes
- else
- state
- else (* not (Options.Functions.check kf): do not monitor [kf] *)
- state
- in
- let state =
- (* take initializers into account *)
- if is_first then
- let main, lib = Globals.entry_point () in
- if Kernel_function.equal kf main && not lib then
- register_initializers state
- else
- state
- else
- state
- in
- Some state)
+ in
+ let s =
+ handle_annot is_first Annotations.fold_requires s
+ in
+ let s =
+ handle_annot is_first Annotations.fold_assumes s
+ in
+ handle_annot
+ is_last
+ (fun f ->
+ Annotations.fold_ensures (fun e (_, p) -> f e p)) s)
+ kf
+ state
+ else
+ state
+ in
+ let state =
+ Annotations.fold_code_annot
+ (fun _ -> register_code_annot kf) stmt state
+ in
+ if stmt.ghost then
+ let rtes = Rte.stmt kf stmt in
+ List.fold_left
+ (fun state a -> register_code_annot kf a state) state rtes
+ else
+ state
+ else (* not (Options.Functions.check kf): do not monitor [kf] *)
+ state
+ in
+ let state =
+ (* take initializers into account *)
+ if is_first then
+ let main, lib = Globals.entry_point () in
+ if Kernel_function.equal kf main && not lib then
+ register_initializers state
+ else
+ state
+ else
+ state
+ in
+ Some state)
let do_call res f args state =
let kf = Globals.Functions.get f in
@@ -512,11 +516,11 @@ let register_predicate kf pred state =
let init =
List.fold_left2
(fun acc p a -> match base_addr a with
- | None -> acc
- | Some vi ->
- if Varinfo.Hptset.mem vi state
- then Varinfo.Hptset.add p acc
- else acc)
+ | None -> acc
+ | Some vi ->
+ if Varinfo.Hptset.mem vi state
+ then Varinfo.Hptset.add p acc
+ else acc)
state
params
args
@@ -536,10 +540,10 @@ let register_predicate kf pred state =
corresponding formals must be kept *)
List.fold_left2
(fun acc p a -> match base_addr a with
- | None -> acc
- | Some vi ->
- if Varinfo.Hptset.mem p state then Varinfo.Hptset.add vi acc
- else acc)
+ | None -> acc
+ | Some vi ->
+ if Varinfo.Hptset.mem p state then Varinfo.Hptset.add vi acc
+ else acc)
state
params
args
@@ -589,19 +593,19 @@ let register_predicate kf pred state =
do_call (Some (Cil.var v)) f args state
| Call(result, f_exp, l, _) ->
(match f_exp.enode with
- | Lval(Var vi, NoOffset) -> do_call result vi l state
- | _ ->
- Options.warning ~current:true
- "function pointers may introduce too limited instrumentation.";
-(* imprecise function call: keep each argument *)
- Dataflow.Done
- (Some
- (List.fold_left
- (fun acc e -> match base_addr e with
- | None -> acc
- | Some vi -> Varinfo.Hptset.add vi acc)
- state
- l)))
+ | Lval(Var vi, NoOffset) -> do_call result vi l state
+ | _ ->
+ Options.warning ~current:true
+ "function pointers may introduce too limited instrumentation.";
+ (* imprecise function call: keep each argument *)
+ Dataflow.Done
+ (Some
+ (List.fold_left
+ (fun acc e -> match base_addr e with
+ | None -> acc
+ | Some vi -> Varinfo.Hptset.add vi acc)
+ state
+ l)))
| Asm _ -> Error.not_yet "asm"
| Skip _ | Code_annot _ -> Dataflow.Default
@@ -633,23 +637,25 @@ end = struct
if is_init then
Extlib.may
(fun set ->
- List.iter
- (fun s ->
- let old =
- try Extlib.the (Stmt.Hashtbl.find tbl s)
- with Not_found -> assert false
- in
- Stmt.Hashtbl.replace
- tbl
- s
- (Some (Varinfo.Hptset.union set old)))
- returns)
+ List.iter
+ (fun s ->
+ let old =
+ try Extlib.the (Stmt.Hashtbl.find tbl s)
+ with Not_found -> assert false
+ in
+ Stmt.Hashtbl.replace
+ tbl
+ s
+ (Some (Varinfo.Hptset.union set old)))
+ returns)
init_set
else begin
List.iter (fun s -> Stmt.Hashtbl.add tbl s None) stmts;
Extlib.may
(fun set ->
- List.iter (fun s -> Stmt.Hashtbl.replace tbl s (Some set)) returns)
+ List.iter
+ (fun s -> Stmt.Hashtbl.replace tbl s (Some set))
+ returns)
init_set
end;
D.compute stmts
@@ -665,12 +671,12 @@ end = struct
else
try
let stmt = Kernel_function.find_first_stmt kf in
-(* Options.feedback "GETTING %a" Kernel_function.pretty kf;*)
+ (* Options.feedback "GETTING %a" Kernel_function.pretty kf;*)
let tbl =
if Env.mem_init kf init then
try Env.find kf with Not_found -> assert false
else begin
- (* WARN: potentially incorrect in case of recursive call *)
+ (* WARN: potentially incorrect in case of recursive call *)
Env.add_init kf init;
Env.apply (compute init) kf
end
@@ -691,16 +697,18 @@ let consolidated_must_model_vi vi =
Env.consolidated_mem vi
else begin
Options.feedback ~level:2 "performing pre-analysis for minimal memory \
-instrumentation.";
+ instrumentation.";
(try
let main, _ = Globals.entry_point () in
let set = Compute.get main in
Env.consolidate set
with Globals.No_such_entry_point s ->
- Options.warning ~once:true "%s@ \
-@[The generated program may miss memory instrumentation@ \
-if there are memory-related annotations.@]"
- s);
+ Options.warning
+ ~once:true
+ "%s@ \
+ @[The generated program may miss memory instrumentation@ \
+ if there are memory-related annotations.@]"
+ s);
Options.feedback ~level:2 "pre-analysis done.";
Env.consolidated_mem vi
end
@@ -715,24 +723,24 @@ let must_model_vi ?kf ?stmt vi =
TODO: could be optimized though *)
consolidated_must_model_vi vi
(* match stmt, kf with
- | None, _ -> consolidated_must_model_vi vi
- | Some _, None ->
+ | None, _ -> consolidated_must_model_vi vi
+ | Some _, None ->
assert false
- | Some stmt, Some kf ->
+ | Some stmt, Some kf ->
if not (Env.is_consolidated ()) then
ignore (consolidated_must_model_vi vi);
try
let tbl = Env.find kf in
try
-let set = Stmt.Hashtbl.find tbl stmt in
-Varinfo.Hptset.mem vi (Env.default_varinfos set)
+ let set = Stmt.Hashtbl.find tbl stmt in
+ Varinfo.Hptset.mem vi (Env.default_varinfos set)
with Not_found ->
-(* new statement *)
-consolidated_must_model_vi vi
+ (* new statement *)
+ consolidated_must_model_vi vi
with Not_found ->
(* [kf] is dead code *)
false
- *)
+*)
let rec apply_on_vi_base_from_lval f ?kf ?stmt = function
| Var vi, _ -> f ?kf ?stmt vi
@@ -748,7 +756,7 @@ and apply_on_vi_base_from_exp f ?kf ?stmt e = match e.enode with
|| apply_on_vi_base_from_exp f ?kf ?stmt e2
| Info(e, _) | CastE(_, e) -> apply_on_vi_base_from_exp f ?kf ?stmt e
| BinOp((PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt | Lt | Gt | Le
- | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr), _, _, _)
+ | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr), _, _, _)
| Const _ -> (* possible in case of static address *) false
| UnOp _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
Options.fatal "[pre_analysis] unexpected expression %a" Exp.pretty e
@@ -777,20 +785,20 @@ let must_never_monitor_exp ?kf ?stmt lv =
let must_model_vi ?kf ?stmt vi =
not (must_never_monitor vi)
&&
- (Options.Full_mmodel.get ()
- || Error.generic_handle (must_model_vi ?kf ?stmt) false vi)
+ (Options.Full_mmodel.get ()
+ || Error.generic_handle (must_model_vi ?kf ?stmt) false vi)
let must_model_lval ?kf ?stmt lv =
not (must_never_monitor_lval ?kf ?stmt lv)
&&
- (Options.Full_mmodel.get ()
- || Error.generic_handle (must_model_lval ?kf ?stmt) false lv)
+ (Options.Full_mmodel.get ()
+ || Error.generic_handle (must_model_lval ?kf ?stmt) false lv)
let must_model_exp ?kf ?stmt exp =
not (must_never_monitor_exp ?kf ?stmt exp)
&&
- (Options.Full_mmodel.get ()
- || Error.generic_handle (must_model_exp ?kf ?stmt) false exp)
+ (Options.Full_mmodel.get ()
+ || Error.generic_handle (must_model_exp ?kf ?stmt) false exp)
let use_model () =
not (Env.is_empty ())
diff --git a/src/plugins/e-acsl/src/analyses/rte.ml b/src/plugins/e-acsl/src/analyses/rte.ml
index 96a1afbb988346ccc261a2181d097d949b370c8b..9305eff3a55b06c68106628a229bb27afd265565 100644
--- a/src/plugins/e-acsl/src/analyses/rte.ml
+++ b/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:
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 040c83991edcca505c5758fdf0ad4dea40420c12..671ea306b1f641e8cacba62184345c3256d526fd 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
@@ -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
(*
diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli b/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
index f5b51d739bd4de58a55583a2e68cd2f95696b87e..0a971045fddfe3d0cc9ec1f9a90a6fdf982a46ed 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index e457ac5c2264548399b60b7ed77206f49cd6973e..cfdbe5fdda47bb9b3ea0aab39423b7e26bf8c5c6 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -56,7 +56,7 @@ type local_env = {
type t = {
lscope: Lscope.t;
lscope_reset: bool;
- annotation_kind: Constructor.annotation_kind;
+ annotation_kind: Smart_stmt.annotation_kind;
new_global_vars: (varinfo * localized_scope) list;
(* generated variables. The scope indicates the level where the variable
should be added. *)
@@ -88,7 +88,7 @@ let empty_local_env =
let empty =
{ lscope = Lscope.empty;
lscope_reset = true;
- annotation_kind = Constructor.Assertion;
+ annotation_kind = Smart_stmt.Assertion;
new_global_vars = [];
global_mp_tbl = empty_mp_tbl;
env_stack = [];
@@ -257,7 +257,7 @@ let rtl_call_to_new_var ~loc ?scope ?name env kf t ty func_name args =
t
ty
(fun v _ ->
- [ Constructor.mk_rtl_call ~loc ~result:(Cil.var v) func_name args ])
+ [ Smart_stmt.rtl_call ~loc ~result:(Cil.var v) func_name args ])
in
exp, env
@@ -351,9 +351,9 @@ let add_stmt ?(post=false) ?before env kf stmt =
{ env with env_stack = local_env :: tl }
let extend_stmt_in_place env stmt ~label block =
- let new_stmt = Constructor.mk_block_stmt block in
+ let new_stmt = Smart_stmt.block_stmt block in
let sk = stmt.skind in
- stmt.skind <- Block (Cil.mkBlock [ new_stmt; Constructor.mk_stmt sk ]);
+ stmt.skind <- Block (Cil.mkBlock [ new_stmt; Smart_stmt.stmt sk ]);
let pre = match label with
| BuiltinLabel(Here | Post) -> true
| BuiltinLabel(Old | Pre | LoopEntry | LoopCurrent | Init)
@@ -447,7 +447,7 @@ let pop_and_get ?(split=false) env stmt ~global_clear where =
add the given [stmt] afterwards. This way, we have the guarantee that
the final block does not contain any local, so may be transient. *)
if split then
- let sblock = Constructor.mk_block_stmt b in
+ let sblock = Smart_stmt.block_stmt b in
Cil.transient_block (Cil.mkBlock [ sblock; stmt ])
else
b
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 847b551cacb7222e4efdf9f1448012bcc655496a..94c11335f1c96bbcee2a1def0150be956bb81435 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -148,8 +148,8 @@ end
(** {2 Current annotation kind} *)
(* ************************************************************************** *)
-val annotation_kind: t -> Constructor.annotation_kind
-val set_annotation_kind: t -> Constructor.annotation_kind -> t
+val annotation_kind: t -> Smart_stmt.annotation_kind
+val set_annotation_kind: t -> Smart_stmt.annotation_kind -> t
(* ************************************************************************** *)
(** {2 Loop invariants} *)
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.ml b/src/plugins/e-acsl/src/code_generator/global_observer.ml
index ab1d0ed88db4408e4dd14635e8291350f6666ba8..0e6a3ac2302a17cae489c61671fb46e4f7946ecc 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.ml
@@ -123,8 +123,8 @@ let mk_init_function () =
if Misc.is_fc_or_compiler_builtin vi then stmts
else
(* a global is both allocated and initialized *)
- Constructor.mk_store_stmt vi
- :: Constructor.mk_initialize ~loc:Location.unknown (Cil.var vi)
+ Smart_stmt.store_stmt vi
+ :: Smart_stmt.initialize ~loc:Location.unknown (Cil.var vi)
:: stmts)
tbl
stmts
@@ -136,10 +136,10 @@ let mk_init_function () =
let loc = Location.unknown in
let e = Cil.new_exp ~loc:loc (Const (CStr s)) in
let str_size = Cil.new_exp loc (SizeOfStr s) in
- Constructor.mk_assigns ~loc ~result:(Cil.var vi) e
- :: Constructor.mk_store_stmt ~str_size vi
- :: Constructor.mk_full_init_stmt vi
- :: Constructor.mk_mark_readonly vi
+ Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
+ :: Smart_stmt.store_stmt ~str_size vi
+ :: Smart_stmt.full_init_stmt vi
+ :: Smart_stmt.mark_readonly vi
:: stmts)
stmts
in
@@ -150,7 +150,7 @@ let mk_init_function () =
let b, _env = Env.pop_and_get env stmt ~global_clear:true Env.Before in
b, stmts
in
- let stmts = Constructor.mk_block_stmt b :: stmts in
+ let stmts = Smart_stmt.block_stmt b :: stmts in
(* prevent multiple calls to [__e_acsl_globals_init] *)
let loc = Location.unknown in
let vi_already_run =
@@ -168,14 +168,14 @@ let mk_init_function () =
(Local_init (vi_already_run, init, loc))
in
let already_run =
- Constructor.mk_assigns
+ Smart_stmt.assigns
~loc
~result:(Cil.var vi_already_run)
(Cil.one ~loc)
in
let stmts = already_run :: stmts in
let guard =
- Constructor.mk_if
+ Smart_stmt.if_stmt
~loc
~cond:(Cil.evar vi_already_run)
(Cil.mkBlock [])
@@ -195,7 +195,7 @@ let mk_delete_function () =
Varinfo.Hashtbl.fold_sorted
(fun vi _l acc ->
if Misc.is_fc_or_compiler_builtin vi then acc
- else Constructor.mk_delete_stmt vi :: acc)
+ else Smart_stmt.delete_stmt vi :: acc)
tbl
[]
in
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index 8c28ac5e32e0267754723bd1a0042f492fb6cb17..8a2b5385f1cb1830a92ff5272cb14bd0cd3d7c69 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -33,7 +33,7 @@ let apply_on_var ~loc funname e =
else if Gmp_types.Q.is_t ty then "__gmpq_"
else assert false
in
- Constructor.mk_lib_call ~loc (prefix ^ funname) [ e ]
+ Smart_stmt.lib_call ~loc (prefix ^ funname) [ e ]
let init ~loc e = apply_on_var "init" ~loc e
let clear ~loc e = apply_on_var "clear" ~loc e
@@ -90,9 +90,9 @@ let generic_affect ~loc fname lv ev e =
let ty = Cil.typeOf ev in
if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then begin
let suf, args = get_set_suffix_and_arg ty e in
- Constructor.mk_lib_call ~loc (fname ^ suf) (ev :: args)
+ Smart_stmt.lib_call ~loc (fname ^ suf) (ev :: args)
end else
- Constructor.mk_assigns ~loc:e.eloc ~result:lv e
+ Smart_stmt.assigns ~loc:e.eloc ~result:lv e
let init_set ~loc lv ev e =
let fname =
@@ -111,7 +111,7 @@ let init_set ~loc lv ev e =
| Lval elv ->
assert (Gmp_types.Z.is_t (Cil.typeOf ev));
let call =
- Constructor.mk_lib_call ~loc
+ Smart_stmt.lib_call ~loc
"__gmpz_import"
[ ev;
Cil.one ~loc;
@@ -121,7 +121,7 @@ let init_set ~loc lv ev e =
Cil.zero ~loc;
Cil.mkAddrOf ~loc elv ]
in
- Constructor.mk_block_stmt (Cil.mkBlock [ init ~loc ev; call ])
+ Smart_stmt.block_stmt (Cil.mkBlock [ init ~loc ev; call ])
| _ ->
Error.not_yet "unsigned long long expression requiring GMP")
| Longlong ILongLong ->
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index dd1222051d790f8757da083c9f9628ac3be4d877..cdc6486702d1fbcc234a0f0f7bf19b1f616e74c9 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -60,7 +60,7 @@ let inject_in_local_init loc env kf vi = function
| ConsInit (fvi, sz :: _, _) as init
when Functions.Libc.is_vla_alloc_name fvi.vname ->
(* add a store statement when creating a variable length array *)
- let store = Constructor.mk_store_stmt ~str_size:sz vi in
+ let store = Smart_stmt.store_stmt ~str_size:sz vi in
let env = Env.add_stmt ~post:true env kf store in
init, env
@@ -145,13 +145,13 @@ let add_initializer loc ?vi lv ?(post=false) stmt env kf =
(* bitfields are not yet supported ==> no initializer.
a [not_yet] will be raised in [Translate]. *)
if Cil.isBitfield lv then Cil.mkEmptyStmt ()
- else Constructor.mk_initialize ~loc lv
+ else Smart_stmt.initialize ~loc lv
in
let env = Env.add_stmt ~post ~before env kf new_stmt in
let env = match vi with
| None -> env
| Some vi ->
- let new_stmt = Constructor.mk_store_stmt vi in
+ let new_stmt = Smart_stmt.store_stmt vi in
Env.add_stmt ~post ~before env kf new_stmt
in
env
@@ -189,7 +189,7 @@ let inject_in_instr env kf stmt = function
if Functions.Libc.is_vla_free caller then
match args with
| [ { enode = CastE (_, { enode = Lval (Var vi, NoOffset) }) } ] ->
- let delete_block = Constructor.mk_delete_stmt ~is_addr:true vi in
+ let delete_block = Smart_stmt.delete_stmt ~is_addr:true vi in
Env.add_stmt env kf delete_block
| _ -> Options.fatal "The normalization of __fc_vla_free() has changed"
else
@@ -263,7 +263,7 @@ let add_new_block_in_stmt env kf stmt =
let b, env =
Env.pop_and_get env new_stmt ~global_clear:true Env.After
in
- let new_stmt = Constructor.mk_block stmt b in
+ let new_stmt = Smart_stmt.block stmt b in
if not (Cil_datatype.Stmt.equal stmt new_stmt) then begin
(* move the labels of the return to the new block in order to
evaluate the postcondition when jumping to them. *)
@@ -293,7 +293,7 @@ let add_new_block_in_stmt env kf stmt =
let post_block, env =
Env.pop_and_get
env
- (Constructor.mk_block new_stmt pre_block)
+ (Smart_stmt.block new_stmt pre_block)
~global_clear:false
Env.Before
in
@@ -302,7 +302,7 @@ let add_new_block_in_stmt env kf stmt =
then Cil.transient_block post_block
else post_block
in
- let res = Constructor.mk_block new_stmt post_block in
+ let res = Smart_stmt.block new_stmt post_block in
if not (Cil_datatype.Stmt.equal new_stmt res) then
E_acsl_label.move kf new_stmt res;
res, env
@@ -337,7 +337,7 @@ let insert_as_last_stmts_in_innermost_block ~last_stmts kf outer_block =
match return_stmt with
| Some return_stmt ->
let b = Cil.mkBlock new_stmts in
- let new_stmt = Constructor.mk_block return_stmt b in
+ let new_stmt = Smart_stmt.block return_stmt b in
E_acsl_label.move kf return_stmt new_stmt;
[ new_stmt ]
| None -> new_stmts
@@ -516,7 +516,7 @@ and inject_in_block (env: Env.t) kf blk =
List.fold_left
(fun acc vi ->
if Mmodel_analysis.must_model_vi ~kf vi
- then Constructor.mk_delete_stmt vi :: acc
+ then Smart_stmt.delete_stmt vi :: acc
else acc)
stmts
blk.blocals
@@ -531,7 +531,7 @@ and inject_in_block (env: Env.t) kf blk =
List.fold_left
(fun acc vi ->
if Mmodel_analysis.must_model_vi vi && not vi.vdefined
- then Constructor.mk_store_stmt vi :: acc
+ then Smart_stmt.store_stmt vi :: acc
else acc)
blk.bstmts
blk.blocals;
@@ -821,8 +821,8 @@ let inject_mmodel_handler main =
in
let ptr_size = Cil.sizeOf loc Cil.voidPtrType in
let args = args @ [ ptr_size ] in
- let init = Constructor.mk_rtl_call loc "memory_init" args in
- let clean = Constructor.mk_rtl_call loc "memory_clean" [] in
+ let init = Smart_stmt.rtl_call loc "memory_init" args in
+ let clean = Smart_stmt.rtl_call loc "memory_clean" [] in
surround_function_with main fundec init (Some clean)
in
Extlib.may handle_main main
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml
index af522479dc6c22f7926c9edfee20c28821c1ce1a..08e9eda66c45e2f5e0967f4cd49c3a9340a85703 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_array.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml
@@ -95,7 +95,7 @@ let length_exp ~loc kf env ~name array =
~name
Cil.theMachine.typeOfSizeOf
(fun v _ -> [
- Constructor.mk_assigns
+ Smart_stmt.assigns
~loc
~result:(Cil.var v)
(Cil.mkBinOp
@@ -168,7 +168,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
None
~name
Cil.intType
- (fun v _ -> [ Constructor.mk_assigns ~loc ~result:(Cil.var v) (res_value ()) ])
+ (fun v _ -> [ Smart_stmt.assigns ~loc ~result:(Cil.var v) (res_value ()) ])
in
(* Retrieve the length of the arrays *)
@@ -193,8 +193,8 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
arrays. This env will enable us to also check RTEs *)
let env = Env.push env in
(* Create the access to the arrays *)
- let array1_iter_e = Constructor.mk_subscript ~loc array1 iter_e in
- let array2_iter_e = Constructor.mk_subscript ~loc array2 iter_e in
+ let array1_iter_e = Smart_exp.subscript ~loc array1 iter_e in
+ let array2_iter_e = Smart_exp.subscript ~loc array2 iter_e in
(* Check RTE on the arrays, filtering out bounding checks since the accesses
are built already in bounds *)
let filter a =
@@ -212,12 +212,12 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
let cond = Cil.mkBinOp ~loc Ne array1_iter_e array2_iter_e in
(* Create the statement representing the body of the for loop *)
let body =
- Constructor.mk_if
+ Smart_stmt.if_stmt
~loc
~cond
(Cil.mkBlock [
- Constructor.mk_assigns ~loc ~result:(Cil.var comparison_vi) (res_value ~flip:true ());
- Constructor.mk_break ~loc
+ Smart_stmt.assigns ~loc ~result:(Cil.var comparison_vi) (res_value ~flip:true ());
+ Smart_stmt.break ~loc
])
in
(* Pop the env to build the body of the for loop *)
@@ -225,14 +225,14 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
(* Create the statement representing the full for loop *)
let for_loop =
- (Constructor.mk_block_stmt
+ (Smart_stmt.block_stmt
(Cil.mkBlock
(Cil.mkForIncr
~iter
~first:(Cil.zero ~loc)
~stopat:len1_exp
~incr:(Cil.one ~loc)
- ~body:[ Constructor.mk_block_stmt body_blk ]
+ ~body:[ Smart_stmt.block_stmt body_blk ]
)
)
)
@@ -244,7 +244,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
(* Add the check for the length before the for loop *)
let prepend_coercion_check ~name env stmts array len =
- let array_orig = Option.get (Constructor.extract_uncoerced_lval array) in
+ let array_orig = Option.get (Misc.extract_uncoerced_lval array) in
if array_orig == array then
stmts, env
else
@@ -259,7 +259,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
in
let p = { p with pred_name = "array_coercion" :: p.pred_name } in
let stmt =
- Constructor.mk_runtime_check Constructor.RTE kf e p
+ Smart_stmt.runtime_check Smart_stmt.RTE kf e p
in
stmt :: stmts, env
in
@@ -272,17 +272,17 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
(* Pop the env to build the full then block *)
let then_blk, env =
- pop_and_get_env env (Constructor.mk_block_stmt (Cil.mkBlock then_stmts))
+ pop_and_get_env env (Smart_stmt.block_stmt (Cil.mkBlock then_stmts))
in
(* Create the statement representing the whole generated code *)
let stmt =
- Constructor.mk_if
+ Smart_stmt.if_stmt
~loc
~cond:(Cil.mkBinOp ~loc Eq len1_exp len2_exp)
then_blk
~else_blk:(Cil.mkBlock
- [ Constructor.mk_assigns
+ [ Smart_stmt.assigns
~loc
~result:(Cil.var comparison_vi)
(res_value ~flip:true ()) ])
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index d5bf1c4da99b052ef55ba976adb9eba5c4929ff7..97c6523575a25720e3316e1fd0a532bf7331894a 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -98,7 +98,7 @@ let term_to_block ~loc kf env ret_ty ret_vi t =
function (by reference). *)
let set =
let lv_star_ret = Cil.mkMem ~addr:(Cil.evar ~loc ret_vi) ~off:NoOffset in
- let star_ret = Constructor.mk_lval ~loc lv_star_ret in
+ let star_ret = Smart_exp.lval ~loc lv_star_ret in
Gmp.init_set ~loc lv_star_ret star_ret e
in
let return_void = Cil.mkStmt ~valid_sid:true (Return (None, loc)) in
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index bca60ec4f2cd8197f440f38a15241dd03c70761e..c8a5f714ddc2b23fab8a20edded2bd7ea2b6d663 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -59,11 +59,11 @@ let preserve_invariant env kf stmt = match stmt.skind with
let blk, env =
Env.pop_and_get env last ~global_clear:false Env.Before
in
- Constructor.mk_block last blk :: stmts, env
+ Smart_stmt.block last blk :: stmts, env
| s :: tl ->
handle_invariants (s :: stmts, env) tl
in
- let env = Env.set_annotation_kind env Constructor.Invariant in
+ let env = Env.set_annotation_kind env Smart_stmt.Invariant in
let stmts, env = handle_invariants ([], env) stmts in
let new_blk = { blk with bstmts = List.rev stmts } in
{ stmt with skind = Loop([], new_blk, loc, cont, break) },
@@ -212,7 +212,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
Env.Middle
in
(* generate the guard [x bop t2] *)
- let block_to_stmt b = Constructor.mk_block_stmt b in
+ let block_to_stmt b = Smart_stmt.block_stmt b in
let tlv = Logic_const.tvar ~loc logic_x in
let guard =
(* must copy [t2] to force being typed again *)
@@ -221,10 +221,10 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
in
Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
let guard_exp, env = term_to_exp kf (Env.push env) guard in
- let break_stmt = Constructor.mk_break ~loc:guard_exp.eloc in
+ let break_stmt = Smart_stmt.break ~loc:guard_exp.eloc in
let guard_blk, env = Env.pop_and_get
env
- (Constructor.mk_if
+ (Smart_stmt.if_stmt
~loc:guard_exp.eloc
~cond:guard_exp
(mkBlock [ mkEmptyStmt ~loc () ])
@@ -251,10 +251,10 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
| Some p ->
let e, env = !named_predicate_ref kf (Env.push env) p in
let stmt, env =
- Constructor.mk_runtime_check Constructor.RTE kf e p, env
+ Smart_stmt.runtime_check Smart_stmt.RTE kf e p, env
in
let b, env = Env.pop_and_get env stmt ~global_clear:false Env.After in
- let guard_for_small_type = Constructor.mk_block_stmt b in
+ let guard_for_small_type = Smart_stmt.block_stmt b in
guard_for_small_type :: guard :: body @ [ next ], env
in
let start = block_to_stmt init_blk in
diff --git a/src/plugins/e-acsl/src/code_generator/memory_observer.ml b/src/plugins/e-acsl/src/code_generator/memory_observer.ml
index 0ec5cda04ef5f39be1210766ebaca866b748dd37..629e30432278b7a6912f33453939a7476c31632e 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_observer.ml
@@ -39,7 +39,7 @@ let store ?before env kf vars =
tracking_stmt
?before
List.fold_right (* small list *)
- Constructor.mk_store_stmt
+ Smart_stmt.store_stmt
env
kf
vars
@@ -48,7 +48,7 @@ let duplicate_store ?before env kf vars =
tracking_stmt
?before
Varinfo.Set.fold
- Constructor.mk_duplicate_store_stmt
+ Smart_stmt.duplicate_store_stmt
env
kf
vars
@@ -57,7 +57,7 @@ let delete_from_list ?before env kf vars =
tracking_stmt
?before
List.fold_right (* small list *)
- Constructor.mk_delete_stmt
+ Smart_stmt.delete_stmt
env
kf
vars
@@ -66,7 +66,7 @@ let delete_from_set ?before env kf vars =
tracking_stmt
?before
Varinfo.Set.fold
- Constructor.mk_delete_stmt
+ Smart_stmt.delete_stmt
env
kf
vars
diff --git a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
index f5cae16eb0bdb82fc8330038a5c218c6c79f50f7..654433624a3147fc868f052b6d16ab13c9adfaa1 100644
--- a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
@@ -155,8 +155,8 @@ let gmp_to_sizet ~loc kf env size p =
None
sizet
(fun vi _ ->
- [ Constructor.mk_runtime_check Constructor.RTE kf guard p;
- Constructor.mk_lib_call ~loc
+ [ Smart_stmt.runtime_check Smart_stmt.RTE kf guard p;
+ Smart_stmt.lib_call ~loc
~result:(Cil.var vi)
"__gmpz_get_ui"
[ size ] ])
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index b6114f25cd132102a8ccd4e606ca1ad303c2047a..b32d939f05d87cf39e1b798480a59e53a44b6d52 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -174,7 +174,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
intType
(fun v _ ->
let lv = var v in
- [ Constructor.mk_assigns ~loc ~result:lv init_val ])
+ [ Smart_stmt.assigns ~loc ~result:lv init_val ])
in
let end_loop_ref = ref dummyStmt in
(* innermost block *)
@@ -188,23 +188,23 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
(* use a 'goto', not a simple 'break' in order to handle 'forall' with
multiple binders (leading to imbricated loops) *)
mkBlock
- [ Constructor.mk_assigns ~loc ~result:(var var_res) found_val;
+ [ Smart_stmt.assigns ~loc ~result:(var var_res) found_val;
mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ]
in
let blk, env = Env.pop_and_get
env
- (Constructor.mk_if ~loc ~cond:(mk_guard test) then_blk ~else_blk)
+ (Smart_stmt.if_stmt ~loc ~cond:(mk_guard test) then_blk ~else_blk)
~global_clear:false
Env.After
in
let blk = Cil.flatten_transient_sub_blocks blk in
- [ Constructor.mk_block_stmt blk ], env
+ [ Smart_stmt.block_stmt blk ], env
in
let stmts, env =
Loops.mk_nested_loops ~loc mk_innermost_block kf env lvs_guards
in
let env =
- Env.add_stmt env kf (Constructor.mk_block_stmt (mkBlock stmts))
+ Env.add_stmt env kf (Smart_stmt.block_stmt (mkBlock stmts))
in
(* where to jump to go out of the loop *)
let end_loop = mkEmptyStmt ~loc () in
diff --git a/src/plugins/e-acsl/src/code_generator/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
index 3a0da53951b3b4f569e7f55bc2ea3d4849e1fcc4..2f4417b0191213b6730879074147a5f66f68fe43 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -24,7 +24,7 @@ open Cil_types
(* No init_set for GMPQ: init then set separately *)
let init_set ~loc lval vi_e e =
- Constructor.mk_block_stmt
+ Smart_stmt.block_stmt
(Cil.mkBlock
[ Gmp.init ~loc vi_e ;
Gmp.affect ~loc lval vi_e e ])
@@ -148,7 +148,7 @@ let add_cast ~loc ?name e env kf ty =
None
Cil.doubleType
(fun v _ ->
- [ Constructor.mk_lib_call ~loc
+ [ Smart_stmt.lib_call ~loc
~result:(Cil.var v)
"__gmpq_get_d"
[ e ] ])
@@ -197,7 +197,7 @@ let cmp ~loc bop e1 e2 env kf t_opt =
~name
Cil.intType
(fun v _ ->
- [ Constructor.mk_lib_call ~loc ~result:(Cil.var v) fname [ e1; e2 ] ])
+ [ Smart_stmt.lib_call ~loc ~result:(Cil.var v) fname [ e1; e2 ] ])
in
Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
@@ -226,7 +226,7 @@ let binop ~loc bop e1 e2 env kf t_opt =
[e2] *)
let e1, env = create ~loc e1 env kf None in
let e2, env = create ~loc e2 env kf None in
- let mk_stmts _ e = [ Constructor.mk_lib_call ~loc name [ e; e1; e2 ] ] in
+ let mk_stmts _ e = [ Smart_stmt.lib_call ~loc name [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
let _, e, env = new_var_and_init ~loc ~name env kf t_opt mk_stmts in
e, env
diff --git a/src/plugins/e-acsl/src/code_generator/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/code_generator/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml
index a2694969cc618f039f6314f651099618e8985184..96f5c22ee29764fd99bded8ea64abf265fabb0d0 100644
--- a/src/plugins/e-acsl/src/code_generator/temporal.ml
+++ b/src/plugins/e-acsl/src/code_generator/temporal.ml
@@ -51,9 +51,9 @@ type flow =
module Mk: sig
(* Generate either
- - [store_nblock(lhs, rhs)], or
- - [store_nreferent(lhs, rhs)]
- function call based on the value of [flow] *)
+ - [store_nblock(lhs, rhs)], or
+ - [store_nreferent(lhs, rhs)]
+ function call based on the value of [flow] *)
val store_reference: loc:location -> flow -> lval -> exp -> stmt
(* Generate a [save_*_parameter] call *)
@@ -81,7 +81,7 @@ end = struct
| Copy -> Options.fatal "Copy flow type in store_reference"
in
let fname = RTL.mk_temporal_name fname in
- Constructor.mk_lib_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs ]
+ Smart_stmt.lib_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs ]
let save_param ~loc flow lhs pos =
let infix = match flow with
@@ -91,13 +91,13 @@ end = struct
in
let fname = "save_" ^ infix ^ "_parameter" in
let fname = RTL.mk_temporal_name fname in
- Constructor.mk_lib_call ~loc fname [ lhs ; Cil.integer ~loc pos ]
+ Smart_stmt.lib_call ~loc fname [ lhs ; Cil.integer ~loc pos ]
let pull_param ~loc vi pos =
let exp = Cil.mkAddrOfVi vi in
let fname = RTL.mk_temporal_name "pull_parameter" in
let sz = Cil.kinteger ~loc IULong (Cil.bytesSizeOf vi.vtype) in
- Constructor.mk_lib_call ~loc fname [ exp ; Cil.integer ~loc pos ; sz ]
+ Smart_stmt.lib_call ~loc fname [ exp ; Cil.integer ~loc pos ; sz ]
let handle_return_referent ~save ~loc lhs =
let fname = match save with
@@ -106,17 +106,17 @@ end = struct
in
(* TODO: Returning structs is unsupported so far *)
(match (Cil.typeOf lhs) with
- | TPtr _ -> ()
- | _ -> Error.not_yet "Struct in return");
- Constructor.mk_lib_call ~loc (RTL.mk_temporal_name fname) [ lhs ]
+ | TPtr _ -> ()
+ | _ -> Error.not_yet "Struct in return");
+ Smart_stmt.lib_call ~loc (RTL.mk_temporal_name fname) [ lhs ]
let reset_return_referent ~loc =
- Constructor.mk_lib_call ~loc (RTL.mk_temporal_name "reset_return") []
+ Smart_stmt.lib_call ~loc (RTL.mk_temporal_name "reset_return") []
let temporal_memcpy_struct ~loc lhs rhs =
let fname = RTL.mk_temporal_name "memcpy" in
let size = Cil.sizeOf ~loc (Cil.typeOfLval lhs) in
- Constructor.mk_lib_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs; size ]
+ Smart_stmt.lib_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs; size ]
end
(* }}} *)
@@ -125,10 +125,10 @@ end
(* ************************************************************************** *)
(* Given an lvalue [lhs] representing LHS of an assignment, and an expression
- [rhs] representing its RHS compute triple (l,r,f), such that:
+ [rhs] representing its RHS compute triple (l,r,f), such that:
- lval [l] and exp [r] are addresses of a pointer and a memory block, and
- flow [f] indicates how to update the meta-data of [l] using information
- stored by [r]. The values of [f] indicate the following
+ stored by [r]. The values of [f] indicate the following
+ Direct - referent number of [l] is assigned the referent number of [r]
+ Indirect - referent number of [l] is assigned the origin number of [r]
+ Copy - metadata of [r] is copied to metadata of [l] *)
@@ -145,51 +145,52 @@ let assign ?(ltype) lhs rhs loc =
let base, _ = Misc.ptr_index rhs in
let rhs, flow =
(match base.enode with
- | AddrOf _
- | StartOf _ -> rhs, Direct
- (* Unary operator describes !, ~ or -: treat it same as Const since
- it implies integer or logical operations. This case is rare but
- happens: for instance in Gap SPEC CPU benchmark the returned pointer
- is assigned -1 (for whatever bizarre reason) *)
- | Const _ | UnOp _ -> base, Direct
- (* Special case for literal strings which E-ACSL rewrites into
- global variables: take the origin number of a string *)
- | Lval(Var vi, _) when RTL.is_generated_name vi.vname ->
- base, Direct
- (* Lvalue of a pointer type can be a cast of an integral type, for
- instance for the case when address is taken by value (shown via the
- following example).
- uintptr_t addr = ...;
- char *p = (char* )addr;
- If this is the case then the analysis takes the value of a variable. *)
- | Lval lv ->
- if Cil.isPointerType (Cil.unrollType (Cil.typeOfLval lv)) then
- Cil.mkAddrOf ~loc lv, Indirect
- else
- rhs, Direct
- (* Binary operation which yields an integer (or FP) type.
- Since LHS is of pointer type we assume that the whole integer
- expression computes to an address for which there is no
- outer container, so the only thing to do is to take origin number *)
- | BinOp(op, _, _, _) ->
- (* At this point [ptr_index] should have split pointer arithmetic into
- base pointer and index so there should be no pointer arithmetic
- operations there. The following bit is to make sure of it. *)
- (match op with
+ | AddrOf _
+ | StartOf _ -> rhs, Direct
+ (* Unary operator describes !, ~ or -: treat it same as Const since
+ it implies integer or logical operations. This case is rare but
+ happens: for instance in Gap SPEC CPU benchmark the returned pointer
+ is assigned -1 (for whatever bizarre reason) *)
+ | Const _ | UnOp _ -> base, Direct
+ (* Special case for literal strings which E-ACSL rewrites into
+ global variables: take the origin number of a string *)
+ | Lval(Var vi, _) when RTL.is_generated_name vi.vname ->
+ base, Direct
+ (* Lvalue of a pointer type can be a cast of an integral type, for
+ instance for the case when address is taken by value (shown via the
+ following example).
+ uintptr_t addr = ...;
+ char *p = (char* )addr;
+ If this is the case then the analysis takes the value of a variable.
+ *)
+ | Lval lv ->
+ if Cil.isPointerType (Cil.unrollType (Cil.typeOfLval lv)) then
+ Cil.mkAddrOf ~loc lv, Indirect
+ else
+ rhs, Direct
+ (* Binary operation which yields an integer (or FP) type.
+ Since LHS is of pointer type we assume that the whole integer
+ expression computes to an address for which there is no
+ outer container, so the only thing to do is to take origin number *)
+ | BinOp(op, _, _, _) ->
+ (* At this point [ptr_index] should have split pointer arithmetic into
+ base pointer and index so there should be no pointer arithmetic
+ operations there. The following bit is to make sure of it. *)
+ (match op with
| MinusPI | PlusPI | IndexPI -> assert false
| _ -> ());
- base, Direct
- | _ -> assert false)
+ base, Direct
+ | _ -> assert false)
in Some (lhs, rhs, flow)
| TNamed _ -> assert false
| TInt _ | TFloat _ | TEnum _ -> None
| TComp _ ->
let rhs = match rhs.enode with
- | AddrOf _ -> rhs
- | Lval lv -> Cil.mkAddrOf ~loc lv
- | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
- | UnOp _ | BinOp _ | CastE _ | StartOf _ | Info _ ->
- Options.abort "unsupported RHS %a" Printer.pp_exp rhs
+ | AddrOf _ -> rhs
+ | Lval lv -> Cil.mkAddrOf ~loc lv
+ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
+ | UnOp _ | BinOp _ | CastE _ | StartOf _ | Info _ ->
+ Options.abort "unsupported RHS %a" Printer.pp_exp rhs
in Some (lhs, rhs, Copy)
(* va_list is a builtin type, we assume it has no pointers here and treat
it as a "big" integer rather than a struct *)
@@ -240,29 +241,29 @@ end = struct
structure so they can be retrieved once that function is called *)
let save_params current_stmt loc args env kf =
let (env, _) = List.fold_left
- (fun (env, index) param ->
- let lv = Mem(param), NoOffset in
- let ltype = Cil.typeOf param in
- let vals = assign ~ltype lv param loc in
- Extlib.may_map
- (fun (_, rhs, flow) ->
- let env =
- if Mmodel_analysis.must_model_exp ~kf param then
- let stmt = Mk.save_param ~loc flow rhs index in
- Env.add_stmt ~before:current_stmt ~post:false env kf stmt
- else env
- in
- (env, index+1))
- ~dft:(env, index+1)
- vals)
- (env, 0)
- args
+ (fun (env, index) param ->
+ let lv = Mem(param), NoOffset in
+ let ltype = Cil.typeOf param in
+ let vals = assign ~ltype lv param loc in
+ Extlib.may_map
+ (fun (_, rhs, flow) ->
+ let env =
+ if Mmodel_analysis.must_model_exp ~kf param then
+ let stmt = Mk.save_param ~loc flow rhs index in
+ Env.add_stmt ~before:current_stmt ~post:false env kf stmt
+ else env
+ in
+ (env, index+1))
+ ~dft:(env, index+1)
+ vals)
+ (env, 0)
+ args
in env
(* Update local environment with a statement tracking temporal metadata
associated with assignment [ret] = [func(args)]. *)
let call_with_ret ?(alloc=false) current_stmt loc ret env kf =
- let rhs = Constructor.mk_lval ~loc ret in
+ let rhs = Smart_exp.lval ~loc ret in
let vals = assign ret rhs loc in
(* Track referent numbers of assignments via function calls.
Library functions (i.e., with no source code available) that return
@@ -282,17 +283,17 @@ end = struct
[pull_return] added via a call to [Mk.handle_return_referent] *)
Extlib.may_map
(fun (lhs, rhs, flow) ->
- let flow, rhs = match flow with
- | Indirect when alloc -> Direct, (Constructor.mk_deref ~loc rhs)
- | _ -> flow, rhs
- in
- let stmt =
- if alloc then
- Mk.store_reference ~loc flow lhs rhs
- else
- Mk.handle_return_referent ~save:false ~loc (Cil.mkAddrOf ~loc lhs)
- in
- Env.add_stmt ~before:current_stmt ~post:true env kf stmt)
+ let flow, rhs = match flow with
+ | Indirect when alloc -> Direct, (Smart_exp.deref ~loc rhs)
+ | _ -> flow, rhs
+ in
+ let stmt =
+ if alloc then
+ Mk.store_reference ~loc flow lhs rhs
+ else
+ Mk.handle_return_referent ~save:false ~loc (Cil.mkAddrOf ~loc lhs)
+ in
+ Env.add_stmt ~before:current_stmt ~post:true env kf stmt)
~dft:env
vals
@@ -305,7 +306,7 @@ end = struct
| _ -> Options.fatal "[Temporal.call_memxxx] not a left-value"
in
let stmt =
- Constructor.mk_lib_call ~loc (RTL.mk_temporal_name name) args
+ Smart_stmt.lib_call ~loc (RTL.mk_temporal_name name) args
in
Env.add_stmt ~before:current_stmt ~post:false env kf stmt
else
@@ -320,7 +321,7 @@ end = struct
the implementation of the function should be empty and compiler should
be able to optimize that code out. *)
let name = (RTL.mk_temporal_name "reset_parameters") in
- let stmt = Constructor.mk_lib_call ~loc name [] in
+ let stmt = Smart_stmt.lib_call ~loc name [] in
let env = Env.add_stmt ~before:current_stmt ~post:false env kf stmt in
let stmt = Mk.reset_return_referent ~loc in
let env = Env.add_stmt ~before:current_stmt ~post:false env kf stmt in
@@ -340,9 +341,9 @@ end = struct
let alloc = not has_def in
Extlib.may_map
(fun lhs ->
- if Mmodel_analysis.must_model_lval ~kf lhs then
- call_with_ret ~alloc current_stmt loc lhs env kf
- else env)
+ if Mmodel_analysis.must_model_lval ~kf lhs then
+ call_with_ret ~alloc current_stmt loc lhs env kf
+ else env)
~dft:env
ret
end
@@ -465,15 +466,15 @@ let mk_global_init ~loc vi off init =
corresponding variable which that literal string has been converted to *)
let exp =
try let rec get_string e = match e.enode with
- | Const(CStr str) -> str
- | CastE(_, exp) -> get_string exp
- | _ -> raise Not_found
- in
- let str = get_string exp in
- Cil.evar ~loc (Literal_strings.find str)
- with
+ | Const(CStr str) -> str
+ | CastE(_, exp) -> get_string exp
+ | _ -> raise Not_found
+ in
+ let str = get_string exp in
+ Cil.evar ~loc (Literal_strings.find str)
+ with
(* Not a literal string: just use the expression at hand *)
- Not_found -> exp
+ Not_found -> exp
in
(* The input [vi] is from the old project, so get the corresponding variable
from the new one, otherwise AST integrity is violated *)
@@ -488,15 +489,15 @@ let mk_global_init ~loc vi off init =
let handle_function_parameters kf env =
if is_enabled () then
let env, _ = List.fold_left
- (fun (env, index) param ->
- let env =
- if Mmodel_analysis.must_model_vi ~kf param
- then track_argument param index env kf
- else env
- in
- env, index + 1)
- (env, 0)
- (Kernel_function.get_formals kf)
+ (fun (env, index) param ->
+ let env =
+ if Mmodel_analysis.must_model_vi ~kf param
+ then track_argument param index env kf
+ else env
+ in
+ env, index + 1)
+ (env, 0)
+ (Kernel_function.get_formals kf)
in env
else
env
@@ -505,8 +506,8 @@ let handle_stmt stmt env kf =
if is_enabled () then begin
match stmt.skind with
| Instr instr -> handle_instruction stmt instr env kf
- | Return(ret, loc) -> Extlib.may_map
- (fun ret -> handle_return_stmt loc ret env kf) ~dft:env ret
+ | Return(ret, loc) ->
+ Extlib.may_map (fun ret -> handle_return_stmt loc ret env kf) ~dft:env ret
| Goto _ | Break _ | Continue _ | If _ | Switch _ | Loop _ | Block _
| UnspecifiedSequence _ | Throw _ | TryCatch _ | TryFinally _
| TryExcept _ -> env
diff --git a/src/plugins/e-acsl/src/code_generator/temporal.mli b/src/plugins/e-acsl/src/code_generator/temporal.mli
index 087683efea0f91666aa6e29ad8d8b3f98fe1179d..469df071656ebe7278c7090343e8ab85e3a71959 100644
--- a/src/plugins/e-acsl/src/code_generator/temporal.mli
+++ b/src/plugins/e-acsl/src/code_generator/temporal.mli
@@ -43,8 +43,8 @@ val handle_stmt: stmt -> Env.t -> kernel_function -> Env.t
properties of memory blocks *)
val generate_global_init: varinfo -> offset -> init -> stmt option
- (** Generate [Some s], where [s] is a statement tracking global initializer
- or [None] if there is no need to track it *)
+(** Generate [Some s], where [s] is a statement tracking global initializer
+ or [None] if there is no need to track it *)
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 009763c7931d6f8d47f548698052917a7551ed21..2df14a6f11f222d8a098245d820b8623e232d83d 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -141,7 +141,7 @@ let add_cast ~loc ?name env kf ctx strnum t_opt e =
None
new_ty
(fun v _ ->
- [ Constructor.mk_lib_call ~loc ~result:(Cil.var v) fname [ e ] ])
+ [ Smart_stmt.lib_call ~loc ~result:(Cil.var v) fname [ e ] ])
in
e, env
else if Gmp_types.Q.is_t ty || strnum = Str_R then
@@ -229,7 +229,7 @@ let conditional_to_exp ?(name="if") loc kf t_opt e1 (e2, env2) (e3, env3) =
let s = affect e3 in
Env.pop_and_get env3 s ~global_clear:false Env.Middle
in
- [ Constructor.mk_if ~loc ~cond:e1 then_blk ~else_blk ])
+ [ Smart_stmt.if_stmt ~loc ~cond:e1 then_blk ~else_blk ])
in
e, env
@@ -276,7 +276,7 @@ and context_insensitive_term_to_exp kf env t =
c, env, strnum, ""
| TLval lv ->
let lv, env, name = tlval_to_lval kf env lv in
- Constructor.mk_lval ~loc lv, env, C_number, name
+ Smart_exp.lval ~loc lv, env, C_number, name
| TSizeOf ty -> Cil.sizeOf ~loc ty, env, C_number, "sizeof"
| TSizeOfE t ->
let e, env = term_to_exp kf env t in
@@ -303,7 +303,7 @@ and context_insensitive_term_to_exp kf env t =
kf
~name:vname
(Some t)
- (fun _ ev -> [ Constructor.mk_lib_call ~loc name [ ev; e ] ])
+ (fun _ ev -> [ Smart_stmt.lib_call ~loc name [ ev; e ] ])
in
e, env, C_number, ""
else if Gmp_types.Q.is_t ty then
@@ -332,7 +332,7 @@ and context_insensitive_term_to_exp kf env t =
let e2, env = term_to_exp kf env t2 in
if Gmp_types.Z.is_t ty then
let name = name_of_mpz_arith_bop bop in
- let mk_stmts _ e = [ Constructor.mk_lib_call ~loc name [ e; e1; e2 ] ] in
+ let mk_stmts _ e = [ Smart_stmt.lib_call ~loc name [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
let _, e, env =
Env.new_var_and_mpz_init ~loc ~name env kf (Some t) mk_stmts
@@ -370,14 +370,14 @@ and context_insensitive_term_to_exp kf env t =
let mk_stmts _v e =
assert (Gmp_types.Z.is_t ty);
let cond =
- Constructor.mk_runtime_check
+ Smart_stmt.runtime_check
(Env.annotation_kind env)
kf
guard
p
in
Env.add_assert kf cond p;
- let instr = Constructor.mk_lib_call ~loc name [ e; e1; e2 ] in
+ let instr = Smart_stmt.lib_call ~loc name [ e; e1; e2 ] in
[ cond; instr ]
in
let name = Misc.name_of_binop bop in
@@ -435,7 +435,7 @@ and context_insensitive_term_to_exp kf env t =
(fun vi _e ->
let result = Cil.var vi in
let fname = "__gmpz_fits_ulong_p" in
- [ Constructor.mk_lib_call ~loc ~result fname [ e2 ] ])
+ [ Smart_stmt.lib_call ~loc ~result fname [ e2 ] ])
in
e, env
in
@@ -454,8 +454,8 @@ and context_insensitive_term_to_exp kf env t =
in
let pname = bop_name ^ "_rhs_fits_in_mp_bitcnt_t" in
let pred = { pred with pred_name = pname :: pred.pred_name } in
- let cond = Constructor.mk_runtime_check
- Constructor.RTE
+ let cond = Smart_stmt.runtime_check
+ Smart_stmt.RTE
kf
coerce_guard
pred
@@ -465,7 +465,7 @@ and context_insensitive_term_to_exp kf env t =
in
let result = Cil.var vi in
let name = "__gmpz_get_ui" in
- let instr = Constructor.mk_lib_call ~loc ~result name [ e2 ] in
+ let instr = Smart_stmt.lib_call ~loc ~result name [ e2 ] in
[ coerce_guard_cond; instr ]
in
let name = e2_name ^ bop_name ^ "_coerced" in
@@ -484,7 +484,7 @@ and context_insensitive_term_to_exp kf env t =
(* Create the shift instruction *)
let mk_shift_instr result_e =
let name = name_of_mpz_arith_bop bop in
- Constructor.mk_lib_call ~loc name [ result_e; e1; e2_as_bitcnt_e ]
+ Smart_stmt.lib_call ~loc name [ result_e; e1; e2_as_bitcnt_e ]
in
(* Put t in an option to use with comparison_to_exp and
@@ -515,8 +515,8 @@ and context_insensitive_term_to_exp kf env t =
in
let e1_guard_cond =
let pred = Logic_const.prel ~loc (Rge, t1, zero) in
- let cond = Constructor.mk_runtime_check
- Constructor.RTE
+ let cond = Smart_stmt.runtime_check
+ Smart_stmt.RTE
kf
e1_guard
pred
@@ -568,7 +568,7 @@ and context_insensitive_term_to_exp kf env t =
if Gmp_types.Z.is_t ty then
let mk_stmts _v e =
let name = name_of_mpz_arith_bop bop in
- let instr = Constructor.mk_lib_call ~loc name [ e; e1; e2 ] in
+ let instr = Smart_stmt.lib_call ~loc name [ e; e1; e2 ] in
[ instr ]
in
let name = Misc.name_of_binop bop in
@@ -646,7 +646,7 @@ and context_insensitive_term_to_exp kf env t =
(Some t)
(Misc.cty (Extlib.the li.l_type))
(fun vi _ ->
- [ Constructor.mk_lib_call ~loc ~result:(Cil.var vi) fname args ])
+ [ Smart_stmt.lib_call ~loc ~result:(Cil.var vi) fname args ])
else
(* build the arguments and compute the integer_ty of the parameters *)
let params_ty, args, env =
@@ -788,7 +788,7 @@ and comparison_to_exp
~name
Cil.intType
(fun v _ ->
- [ Constructor.mk_lib_call ~loc
+ [ Smart_stmt.lib_call ~loc
~result:(Cil.var v)
"__gmpz_cmp"
[ e1; e2 ] ])
@@ -855,7 +855,7 @@ and env_of_li li kf env loc =
let e, env = term_to_exp kf env t in
let stmt = match Typing.get_number_ty t with
| Typing.(C_integer _ | C_float _ | Nan) ->
- Constructor.mk_assigns ~loc ~result:(Cil.var vi) e
+ Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
| Typing.Gmpz ->
Gmp.init_set ~loc (Cil.var vi) vi_e e
| Typing.Rational ->
@@ -1033,7 +1033,7 @@ and translate_rte_annots:
fun pp elt kf env l ->
let old_valid = !is_visiting_valid in
let old_kind = Env.annotation_kind env in
- let env = Env.set_annotation_kind env Constructor.RTE in
+ let env = Env.set_annotation_kind env Smart_stmt.RTE in
let env =
List.fold_left
(fun env a -> match a.annot_content with
@@ -1078,7 +1078,7 @@ and translate_named_predicate kf env p =
Env.add_stmt
env
kf
- (Constructor.mk_runtime_check
+ (Smart_stmt.runtime_check
(Env.annotation_kind env)
kf
e
@@ -1168,7 +1168,7 @@ let assumes_predicate bhv =
bhv.b_assumes
let translate_preconditions kf kinstr env behaviors =
- let env = Env.set_annotation_kind env Constructor.Precondition in
+ let env = Env.set_annotation_kind env Smart_stmt.Precondition in
let do_behavior env b =
let assumes_pred = assumes_predicate b in
List.fold_left
@@ -1193,7 +1193,7 @@ let translate_preconditions kf kinstr env behaviors =
List.fold_left do_behavior env behaviors
let translate_postconditions kf kinstr env behaviors =
- let env = Env.set_annotation_kind env Constructor.Postcondition in
+ let env = Env.set_annotation_kind env Smart_stmt.Postcondition in
(* generate one guard by postcondition of each behavior *)
let do_behavior env b =
let env =
@@ -1284,7 +1284,7 @@ let translate_pre_code_annotation kf stmt env annot =
let convert env = match annot.annot_content with
| AAssert(l, _, p) ->
if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
- let env = Env.set_annotation_kind env Constructor.Assertion in
+ let env = Env.set_annotation_kind env Smart_stmt.Assertion in
if l <> [] then
not_yet env "@[assertion applied only on some behaviors@]";
translate_named_predicate kf env p
@@ -1296,7 +1296,7 @@ let translate_pre_code_annotation kf stmt env annot =
translate_pre_spec kf (Kstmt stmt) env spec ;
| AInvariant(l, loop_invariant, p) ->
if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
- let env = Env.set_annotation_kind env Constructor.Invariant in
+ let env = Env.set_annotation_kind env Smart_stmt.Invariant in
if l <> [] then
not_yet env "@[invariant applied only on some behaviors@]";
let env = translate_named_predicate kf env p in
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 ../../../../.."