From 7da89554af46f144c8dc6c24abed036d8974eae8 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 26 Aug 2020 14:05:14 +0200
Subject: [PATCH] [eacsl] Fix file indentations
---
.Makefile.lint | 7 -
.../e-acsl/src/analyses/mmodel_analysis.ml | 382 +++++++++---------
src/plugins/e-acsl/src/analyses/rte.ml | 10 +-
.../src/code_generator/at_with_lscope.ml | 241 +++++------
.../src/code_generator/at_with_lscope.mli | 6 +-
.../e-acsl/src/code_generator/temporal.ml | 191 ++++-----
.../e-acsl/src/code_generator/temporal.mli | 4 +-
7 files changed, 422 insertions(+), 419 deletions(-)
diff --git a/.Makefile.lint b/.Makefile.lint
index 80fb691a837..06c49f05b54 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/src/analyses/mmodel_analysis.ml b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
index c480e318b76..db85a8c4c96 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 96a1afbb988..9305eff3a55 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 040c83991ed..fe974d215cd 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 =
+ 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;
+ [])
in
(* Index *)
let t_index = index_from_sizes_and_shifts ~loc sizes_and_shifts in
@@ -301,28 +302,28 @@ let to_exp ~loc kf env pot label =
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. *)
+ variable declarations. *)
[ Constructor.mk_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 =
+ 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"
end
in
(* Storing loops *)
@@ -333,10 +334,10 @@ 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
+ (Constructor.mk_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
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 f5b51d739bd..0a971045fdd 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/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml
index a2694969cc6..e57b894f428 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 *)
@@ -106,8 +106,8 @@ end = struct
in
(* TODO: Returning structs is unsupported so far *)
(match (Cil.typeOf lhs) with
- | TPtr _ -> ()
- | _ -> Error.not_yet "Struct in return");
+ | TPtr _ -> ()
+ | _ -> Error.not_yet "Struct in return");
Constructor.mk_lib_call ~loc (RTL.mk_temporal_name fname) [ lhs ]
let reset_return_referent ~loc =
@@ -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,23 +241,23 @@ 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
@@ -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, (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)
~dft:env
vals
@@ -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 087683efea0..469df071656 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:
--
GitLab