diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index e040d56b4057e911318d689fca91beb857e3832a..67badd902929239d8d609c12369c336bd1f4779d 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -58,7 +58,9 @@ PLUGIN_CMO:= local_config \
gmpz \
literal_strings \
mmodel_analysis \
+ prepare_ast \
dup_functions \
+ exit_points \
label \
env \
interval \
diff --git a/src/plugins/e-acsl/exit_points.ml b/src/plugins/e-acsl/exit_points.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2701b2be851f7e26cd08a315df3fb772adeb1f86
--- /dev/null
+++ b/src/plugins/e-acsl/exit_points.ml
@@ -0,0 +1,142 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2016 *)
+(* 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 license/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Cil_datatype
+
+module Build_env(X: sig type t val name: string end): sig
+ val add: stmt -> X.t -> unit
+ val get: stmt -> X.t
+ val get_all: stmt -> X.t list
+ val is_empty: unit -> bool
+ val clear: unit -> unit
+end = struct
+
+ let tbl = Stmt.Hashtbl.create 17
+ let add = Stmt.Hashtbl.add tbl
+
+ let get stmt =
+ try Stmt.Hashtbl.find tbl stmt
+ with Not_found ->
+ Options.fatal "unknown stmt %a in %s" Printer.pp_stmt stmt X.name
+
+ let get_all = Stmt.Hashtbl.find_all tbl
+ let is_empty () = Stmt.Hashtbl.length tbl = 0
+ let clear () = Stmt.Hashtbl.clear tbl
+
+end
+
+(* Mapping of statements to local variables available within that statement's
+ scope. The mappings of this structure are used to determine variables which
+ need to be removed before goto jumps. Generally, if some goto (with
+ scope variables are given by set G') jumps to a labeled statement with
+ scope variables given by set L', then the goto exists the scopes of
+ variables given via set G' \ L'. Consequently, if those variables are
+ tracked, they need to be removed from tracking. *)
+module SLocals =
+ Build_env(struct type t = Varinfo.Set.t let name = "SLocals" end)
+
+(* Statement to statement mapping indicating source/destination of a jump.
+ For instance, break statements are mapped to switches or loops they jump
+ out from and goto statements are mapped to their labeled statements. Notably,
+ such information does not really be computed for gotos (since they already
+ capture references to labelled statements they jumps to). Nevertheless it is
+ done for consistency, so all required information is stored uniformly. *)
+module Exits =
+ Build_env(struct type t = stmt let name = "Exits" end)
+
+(* Map labelled statements back to gotos which lead to them *)
+module LJumps =
+ Build_env(struct type t = stmt let name = "LJumps" end)
+
+let clear () =
+ SLocals.clear ();
+ Exits.clear ();
+ LJumps.clear ()
+
+let is_empty () =
+ SLocals.is_empty () && Exits.is_empty () && LJumps.is_empty ()
+
+let delete_vars stmt =
+ match stmt.skind with
+ | Goto _ | Break _ | Continue _ ->
+ Varinfo.Set.diff (SLocals.get stmt) (SLocals.get (Exits.get stmt))
+ | _ ->
+ Varinfo.Set.empty
+
+let store_vars stmt =
+ let gotos = LJumps.get_all stmt in
+ List.fold_left
+ (fun acc goto ->
+ Varinfo.Set.union
+ acc
+ (Varinfo.Set.diff (SLocals.get stmt) (SLocals.get goto)))
+ Varinfo.Set.empty
+ gotos
+
+let list_flatten_to_set =
+ List.fold_left
+ (List.fold_left (fun acc v -> Varinfo.Set.add v acc))
+ Varinfo.Set.empty
+
+class jump_context = object (_)
+ inherit Visitor.frama_c_inplace
+
+ val mutable locals = [[]]
+ (* Maintained list of local variables within the scope of a currently
+ visited statement. Variables within a single scope are given by a
+ single list *)
+
+ val jumps = Stack.create ()
+ (* Stack of entered switches and loops *)
+
+ method !vblock blk =
+ locals <- [blk.blocals] @ locals;
+ Cil.DoChildrenPost
+ (fun blk -> locals <- List.tl locals; blk)
+
+ method !vstmt stmt =
+ match stmt.skind with
+ | Loop _ | Switch _ ->
+ SLocals.add stmt (list_flatten_to_set locals);
+ Stack.push stmt jumps;
+ Cil.DoChildrenPost (fun st -> ignore(Stack.pop jumps); st)
+ | Break _ | Continue _ ->
+ Exits.add stmt (Stack.top jumps);
+ SLocals.add stmt (list_flatten_to_set locals);
+ Cil.DoChildren
+ | Goto(sref, _) ->
+ SLocals.add stmt (list_flatten_to_set locals);
+ Exits.add stmt !sref;
+ LJumps.add !sref stmt;
+ Cil.DoChildren
+ | Instr _ | Return _ | If _ | Block _ | UnspecifiedSequence _
+ | Throw _ | TryCatch _ | TryFinally _ | TryExcept _ ->
+ (match stmt.labels with
+ | [] -> ()
+ | _ :: _ -> SLocals.add stmt (list_flatten_to_set locals));
+ Cil.DoChildren
+end
+
+let generate fct =
+ assert (is_empty ());
+ ignore (Cil.visitCilFunction (new jump_context :> Cil.cilVisitor) fct)
diff --git a/src/plugins/e-acsl/exit_points.mli b/src/plugins/e-acsl/exit_points.mli
new file mode 100644
index 0000000000000000000000000000000000000000..57d6773a83858e89e1c9effce1dc9c6fa9d76642
--- /dev/null
+++ b/src/plugins/e-acsl/exit_points.mli
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2016 *)
+(* 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 license/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** E-ACSL tracks a local variable by injecting:
+ - a call to [__e_acsl_store_block] at the beginning of its scope, and
+ - a call to [__e_acsl_delete_block] at the end of the scope.
+ This is not always sufficient to track variables because execution
+ may exit a scope early (for instance via a goto or a break statement).
+ This module computes program points at which extra `delete_block` statements
+ need to be added to handle such early scope exits. *)
+
+open Cil_types
+open Cil_datatype
+
+val generate: fundec -> unit
+(** Visit a function and populate data structures used to compute exit points *)
+
+val clear: unit -> unit
+(** Clear all gathered data *)
+
+val delete_vars: stmt -> Varinfo.Set.t
+(** Given a statement which potentially leads to an early scope exit (such as
+ goto, break or continue) return the list of local variables which
+ need to be removed from tracking before that statement is executed.
+ Before calling this function [generate] need to be executed. *)
+
+val store_vars: stmt -> Varinfo.Set.t
+(** Compute variables that should be re-recorded before a labelled statement to
+ which some goto jumps *)
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index d8ea9eca1d94fb8eda2ca6fa2cd9cefbd8e89edf..3873ed15198e33e57d2d87e96413ec1a583957d8 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -25,7 +25,7 @@ let check () =
let t = Error.nb_untypable () in
let n = Error.nb_not_yet () in
let print msg n =
- Options.result "@[%d annotation%s %s ignored,@ being %s.@]"
+ Options.result "@[%d annotation%s %s ignored,@ being %s.@]"
n
(if n > 1 then "s" else "")
(if n > 1 then "were" else "was")
@@ -75,26 +75,26 @@ let unmemoized_extend_ast () =
Options.feedback ~level:2 "AST already computed: \
E-ACSL is going to work on a copy.";
let name = Project.get_name (Project.current ()) in
- let tmpfile =
+ let tmpfile =
Extlib.temp_file_cleanup_at_exit ("e_acsl_" ^ name) ".i" in
let cout = open_out tmpfile in
let fmt = Format.formatter_of_out_channel cout in
File.pretty_ast ~fmt ();
- let selection =
+ let selection =
State_selection.diff
- State_selection.full
- (State_selection.with_dependencies Ast.self)
+ State_selection.full
+ (State_selection.with_dependencies Ast.self)
in
let prj =
Project.create_by_copy
~last:false
- ~selection
- (Format.asprintf "%s for E-ACSL" name)
+ ~selection
+ (Format.asprintf "%s for E-ACSL" name)
in
Project.on prj
(fun () ->
- Kernel.Files.set [ tmpfile ];
- extend ())
+ Kernel.Files.set [ tmpfile ];
+ extend ())
();
Some prj
end else begin
@@ -103,7 +103,7 @@ E-ACSL is going to work on a copy.";
end
let extend_ast () = match !extended_ast_project with
- | To_be_extended ->
+ | To_be_extended ->
let prj = unmemoized_extend_ast () in
extended_ast_project := Already_extended prj;
(match prj with
@@ -147,31 +147,42 @@ let generate_code =
apply_on_e_acsl_ast
(fun () ->
Options.feedback "beginning translation.";
- let dup_prj = Dup_functions.dup () in
+ let prepared_prj = Prepare_ast.prepare () in
let res =
- Project.on
- dup_prj
- (fun () ->
- Gmpz.init_t ();
- Mmodel_analysis.reset ();
- let visit prj = Visit.do_visit ~prj true in
- let prj = File.create_project_from_visitor name visit in
- Loops.apply_after_transformation prj;
-(* remove the RTE's results computed from E-ACSL: their are
- partial and associated with the wrong kernel function (the
- one of the old project). *)
- Project.clear
- ~selection:(State_selection.with_dependencies !Db.RteGen.self)
- ~project:prj
- ();
- Resulting_projects.mark_as_computed ();
- Project.copy
- ~selection:(State_selection.singleton Kernel.Files.self)
- prj;
- prj)
+ Project.on prepared_prj
+ (fun () ->
+ let dup_prj = Dup_functions.dup () in
+ let res =
+ Project.on
+ dup_prj
+ (fun () ->
+ Gmpz.init_t ();
+ Mmodel_analysis.reset ();
+ let visit prj = Visit.do_visit ~prj true in
+ let prj = File.create_project_from_visitor name visit in
+ Loops.apply_after_transformation prj;
+ (* remove the RTE's results computed from E-ACSL: their are
+ partial and associated with the wrong kernel function
+ (the one of the old project). *)
+ let selection =
+ State_selection.with_dependencies !Db.RteGen.self
+ in
+ Project.clear ~selection ~project:prj ();
+ Resulting_projects.mark_as_computed ();
+ Project.copy
+ ~selection:(State_selection.singleton Kernel.Files.self)
+ prj;
+ prj)
+ ()
+ in
+ if Options.Debug.get () = 0 then
+ Project.remove ~project:dup_prj ();
+ res)
()
in
- if Options.Debug.get () = 0 then Project.remove ~project:dup_prj ();
+ if Options.Debug.get () = 0 then begin
+ Project.remove ~project:prepared_prj ();
+ end;
Options.feedback "translation done in project \"%s\"."
(Options.Project_name.get ());
res)
@@ -194,7 +205,7 @@ let predicate_to_exp =
Kernel_function.ty Cil_datatype.Predicate.ty Cil_datatype.Exp.ty)
Translate.predicate_to_exp
-let add_e_acsl_library _files =
+let add_e_acsl_library _files =
if Options.must_visit () || Options.Prepare.get () then ignore (extend_ast ())
(* extending the AST as soon as possible reduce the amount of time the AST is
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 3cc48be66de6d8639af873f86664d0f600140633..a22b60a23e2e0d4c2954d45a3d9b757d2135754d 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -34,14 +34,14 @@ let library_files () =
"e_acsl_gmp.h";
"e_acsl_mmodel_api.h" ]
-let normalized_library_files =
+let normalized_library_files =
lazy (List.map Filepath.normalize (library_files ()))
-let is_library_loc (loc, _) =
+let is_library_loc (loc, _) =
List.mem loc.Lexing.pos_fname (Lazy.force normalized_library_files)
let library_functions = Datatype.String.Hashtbl.create 17
-let register_library_function vi =
+let register_library_function vi =
Datatype.String.Hashtbl.add library_functions vi.vname vi
let reset () = Datatype.String.Hashtbl.clear library_functions
@@ -69,7 +69,7 @@ let mk_call ~loc ?result fname args =
in
let args =
List.map2
- (fun (_, ty, _) arg ->
+ (fun (_, ty, _) arg ->
let e =
match ty, Cil.unrollType (Cil.typeOf arg), arg.enode with
| TPtr _, TArray _, Lval lv -> Cil.new_exp ~loc (StartOf lv)
@@ -82,15 +82,15 @@ let mk_call ~loc ?result fname args =
in
Cil.mkStmtOneInstr ~valid_sid:true (Call(result, f, args, loc))
-type annotation_kind =
+type annotation_kind =
| Assertion
| Precondition
| Postcondition
| Invariant
| RTE
-let kind_to_string loc k =
- Cil.mkString
+let kind_to_string loc k =
+ Cil.mkString
~loc
(match k with
| Assertion -> "Assertion"
@@ -143,44 +143,44 @@ let mk_api_name fname =
e_acsl_api_prefix ^ fname
let mk_gen_name name =
- e_acsl_gen_prefix ^ name
+ e_acsl_gen_prefix ^ name
(* Build a C conditional doing a runtime assertion check. *)
let mk_e_acsl_guard ?(reverse=false) kind kf e p =
let loc = p.pred_loc in
- let msg =
+ let msg =
Kernel.Unicode.without_unicode
- (Format.asprintf "%a@?" Printer.pp_predicate) p
+ (Format.asprintf "%a@?" Printer.pp_predicate) p
in
let line = (fst loc).Lexing.pos_lnum in
- let e =
- if reverse then e else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
+ let e =
+ if reverse then e else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
in
- mk_call
- ~loc
+ mk_call
+ ~loc
(mk_api_name "assert")
- [ e;
- kind_to_string loc kind;
- Cil.mkString ~loc (get_orig_name kf);
- Cil.mkString ~loc msg;
- Cil.integer loc line ]
+ [ e;
+ kind_to_string loc kind;
+ Cil.mkString ~loc (get_orig_name kf);
+ Cil.mkString ~loc msg;
+ Cil.integer loc line ]
-let mk_block prj stmt b =
+let mk_block prj stmt b =
let mk b = match b.bstmts with
- | [] ->
+ | [] ->
(match stmt.skind with
| Instr(Skip _) -> stmt
| _ -> assert false)
- | [ s ] ->
- if Stmt.equal stmt s then s
- else
+ | [ s ] ->
+ if Stmt.equal stmt s then s
+ else
(* [JS 2012/10/19] this case exactly corresponds to
__e_acsl_assert(...) when the annotation is associated to a
statement <skip>. Creating a block prevents the printer to add
a stupid unintuitive block *)
Cil.mkStmt ~valid_sid:true (Block b)
| _ :: _ -> Cil.mkStmt ~valid_sid:true (Block b)
- in
+ in
Project.on prj mk b
(* ************************************************************************** *)
@@ -188,8 +188,8 @@ let mk_block prj stmt b =
(* ************************************************************************** *)
let result_lhost kf =
- let stmt =
- try Kernel_function.find_return kf
+ let stmt =
+ try Kernel_function.find_return kf
with Kernel_function.No_Statement -> assert false
in
match stmt.skind with
@@ -206,11 +206,11 @@ let result_vi kf = match result_lhost kf with
let mk_debug_mmodel_stmt stmt =
if Options.debug_atleast 1
- && Options.is_debug_key_enabled Options.dkey_analysis
+ && Options.is_debug_key_enabled Options.dkey_analysis
then
let debug = mk_call ~loc:(Stmt.loc stmt) (mk_api_name "memory_debug") [] in
Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ stmt; debug]))
- else
+ else
stmt
let mk_full_init_stmt ?(addr=true) vi =
@@ -223,21 +223,21 @@ let mk_full_init_stmt ?(addr=true) vi =
mk_debug_mmodel_stmt stmt
let mk_initialize ~loc (host, offset as lv) = match host, offset with
- | Var _, NoOffset -> mk_call ~loc
+ | Var _, NoOffset -> mk_call ~loc
(mk_api_name "full_init")
[ Cil.mkAddrOf ~loc lv ]
- | _ ->
+ | _ ->
let typ = Cil.typeOfLval lv in
- mk_call ~loc
+ mk_call ~loc
(mk_api_name "initialize")
[ Cil.mkAddrOf ~loc lv; Cil.new_exp loc (SizeOf typ) ]
-let mk_store_stmt ?str_size vi =
+let mk_named_store_stmt name ?str_size vi =
let ty = Cil.unrollType vi.vtype in
let loc = vi.vdecl in
- let store = mk_call ~loc (mk_api_name "store_block") in
+ let store = mk_call ~loc (mk_api_name name) in
let stmt = match ty, str_size with
- | TArray(_, Some _,_,_), None ->
+ | TArray(_, Some _,_,_), None ->
store [ Cil.evar ~loc vi ; Cil.sizeOf ~loc ty ]
| TPtr(TInt(IChar, _), _), Some size -> store [ Cil.evar ~loc vi ; size ]
| _, None -> store [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
@@ -245,12 +245,17 @@ let mk_store_stmt ?str_size vi =
in
mk_debug_mmodel_stmt stmt
+let mk_store_stmt ?str_size vi =
+ mk_named_store_stmt "store_block" ?str_size vi
+
+let mk_duplicate_store_stmt ?str_size vi =
+ mk_named_store_stmt "store_block_duplicate" ?str_size vi
+
let mk_delete_stmt vi =
let loc = vi.vdecl in
let stmt = match Cil.unrollType vi.vtype with
| TArray(_, Some _, _, _) ->
mk_call ~loc (mk_api_name "delete_block") [ Cil.evar ~loc vi ]
- (* | Tarray(_, None, _, _)*)
| _ -> mk_call ~loc (mk_api_name "delete_block") [ Cil.mkAddrOfVi vi ]
in
mk_debug_mmodel_stmt stmt
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index e00746e146fcd696323dd285c77eeff15903f753..e9de1d3662c1aae4f9ea27c5e320add1ace87d82 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -38,15 +38,15 @@ val mk_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
val mk_debug_mmodel_stmt: stmt -> stmt
-type annotation_kind =
+type annotation_kind =
| Assertion
| Precondition
| Postcondition
| Invariant
| RTE
-val mk_e_acsl_guard:
- ?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate
+val mk_e_acsl_guard:
+ ?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate
-> stmt
val mk_block: Project.t -> stmt -> block -> stmt
@@ -71,6 +71,7 @@ val register_library_function: varinfo -> unit
val reset: unit -> unit
val mk_store_stmt: ?str_size:exp -> varinfo -> stmt
+val mk_duplicate_store_stmt: ?str_size:exp -> varinfo -> stmt
val mk_delete_stmt: varinfo -> stmt
val mk_full_init_stmt: ?addr:bool -> varinfo -> stmt
val mk_initialize: loc:location -> lval -> stmt
diff --git a/src/plugins/e-acsl/prepare_ast.ml b/src/plugins/e-acsl/prepare_ast.ml
new file mode 100644
index 0000000000000000000000000000000000000000..dbebc4ef421cd7f35c57bd48d3fdd2936788e4bd
--- /dev/null
+++ b/src/plugins/e-acsl/prepare_ast.ml
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2016 *)
+(* 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 license/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+class prepare_visitor prj = object (_)
+ inherit Visitor.frama_c_copy prj
+
+ method !vstmt_aux _ =
+ Cil.DoChildrenPost (fun stmt ->
+ match stmt.skind with
+ | Switch(_,sw_blk,_,_) ->
+ let new_blk = Cil.mkBlock [ stmt ] in
+ let new_stmt = Cil.mkStmt (Block new_blk) in
+ new_blk.blocals <- sw_blk.blocals;
+ sw_blk.blocals <- [];
+ new_stmt
+ | _ -> stmt)
+
+ initializer
+ Project.copy ~selection:(Parameter_state.get_selection ()) prj
+end
+
+let prepare () =
+ Options.feedback ~level:2 "prepare AST for E-ACSL transformations";
+ File.create_project_from_visitor
+ "e_acsl_prepare_ast"
+ (new prepare_visitor)
diff --git a/src/plugins/e-acsl/prepare_ast.mli b/src/plugins/e-acsl/prepare_ast.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a8c4fed1ee6facfbd7229a4211a2d3477846c779
--- /dev/null
+++ b/src/plugins/e-acsl/prepare_ast.mli
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2016 *)
+(* 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 license/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Prepare AST for E-ACSL generation.
+ * So for this mudule performs the only task:
+ * - Move declarations of variables declared in the bodies of switch
+ * statements to upper scopes.
+*)
+
+val prepare: unit -> Project.t
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
index 21985b94e1cd2eca4695e98af06be88476ce5e06..e62516c2fa143a86ea7cc919724857bfa3c95a7b 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
@@ -314,6 +314,24 @@ static void delete_block(void* ptr) {
}
}
}
+
+static void* store_block_duplicate(void* ptr, size_t size) {
+ bt_block * tmp = NULL;
+ if (ptr != NULL) {
+ bt_block * tmp = bt_lookup(ptr);
+ if (tmp) {
+#ifdef E_ACSL_DEBUG
+ /* Make sure that duplicate block, if so is of the same length */
+ if (tmp->size != size)
+ vabort("Attempt to store duplicate block of different length");
+#endif
+ delete_block(ptr);
+ }
+ store_block(ptr, size);
+ }
+ return tmp;
+}
+
/* }}} */
/* HEAP ALLOCATION {{{ */
@@ -566,6 +584,7 @@ strong_alias(bittree_aligned_alloc, aligned_alloc)
/* Explicit tracking */
public_alias(delete_block)
public_alias(store_block)
+public_alias(store_block_duplicate)
/* Predicates */
public_alias(offset)
public_alias(base_addr)
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
index 46a375dc46cf7548137a3ad8ea58c50c09f5b0d8..f19c4294999fd8276c77caa25075c4e87785026a 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
@@ -82,6 +82,16 @@ int posix_memalign(void **memptr, size_t alignment, size_t size)
void * __e_acsl_store_block(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
+/*! \brief Same as `__e_acsl_store_block`, but first check
+ * checks whether a block with a base address given by `ptr` exists in the
+ * tracked allocation and remove it before storing a new block.
+ *
+ * \param ptr base address of the tracked memory block
+ * \param size size of the tracked block in bytes */
+/*@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
+void * __e_acsl_store_block_duplicate(void * ptr, size_t size)
+ __attribute__((FC_BUILTIN));
+
/*! \brief Remove a memory block which base address is \p ptr from tracking. */
/*@ assigns \nothing; */
void __e_acsl_delete_block(void * ptr)
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
index a740e1e360c7fd0646467249027c2b6d61182a33..4699f2d81716064a64b8dc1578e6783eb36080dc 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
@@ -31,6 +31,7 @@
#include <sys/resource.h>
static int valid(void * ptr, size_t size);
+static int valid_read(void * ptr, size_t size);
#include "e_acsl_string.h"
#include "e_acsl_bits.h"
@@ -57,6 +58,13 @@ static void delete_block(void * ptr) {
shadow_freea(ptr);
}
+static void * store_block_duplicate(void * ptr, size_t size) {
+ if (valid_read(ptr, size))
+ delete_block(ptr);
+ shadow_alloca(ptr, size);
+ return ptr;
+}
+
static void full_init(void * ptr) {
initialize(ptr, block_length(ptr));
}
@@ -180,6 +188,7 @@ strong_alias(shadow_posix_memalign, posix_memalign)
/* Explicit tracking */
public_alias(delete_block)
public_alias(store_block)
+public_alias(store_block_duplicate)
/* Predicates */
public_alias2(segment_offset, offset)
public_alias2(segment_base_addr, base_addr)
diff --git a/src/plugins/e-acsl/tests/bts/bts1740.i b/src/plugins/e-acsl/tests/bts/bts1740.i
new file mode 100644
index 0000000000000000000000000000000000000000..98e99dc7358c69c4d66e322b75829050a4dacb71
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/bts1740.i
@@ -0,0 +1,18 @@
+/* run.config
+ COMMENT: bts #1740, about failure to correctly track local variables
+ in presence of goto
+*/
+
+int main(void) {
+ int *p;
+ {
+ int a = 0;
+ p = &a;
+ /*@ assert \valid(p); */
+ goto L;
+ }
+
+ L:
+ /*@ assert ! \valid(p); */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1740.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1740.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..845be00612efea9581746723802617b328a66215
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
@@ -0,0 +1,7 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/bts/bts1740.i:12:[value] warning: locals {a} escaping the scope of a block of main through p
+tests/bts/bts1740.i:16:[value] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&p);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index ccf51aabe3e61bb7666fba2f9d1f45dad23d3bdf..65b4060b695afdfc576b001f8caddb3c60b020cf 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -24,15 +24,15 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out);
*/
void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
{
- __e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
- __e_acsl_store_block((void *)(& Mwmax),(size_t)8);
__e_acsl_store_block((void *)(& Mtmax_out),(size_t)8);
+ __e_acsl_store_block((void *)(& Mwmax),(size_t)8);
+ __e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
__e_acsl_initialize((void *)Mtmax_out,sizeof(float));
*Mtmax_out = (float)((double)*Mtmax_in + ((double)5 - (double)((float)(
5 / 80) * *Mwmax) * 0.4));
- __e_acsl_delete_block((void *)(& Mtmax_in));
- __e_acsl_delete_block((void *)(& Mwmax));
__e_acsl_delete_block((void *)(& Mtmax_out));
+ __e_acsl_delete_block((void *)(& Mwmax));
+ __e_acsl_delete_block((void *)(& Mtmax_in));
return;
}
@@ -62,14 +62,14 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out);
*/
void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
{
- __e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
- __e_acsl_store_block((void *)(& Mwmin),(size_t)8);
__e_acsl_store_block((void *)(& Mtmin_out),(size_t)8);
+ __e_acsl_store_block((void *)(& Mwmin),(size_t)8);
+ __e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
__e_acsl_initialize((void *)Mtmin_out,sizeof(float));
*Mtmin_out = (float)(0.85 * (double)*Mwmin);
- __e_acsl_delete_block((void *)(& Mtmin_in));
- __e_acsl_delete_block((void *)(& Mwmin));
__e_acsl_delete_block((void *)(& Mtmin_out));
+ __e_acsl_delete_block((void *)(& Mwmin));
+ __e_acsl_delete_block((void *)(& Mtmin_in));
return;
}
@@ -120,9 +120,9 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
int __gen_e_acsl_valid;
int __gen_e_acsl_valid_2;
int __gen_e_acsl_valid_3;
- __e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
- __e_acsl_store_block((void *)(& Mwmin),(size_t)8);
__e_acsl_store_block((void *)(& Mtmin_out),(size_t)8);
+ __e_acsl_store_block((void *)(& Mwmin),(size_t)8);
+ __e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
__gen_e_acsl_valid = __e_acsl_valid((void *)Mtmin_in,sizeof(float));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"bar",
(char *)"\\valid(Mtmin_in)",17);
@@ -190,9 +190,9 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_assert(__gen_e_acsl_if,(char *)"Postcondition",(char *)"bar",
(char *)"*\\old(Mtmin_out) == *\\old(Mtmin_in) < 0.85 * *\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.:\n 0.85 * *\\old(Mwmin) != 0.",
23);
- __e_acsl_delete_block((void *)(& Mtmin_in));
- __e_acsl_delete_block((void *)(& Mwmin));
__e_acsl_delete_block((void *)(& Mtmin_out));
+ __e_acsl_delete_block((void *)(& Mwmin));
+ __e_acsl_delete_block((void *)(& Mtmin_in));
return;
}
}
@@ -216,9 +216,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
int __gen_e_acsl_valid;
int __gen_e_acsl_valid_2;
int __gen_e_acsl_valid_3;
- __e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
- __e_acsl_store_block((void *)(& Mwmax),(size_t)8);
__e_acsl_store_block((void *)(& Mtmax_out),(size_t)8);
+ __e_acsl_store_block((void *)(& Mwmax),(size_t)8);
+ __e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
__gen_e_acsl_valid = __e_acsl_valid((void *)Mtmax_in,sizeof(float));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"foo",
(char *)"\\valid(Mtmax_in)",5);
@@ -255,9 +255,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
(char *)"Postcondition",(char *)"foo",
(char *)"*\\old(Mtmax_out) == *\\old(Mtmax_in) + (5 - ((5 / 80) * *\\old(Mwmax)) * 0.4)",
11);
- __e_acsl_delete_block((void *)(& Mtmax_in));
- __e_acsl_delete_block((void *)(& Mwmax));
__e_acsl_delete_block((void *)(& Mtmax_out));
+ __e_acsl_delete_block((void *)(& Mwmax));
+ __e_acsl_delete_block((void *)(& Mtmax_in));
return;
}
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index eb341729c74ff62536e0b0f39ef1e298608c6bd6..73fe45e9e4e369b1cffed17422d3cd9a3a402ed2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -20,12 +20,12 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
*/
void atp_NORMAL_computeAverageAccel(ArrayInt *Accel, int *AverageAccel)
{
- __e_acsl_store_block((void *)(& Accel),(size_t)8);
__e_acsl_store_block((void *)(& AverageAccel),(size_t)8);
+ __e_acsl_store_block((void *)(& Accel),(size_t)8);
__e_acsl_initialize((void *)AverageAccel,sizeof(int));
*AverageAccel = (((((*Accel)[4] + (*Accel)[3]) + (*Accel)[2]) + (*Accel)[1]) + (*Accel)[0]) / 5;
- __e_acsl_delete_block((void *)(& Accel));
__e_acsl_delete_block((void *)(& AverageAccel));
+ __e_acsl_delete_block((void *)(& Accel));
return;
}
@@ -71,8 +71,8 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
ArrayInt *__gen_e_acsl_at_3;
ArrayInt *__gen_e_acsl_at_2;
int *__gen_e_acsl_at;
- __e_acsl_store_block((void *)(& Accel),(size_t)8);
__e_acsl_store_block((void *)(& AverageAccel),(size_t)8);
+ __e_acsl_store_block((void *)(& Accel),(size_t)8);
__gen_e_acsl_at_6 = Accel;
__gen_e_acsl_at_5 = Accel;
__gen_e_acsl_at_4 = Accel;
@@ -127,8 +127,8 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"*\\old(AverageAccel) ==\n(((((*\\old(Accel))[4] + (*\\old(Accel))[3]) + (*\\old(Accel))[2]) +\n (*\\old(Accel))[1])\n + (*\\old(Accel))[0])\n/ 5",
8);
- __e_acsl_delete_block((void *)(& Accel));
__e_acsl_delete_block((void *)(& AverageAccel));
+ __e_acsl_delete_block((void *)(& Accel));
return;
}
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
new file mode 100644
index 0000000000000000000000000000000000000000..7d1822a0543584b1951eae377aca95cd6a931aa6
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
@@ -0,0 +1,62 @@
+/* Generated by Frama-C */
+#include "stdlib.h"
+int main(void)
+{
+ int __retres;
+ int *p;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ {
+ int a;
+ __e_acsl_store_block((void *)(& a),(size_t)4);
+ __e_acsl_full_init((void *)(& a));
+ a = 0;
+ __e_acsl_full_init((void *)(& p));
+ p = & a;
+ /*@ assert \valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(p)",11);
+ }
+ }
+ __e_acsl_delete_block((void *)(& a));
+ goto L;
+ __e_acsl_delete_block((void *)(& a));
+ }
+ L:
+ /*@ assert ¬\valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized_2;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_2;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
+ }
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",
+ (char *)"main",(char *)"!\\valid(p)",16);
+ }
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
index 51bb8fb04b67b3018b4835c3cd33d4a638b5fb4a..96372a88cdf6508baef976d8ab4a3b4ec3bbe0e5 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -38,8 +38,8 @@ void g(int *p, int *q)
int __gen_e_acsl_at_3;
int __gen_e_acsl_at_2;
int __gen_e_acsl_at;
- __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_initialize((void *)p,sizeof(int));
*p = 0;
__e_acsl_initialize((void *)(p + 1),sizeof(int));
@@ -96,8 +96,8 @@ void g(int *p, int *q)
(char *)"\\at(*(p + \\at(*q,L1)),Here) == 2",28);
}
}
- __e_acsl_delete_block((void *)(& p));
__e_acsl_delete_block((void *)(& q));
+ __e_acsl_delete_block((void *)(& p));
return;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
index 76f52e27256a09e59fb476dc2b3eb6112cd8a397..ad94a8884d509d8203ef082ce8d1bb452759004e 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
@@ -103,8 +103,8 @@ void g(int *p, int *q)
int __gen_e_acsl_at_3;
__e_acsl_mpz_t __gen_e_acsl_at_2;
int __gen_e_acsl_at;
- __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_initialize((void *)p,sizeof(int));
*p = 0;
__e_acsl_initialize((void *)(p + 1),sizeof(int));
@@ -178,8 +178,8 @@ void g(int *p, int *q)
__gmpz_clear(__gen_e_acsl__4);
}
}
- __e_acsl_delete_block((void *)(& p));
__e_acsl_delete_block((void *)(& q));
+ __e_acsl_delete_block((void *)(& p));
__gmpz_clear(__gen_e_acsl_at_2);
return;
}
diff --git a/src/plugins/e-acsl/tests/runtime/bypassed_var.c b/src/plugins/e-acsl/tests/runtime/bypassed_var.c
new file mode 100644
index 0000000000000000000000000000000000000000..5201ef5f9cd6a62ba688ec1779d9c91deb5de918
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/bypassed_var.c
@@ -0,0 +1,16 @@
+/* run.config
+ COMMENT: Variable, which declaration is bypassed by a goto jump
+*/
+
+int main(int argc, char const **argv) {
+ goto L;
+ {
+ int *p;
+ L:
+ p = &argc; /* Important to keep this statement here to make sure
+ initialize is ran after store_block */
+
+ /*@ assert \valid(&p); */
+ }
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/runtime/decl_in_switch.c b/src/plugins/e-acsl/tests/runtime/decl_in_switch.c
new file mode 100644
index 0000000000000000000000000000000000000000..4914dfe74a3f67fc2cf0914437a93c4ce020dbc1
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/decl_in_switch.c
@@ -0,0 +1,17 @@
+/* run.config
+ DONTRUN:
+ COMMENT: Variables declared in the body of switch statements so far cannot
+ COMMENT: be tracked
+*/
+
+int main(int argc, char **argv) {
+ switch(argc) {
+ int *p;
+ default: {
+ p = &argc;
+ /*! assert \valid(p); */
+ break;
+ }
+ }
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/runtime/early_exit.c b/src/plugins/e-acsl/tests/runtime/early_exit.c
new file mode 100644
index 0000000000000000000000000000000000000000..8dd7631bf598e04a990f8b334eb37c3c641d0520
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/early_exit.c
@@ -0,0 +1,161 @@
+/* run.config
+ COMMENT: test that local variables within a scope are removed from tracking
+ even if the execution exists the scope early via goto, break or
+ continue.
+*/
+
+/* Simple test case from BTS (#1740) */
+int goto_bts() {
+ int *p;
+ {
+ int a = 0;
+ p = &a;
+ /*@ assert \valid(p); */
+ goto L;
+ }
+
+L:
+ /*@ assert ! \valid(p); */
+ return 0;
+}
+
+/* Make sure that when `goto` jumps over several scopes all locals
+ * from those scopes are removed. */
+int goto_valid() {
+ int a = 9;
+ int *p, *q, *r;
+ {
+ int a1 = 0;
+ p = &a1;
+ {
+ int a2 = 0;
+ q = &a2;
+ {
+ int a3 = 0;
+ r = &a3;
+
+ goto FIRST;
+ /* Dead code */
+ p = (void*)0;
+ r = q = &a;
+ }
+ }
+FIRST:
+ /* At this point `a1` is still in scope, while `a2` and `a3` are not, thus
+ * `q` and `r` become invalid, whereas `p` is still valid. */
+ /*@ assert \valid(p); */
+ /*@ assert ! \valid(q); */
+ /*@ assert ! \valid(r); */
+ /* The following `goto` invalidates `p`. */
+ goto SECOND;
+ /* Dead code */
+ p = r = q = &a;
+ }
+
+SECOND:
+ /*@ assert ! \valid(p); */
+ /*@ assert ! \valid(q); */
+ /*@ assert ! \valid(r); */
+ return 0;
+}
+
+/* Make sure that when a break statement is executed within a switch statement
+ * then all local variables declared within that switch are removed. */
+int switch_valid() {
+ int i = 1;
+ int *p, *q, *s;
+ {
+ s = &i;
+ switch(i) {
+ default: {
+ int a1 = 0;
+ p = &a1;
+ {
+ int a2 = 0;
+ q = &a2;
+ /*@ assert \valid(p); */
+ /*@ assert \valid(q); */
+ /*@ assert \valid(s); */
+ break;
+ }
+ /* Dead code */
+ p = q = &i;
+ s = (void*)0;
+ }
+ }
+ /* Break invalidates `p` and `q` but `s` is still in scope. */
+ /*@ assert ! \valid(q); */
+ /*@ assert ! \valid(p); */
+ /*@ assert \valid(s); */
+ }
+ return 0;
+}
+
+/* Same as switch_valid but for a break statement in a body of a loop. */
+int while_valid() {
+ int *p, *q, *r;
+ int i = 5;
+ {
+ int a0 = 0;
+ r = &a0;
+ while (--i) {
+ {
+ int a1 = 0;
+ p = &a1;
+ {
+ int a2 = 0;
+ q = &a2;
+ /*@ assert \valid(p); */
+ /*@ assert \valid(q); */
+ /*@ assert \valid(r); */
+ if (!i)
+ break;
+ }
+ }
+ }
+ /*@ assert ! \valid(p); */
+ /*@ assert ! \valid(q); */
+ /*@ assert \valid(r); */
+ }
+ return 0;
+}
+
+/* Make sure that when `continue` is executed then local variables in scope
+ * are not recorded twice. */
+void continue_valid() {
+ int i = 0;
+ int *p, *q, *r;
+
+ while (i++) {
+ /*@ assert ! \valid(p); */
+ /*@ assert ! \valid(q); */
+ int a1 = 1;
+ p = &a1;
+
+ /*@ assert \valid(p); */
+ /*@ assert ! \valid(q); */
+
+ {
+ int a2 = 1;
+ q = &a2;
+ /*@ assert \valid(p); */
+ /*@ assert \valid(q); */
+ continue;
+ }
+
+ if (i == 5)
+ break;
+ }
+
+ /*@ assert ! \valid(p); */
+ /*@ assert ! \valid(q); */
+}
+
+int main(int argc, const char *argv[]) {
+ goto_bts();
+ goto_valid();
+ switch_valid();
+ while_valid();
+ continue_valid();
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a0a8836bb7a329fc53da2da239850fee8b952dde
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle
@@ -0,0 +1,4 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/decl_in_switch.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/decl_in_switch.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/decl_in_switch.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/decl_in_switch.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c33737e3cac6e74853111a99a2a4002b6a9d7094
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/decl_in_switch.res.oracle
@@ -0,0 +1,3 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5c4f44cb7b170063e9201f3c9e7ecf22654ddd38
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
@@ -0,0 +1,35 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/runtime/early_exit.c:14:[value] warning: locals {a} escaping the scope of a block of goto_bts through p
+tests/runtime/early_exit.c:18:[value] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&p);
+tests/runtime/early_exit.c:37:[value] warning: locals {a2} escaping the scope of a block of goto_valid through q
+tests/runtime/early_exit.c:37:[value] warning: locals {a3} escaping the scope of a block of goto_valid through r
+tests/runtime/early_exit.c:47:[value] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&q);
+tests/runtime/early_exit.c:48:[value] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&r);
+tests/runtime/early_exit.c:50:[value] warning: locals {a1} escaping the scope of a block of goto_valid through p
+tests/runtime/early_exit.c:56:[value] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&p);
+tests/runtime/early_exit.c:57:[value] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&q);
+tests/runtime/early_exit.c:58:[value] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&r);
+tests/runtime/early_exit.c:79:[value] warning: locals {a1} escaping the scope of a block of switch_valid through p
+tests/runtime/early_exit.c:79:[value] warning: locals {a2} escaping the scope of a block of switch_valid through q
+tests/runtime/early_exit.c:87:[value] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&q);
+tests/runtime/early_exit.c:88:[value] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&p);
+tests/runtime/early_exit.c:103:[value] warning: locals {a1} escaping the scope of a block of while_valid through p
+tests/runtime/early_exit.c:103:[value] warning: locals {a2} escaping the scope of a block of while_valid through q
+tests/runtime/early_exit.c:116:[value] warning: accessing uninitialized left-value. assert \initialized(&p);
+tests/runtime/early_exit.c:116:[value] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&p);
+tests/runtime/early_exit.c:117:[value] warning: accessing uninitialized left-value. assert \initialized(&q);
+tests/runtime/early_exit.c:117:[value] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&q);
+tests/runtime/early_exit.c:99:[value] warning: locals {a0} escaping the scope of a block of while_valid through r
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
new file mode 100644
index 0000000000000000000000000000000000000000..7e1c554bd6a8077d99a6847b795e72bf054eb0fe
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
@@ -0,0 +1,32 @@
+/* Generated by Frama-C */
+#include "stdlib.h"
+int main(int argc, char const **argv)
+{
+ int __retres;
+ __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
+ __e_acsl_store_block((void *)(& argc),(size_t)4);
+ goto L;
+ {
+ int *p;
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ L: __e_acsl_store_block_duplicate((void *)(& p),(size_t)8);
+ __e_acsl_full_init((void *)(& p));
+ p = & argc;
+ /*@ assert \valid(&p); */
+ {
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& p),sizeof(int *));
+ __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",
+ (char *)"main",(char *)"\\valid(&p)",13);
+ __e_acsl_delete_block((void *)(& p));
+ }
+ }
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& argc));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_decl_in_switch.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_decl_in_switch.c
new file mode 100644
index 0000000000000000000000000000000000000000..15d0281d5ae0b4dc878a687bc8131e19bc4aecae
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_decl_in_switch.c
@@ -0,0 +1,24 @@
+/* Generated by Frama-C */
+int main(int argc, char **argv)
+{
+ int __retres;
+ __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_store_block((void *)(& argc),4UL);
+ {
+ int *p;
+ __e_acsl_store_block((void *)(& p),8UL);
+ switch (argc) {
+ default: ;
+ __e_acsl_full_init((void *)(& p));
+ p = & argc;
+ break;
+ }
+ __e_acsl_delete_block((void *)(& p));
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& argc));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
new file mode 100644
index 0000000000000000000000000000000000000000..897f45cce1a73daec858774c05a5077571ab97e6
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
@@ -0,0 +1,753 @@
+/* Generated by Frama-C */
+#include "stdlib.h"
+int goto_bts(void)
+{
+ int __retres;
+ int *p;
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ {
+ int a;
+ __e_acsl_store_block((void *)(& a),(size_t)4);
+ __e_acsl_full_init((void *)(& a));
+ a = 0;
+ __e_acsl_full_init((void *)(& p));
+ p = & a;
+ /*@ assert \valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",
+ (char *)"goto_bts",(char *)"\\valid(p)",13);
+ }
+ }
+ __e_acsl_delete_block((void *)(& a));
+ goto L;
+ __e_acsl_delete_block((void *)(& a));
+ }
+ L:
+ /*@ assert ¬\valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized_2;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_2;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
+ }
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",
+ (char *)"goto_bts",(char *)"!\\valid(p)",18);
+ }
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& p));
+ return __retres;
+}
+
+int goto_valid(void)
+{
+ int __retres;
+ int a;
+ int *p;
+ int *q;
+ int *r;
+ __e_acsl_store_block((void *)(& r),(size_t)8);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ a = 9;
+ {
+ int a1;
+ __e_acsl_store_block((void *)(& a1),(size_t)4);
+ __e_acsl_full_init((void *)(& a1));
+ a1 = 0;
+ __e_acsl_full_init((void *)(& p));
+ p = & a1;
+ {
+ int a2;
+ __e_acsl_store_block((void *)(& a2),(size_t)4);
+ __e_acsl_full_init((void *)(& a2));
+ a2 = 0;
+ __e_acsl_full_init((void *)(& q));
+ q = & a2;
+ {
+ int a3;
+ __e_acsl_store_block((void *)(& a3),(size_t)4);
+ __e_acsl_full_init((void *)(& a3));
+ a3 = 0;
+ __e_acsl_full_init((void *)(& r));
+ r = & a3;
+ __e_acsl_delete_block((void *)(& a2));
+ __e_acsl_delete_block((void *)(& a3));
+ goto FIRST;
+ __e_acsl_full_init((void *)(& p));
+ p = (int *)0;
+ { /* sequence */
+ __e_acsl_full_init((void *)(& q));
+ q = & a;
+ __e_acsl_full_init((void *)(& r));
+ r = q;
+ }
+ __e_acsl_delete_block((void *)(& a3));
+ __e_acsl_delete_block((void *)(& a2));
+ }
+ }
+ FIRST:
+ /*@ assert \valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",
+ (char *)"goto_valid",(char *)"\\valid(p)",46);
+ }
+ }
+ /*@ assert ¬\valid(q); */
+ {
+ {
+ int __gen_e_acsl_initialized_2;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& q),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_2;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&q); */
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
+ }
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",
+ (char *)"goto_valid",(char *)"!\\valid(q)",47);
+ }
+ }
+ /*@ assert ¬\valid(r); */
+ {
+ {
+ int __gen_e_acsl_initialized_3;
+ int __gen_e_acsl_and_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& r),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_3) {
+ int __gen_e_acsl_valid_3;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&r); */
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)r,sizeof(int));
+ __gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
+ }
+ else __gen_e_acsl_and_3 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_3,(char *)"Assertion",
+ (char *)"goto_valid",(char *)"!\\valid(r)",48);
+ }
+ }
+ __e_acsl_delete_block((void *)(& a1));
+ goto SECOND;
+ { /* sequence */
+ __e_acsl_full_init((void *)(& q));
+ q = & a;
+ __e_acsl_full_init((void *)(& r));
+ r = q;
+ __e_acsl_full_init((void *)(& p));
+ p = r;
+ }
+ __e_acsl_delete_block((void *)(& a1));
+ }
+ SECOND:
+ /*@ assert ¬\valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized_4;
+ int __gen_e_acsl_and_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_4) {
+ int __gen_e_acsl_valid_4;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
+ }
+ else __gen_e_acsl_and_4 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_4,(char *)"Assertion",
+ (char *)"goto_valid",(char *)"!\\valid(p)",56);
+ }
+ }
+ /*@ assert ¬\valid(q); */
+ {
+ {
+ int __gen_e_acsl_initialized_5;
+ int __gen_e_acsl_and_5;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& q),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_5) {
+ int __gen_e_acsl_valid_5;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&q); */
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
+ }
+ else __gen_e_acsl_and_5 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_5,(char *)"Assertion",
+ (char *)"goto_valid",(char *)"!\\valid(q)",57);
+ }
+ }
+ /*@ assert ¬\valid(r); */
+ {
+ {
+ int __gen_e_acsl_initialized_6;
+ int __gen_e_acsl_and_6;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& r),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_6) {
+ int __gen_e_acsl_valid_6;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&r); */
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)r,sizeof(int));
+ __gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
+ }
+ else __gen_e_acsl_and_6 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_6,(char *)"Assertion",
+ (char *)"goto_valid",(char *)"!\\valid(r)",58);
+ }
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& r));
+ __e_acsl_delete_block((void *)(& q));
+ __e_acsl_delete_block((void *)(& p));
+ return __retres;
+}
+
+int switch_valid(void)
+{
+ int __retres;
+ int i;
+ int *p;
+ int *q;
+ int *s;
+ __e_acsl_store_block((void *)(& s),(size_t)8);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& i),(size_t)4);
+ __e_acsl_full_init((void *)(& i));
+ i = 1;
+ __e_acsl_full_init((void *)(& s));
+ s = & i;
+ switch (i) {
+ default: ;
+ {
+ int a1;
+ __e_acsl_store_block((void *)(& a1),(size_t)4);
+ __e_acsl_full_init((void *)(& a1));
+ a1 = 0;
+ __e_acsl_full_init((void *)(& p));
+ p = & a1;
+ {
+ int a2;
+ __e_acsl_store_block((void *)(& a2),(size_t)4);
+ __e_acsl_full_init((void *)(& a2));
+ a2 = 0;
+ __e_acsl_full_init((void *)(& q));
+ q = & a2;
+ /*@ assert \valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",
+ (char *)"switch_valid",(char *)"\\valid(p)",76);
+ }
+ }
+ /*@ assert \valid(q); */
+ {
+ {
+ int __gen_e_acsl_initialized_2;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& q),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
+ }
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_2,(char *)"Assertion",
+ (char *)"switch_valid",(char *)"\\valid(q)",77);
+ }
+ }
+ /*@ assert \valid(s); */
+ {
+ {
+ int __gen_e_acsl_initialized_3;
+ int __gen_e_acsl_and_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& s),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_3) {
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)s,sizeof(int));
+ __gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
+ }
+ else __gen_e_acsl_and_3 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_3,(char *)"Assertion",
+ (char *)"switch_valid",(char *)"\\valid(s)",78);
+ }
+ }
+ __e_acsl_delete_block((void *)(& a1));
+ __e_acsl_delete_block((void *)(& a2));
+ break;
+ __e_acsl_delete_block((void *)(& a2));
+ }
+ { /* sequence */
+ __e_acsl_full_init((void *)(& q));
+ q = & i;
+ __e_acsl_full_init((void *)(& p));
+ p = q;
+ }
+ __e_acsl_full_init((void *)(& s));
+ s = (int *)0;
+ __e_acsl_delete_block((void *)(& a1));
+ }
+ }
+ /*@ assert ¬\valid(q); */
+ {
+ {
+ int __gen_e_acsl_initialized_4;
+ int __gen_e_acsl_and_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& q),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_4) {
+ int __gen_e_acsl_valid_4;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&q); */
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
+ }
+ else __gen_e_acsl_and_4 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_4,(char *)"Assertion",
+ (char *)"switch_valid",(char *)"!\\valid(q)",87);
+ }
+ }
+ /*@ assert ¬\valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized_5;
+ int __gen_e_acsl_and_5;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_5) {
+ int __gen_e_acsl_valid_5;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
+ }
+ else __gen_e_acsl_and_5 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_5,(char *)"Assertion",
+ (char *)"switch_valid",(char *)"!\\valid(p)",88);
+ }
+ }
+ /*@ assert \valid(s); */
+ {
+ {
+ int __gen_e_acsl_initialized_6;
+ int __gen_e_acsl_and_6;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& s),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_6) {
+ int __gen_e_acsl_valid_6;
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)s,sizeof(int));
+ __gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
+ }
+ else __gen_e_acsl_and_6 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_6,(char *)"Assertion",
+ (char *)"switch_valid",(char *)"\\valid(s)",89);
+ }
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& s));
+ __e_acsl_delete_block((void *)(& q));
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_delete_block((void *)(& i));
+ return __retres;
+}
+
+int while_valid(void)
+{
+ int __retres;
+ int *p;
+ int *q;
+ int *r;
+ int i;
+ __e_acsl_store_block((void *)(& r),(size_t)8);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ i = 5;
+ {
+ int a0;
+ __e_acsl_store_block((void *)(& a0),(size_t)4);
+ __e_acsl_full_init((void *)(& a0));
+ a0 = 0;
+ __e_acsl_full_init((void *)(& r));
+ r = & a0;
+ while (1) {
+ i --;
+ if (! i) break;
+ {
+ int a1;
+ __e_acsl_store_block((void *)(& a1),(size_t)4);
+ __e_acsl_full_init((void *)(& a1));
+ a1 = 0;
+ __e_acsl_full_init((void *)(& p));
+ p = & a1;
+ {
+ int a2;
+ __e_acsl_store_block((void *)(& a2),(size_t)4);
+ __e_acsl_full_init((void *)(& a2));
+ a2 = 0;
+ __e_acsl_full_init((void *)(& q));
+ q = & a2;
+ /*@ assert \valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",
+ (char *)"while_valid",(char *)"\\valid(p)",108);
+ }
+ }
+ /*@ assert \valid(q); */
+ {
+ {
+ int __gen_e_acsl_initialized_2;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& q),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
+ }
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_2,(char *)"Assertion",
+ (char *)"while_valid",(char *)"\\valid(q)",109);
+ }
+ }
+ /*@ assert \valid(r); */
+ {
+ {
+ int __gen_e_acsl_initialized_3;
+ int __gen_e_acsl_and_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& r),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_3) {
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)r,sizeof(int));
+ __gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
+ }
+ else __gen_e_acsl_and_3 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_3,(char *)"Assertion",
+ (char *)"while_valid",(char *)"\\valid(r)",110);
+ }
+ }
+ if (! i) {
+ __e_acsl_delete_block((void *)(& a1));
+ __e_acsl_delete_block((void *)(& a2));
+ break;
+ }
+ __e_acsl_delete_block((void *)(& a2));
+ __e_acsl_delete_block((void *)(& a1));
+ }
+ }
+ }
+ /*@ assert ¬\valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized_4;
+ int __gen_e_acsl_and_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_4) {
+ int __gen_e_acsl_valid_4;
+ /*@ assert Value: initialisation: \initialized(&p); */
+ /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
+ }
+ else __gen_e_acsl_and_4 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_4,(char *)"Assertion",
+ (char *)"while_valid",(char *)"!\\valid(p)",116);
+ }
+ }
+ /*@ assert ¬\valid(q); */
+ {
+ {
+ int __gen_e_acsl_initialized_5;
+ int __gen_e_acsl_and_5;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& q),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_5) {
+ int __gen_e_acsl_valid_5;
+ /*@ assert Value: initialisation: \initialized(&q); */
+ /*@ assert Value: dangling_pointer: ¬\dangling(&q); */
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
+ }
+ else __gen_e_acsl_and_5 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_5,(char *)"Assertion",
+ (char *)"while_valid",(char *)"!\\valid(q)",117);
+ }
+ }
+ /*@ assert \valid(r); */
+ {
+ {
+ int __gen_e_acsl_initialized_6;
+ int __gen_e_acsl_and_6;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& r),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_6) {
+ int __gen_e_acsl_valid_6;
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)r,sizeof(int));
+ __gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
+ }
+ else __gen_e_acsl_and_6 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_6,(char *)"Assertion",
+ (char *)"while_valid",(char *)"\\valid(r)",118);
+ __e_acsl_delete_block((void *)(& a0));
+ }
+ }
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& r));
+ __e_acsl_delete_block((void *)(& q));
+ __e_acsl_delete_block((void *)(& p));
+ return __retres;
+}
+
+void continue_valid(void)
+{
+ int i;
+ int *p;
+ int *q;
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ i = 0;
+ while (1) {
+ int tmp;
+ { /* sequence */
+ tmp = i;
+ i ++;
+ ;
+ }
+ if (! tmp) break;
+ {
+ int a1;
+ __e_acsl_store_block((void *)(& a1),(size_t)4);
+ /*@ assert ¬\valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(! __gen_e_acsl_and,(char *)"Assertion",
+ (char *)"continue_valid",(char *)"!\\valid(p)",130);
+ }
+ }
+ /*@ assert ¬\valid(q); */
+ {
+ {
+ int __gen_e_acsl_initialized_2;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& q),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
+ }
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",
+ (char *)"continue_valid",(char *)"!\\valid(q)",131);
+ }
+ }
+ __e_acsl_full_init((void *)(& a1));
+ a1 = 1;
+ __e_acsl_full_init((void *)(& p));
+ p = & a1;
+ /*@ assert \valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized_3;
+ int __gen_e_acsl_and_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_3) {
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
+ }
+ else __gen_e_acsl_and_3 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_3,(char *)"Assertion",
+ (char *)"continue_valid",(char *)"\\valid(p)",135);
+ }
+ }
+ /*@ assert ¬\valid(q); */
+ {
+ {
+ int __gen_e_acsl_initialized_4;
+ int __gen_e_acsl_and_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& q),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_4) {
+ int __gen_e_acsl_valid_4;
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
+ }
+ else __gen_e_acsl_and_4 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_4,(char *)"Assertion",
+ (char *)"continue_valid",(char *)"!\\valid(q)",136);
+ }
+ }
+ {
+ int a2;
+ __e_acsl_store_block((void *)(& a2),(size_t)4);
+ __e_acsl_full_init((void *)(& a2));
+ a2 = 1;
+ __e_acsl_full_init((void *)(& q));
+ q = & a2;
+ /*@ assert \valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized_5;
+ int __gen_e_acsl_and_5;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_5) {
+ int __gen_e_acsl_valid_5;
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
+ }
+ else __gen_e_acsl_and_5 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_5,(char *)"Assertion",
+ (char *)"continue_valid",(char *)"\\valid(p)",
+ 141);
+ }
+ }
+ /*@ assert \valid(q); */
+ {
+ {
+ int __gen_e_acsl_initialized_6;
+ int __gen_e_acsl_and_6;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& q),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_6) {
+ int __gen_e_acsl_valid_6;
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
+ }
+ else __gen_e_acsl_and_6 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_6,(char *)"Assertion",
+ (char *)"continue_valid",(char *)"\\valid(q)",
+ 142);
+ }
+ }
+ __e_acsl_delete_block((void *)(& a1));
+ __e_acsl_delete_block((void *)(& a2));
+ continue;
+ __e_acsl_delete_block((void *)(& a2));
+ }
+ if (i == 5) {
+ __e_acsl_delete_block((void *)(& a1));
+ break;
+ }
+ __e_acsl_delete_block((void *)(& a1));
+ }
+ }
+ /*@ assert ¬\valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized_7;
+ int __gen_e_acsl_and_7;
+ __gen_e_acsl_initialized_7 = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_7) {
+ int __gen_e_acsl_valid_7;
+ __gen_e_acsl_valid_7 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and_7 = __gen_e_acsl_valid_7;
+ }
+ else __gen_e_acsl_and_7 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_7,(char *)"Assertion",
+ (char *)"continue_valid",(char *)"!\\valid(p)",150);
+ }
+ }
+ /*@ assert ¬\valid(q); */
+ {
+ {
+ int __gen_e_acsl_initialized_8;
+ int __gen_e_acsl_and_8;
+ __gen_e_acsl_initialized_8 = __e_acsl_initialized((void *)(& q),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_8) {
+ int __gen_e_acsl_valid_8;
+ __gen_e_acsl_valid_8 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_and_8 = __gen_e_acsl_valid_8;
+ }
+ else __gen_e_acsl_and_8 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_8,(char *)"Assertion",
+ (char *)"continue_valid",(char *)"!\\valid(q)",151);
+ }
+ }
+ __e_acsl_delete_block((void *)(& q));
+ __e_acsl_delete_block((void *)(& p));
+ return;
+}
+
+int main(int argc, char const **argv)
+{
+ int __retres;
+ __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
+ goto_bts();
+ goto_valid();
+ switch_valid();
+ while_valid();
+ continue_valid();
+ __retres = 0;
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
index 765047ff16e0e909eb56009920a832a684b0e1c1..3e2f38a1e00738a66d4de878512397bbfb618c57 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
@@ -10,8 +10,8 @@ int main(int argc, char **argv)
{
{
int __gen_e_acsl_valid;
- __e_acsl_store_block((void *)(& argc),(size_t)4);
__e_acsl_store_block((void *)(& argv),(size_t)8);
+ __e_acsl_store_block((void *)(& argc),(size_t)4);
__gen_e_acsl_valid = __e_acsl_valid((void *)(& argc),sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&argc)",10);
@@ -185,8 +185,8 @@ int main(int argc, char **argv)
i ++;
}
__retres = 0;
- __e_acsl_delete_block((void *)(& argc));
__e_acsl_delete_block((void *)(& argv));
+ __e_acsl_delete_block((void *)(& argc));
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index dc9997ed37d194ff5427f6819e16a43de98bdcec..3924bdcb7e46c82bd90df9458537622d5468fb95 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -26,28 +26,6 @@ open Cil_datatype
let dkey = Options.dkey_translation
-let allocate_function env kf =
- List.fold_left
- (fun env vi ->
- if Mmodel_analysis.must_model_vi ~kf vi then
- let vi = Cil.get_varinfo (Env.get_behavior env) vi in
- Env.add_stmt env (Misc.mk_store_stmt vi)
- else
- env)
- env
- (Kernel_function.get_formals kf)
-
-let deallocate_function env kf =
- List.fold_left
- (fun env vi ->
- if Mmodel_analysis.must_model_vi ~kf vi then
- let vi = Cil.get_varinfo (Env.get_behavior env) vi in
- Env.add_stmt env (Misc.mk_delete_stmt vi)
- else
- env)
- env
- (Kernel_function.get_formals kf)
-
(* ************************************************************************** *)
(* Visitor *)
(* ************************************************************************** *)
@@ -57,10 +35,71 @@ let function_env = ref Env.dummy
let dft_funspec = Cil.empty_funspec ()
let funspec = ref dft_funspec
+(* extend the environment with statements which allocate/deallocate memory
+ blocks *)
+module Memory: sig
+ val store: ?before:stmt -> Env.t -> kernel_function -> varinfo list -> Env.t
+ val duplicate_store:
+ ?before:stmt -> Env.t -> kernel_function -> Varinfo.Set.t -> Env.t
+ val delete_from_list:
+ ?before:stmt -> Env.t -> kernel_function -> varinfo list -> Env.t
+ val delete_from_set:
+ ?before:stmt -> Env.t -> kernel_function -> Varinfo.Set.t -> Env.t
+end = struct
+
+ let tracking_stmt ?before fold mk_stmt env kf vars =
+ fold
+ (fun vi env ->
+ if Mmodel_analysis.must_model_vi ~kf vi then
+ let vi = Cil.get_varinfo (Env.get_behavior env) vi in
+ Env.add_stmt ?before env (mk_stmt vi)
+ else
+ env)
+ vars
+ env
+
+ let store ?before env kf vars =
+ tracking_stmt
+ ?before
+ List.fold_right (* small list *)
+ Misc.mk_store_stmt
+ env
+ kf
+ vars
+
+ let duplicate_store ?before env kf vars =
+ tracking_stmt
+ ?before
+ Varinfo.Set.fold
+ Misc.mk_duplicate_store_stmt
+ env
+ kf
+ vars
+
+ let delete_from_list ?before env kf vars =
+ tracking_stmt
+ ?before
+ List.fold_right (* small list *)
+ Misc.mk_delete_stmt
+ env
+ kf
+ vars
+
+ let delete_from_set ?before env kf vars =
+ tracking_stmt
+ ?before
+ Varinfo.Set.fold
+ Misc.mk_delete_stmt
+ env
+ kf
+ vars
+
+end
+
(* the main visitor performing e-acsl checking and C code generator *)
class e_acsl_visitor prj generate = object (self)
- inherit Visitor.generic_frama_c_visitor
+ inherit Visitor.generic_frama_c_visitor
(if generate then Cil.copy_visit prj else Cil.inplace_visit ())
val mutable main_fct = None
@@ -246,7 +285,8 @@ class e_acsl_visitor prj generate = object (self)
f.globals <- new_globals
| None ->
Kernel.warning "@[no entry point specified:@ \
-you must call function `__e_acsl_memory_init` by yourself.@]";
+you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
+ fname;
f.globals <- f.globals @ [ cil_fct ]
in
Project.on prj build_initializer ()
@@ -327,7 +367,7 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
see bts #1392 *)
if vi.vstorage <> Extern then
vi.vghost <- false
- | _ ->
+ | _ ->
()
in
(match g with
@@ -391,33 +431,35 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
f.sbody.blocals <- blocks
method !vfunc f =
- if generate then
+ if generate then begin
+ Exit_points.generate f;
let kf = Extlib.the self#current_kf in
- Options.feedback ~dkey ~level:2 "entering in function %a."
+ Options.feedback ~dkey ~level:2 "entering in function %a."
Kernel_function.pretty kf;
List.iter (fun vi -> vi.vghost <- false) f.slocals;
- Cil.DoChildrenPost
- (fun f ->
- self#add_generated_variables_in_function f;
+ Cil.DoChildrenPost
+ (fun f ->
+ Exit_points.clear ();
+ self#add_generated_variables_in_function f;
Options.feedback ~dkey ~level:2 "function %a done."
Kernel_function.pretty kf;
f)
- else
+ end else
Cil.DoChildren
- method private is_return old_kf stmt =
- let old_ret =
+ method private is_return old_kf stmt =
+ let old_ret =
try Kernel_function.find_return old_kf
with Kernel_function.No_Statement -> assert false
in
Stmt.equal stmt (Cil.get_stmt self#behavior old_ret)
method private is_first_stmt old_kf stmt =
- try
+ try
Stmt.equal
- (Cil.get_original_stmt self#behavior stmt)
+ (Cil.get_original_stmt self#behavior stmt)
(Kernel_function.find_first_stmt old_kf)
- with Kernel_function.No_Statement ->
+ with Kernel_function.No_Statement ->
assert false
method private is_main old_kf =
@@ -427,7 +469,7 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
with Globals.No_such_entry_point _s ->
(* [JS 2013/05/21] already a warning in pre-analysis *)
(* Options.warning ~once:true "%s@ \
- @[The generated program may be incomplete.@]"
+ @[The generated program may be incomplete.@]"
s;*)
false
@@ -462,14 +504,14 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
Literal_strings.add s vi;
env_ref := env;
Cil.ChangeTo exp)
- | _ ->
+ | _ ->
Cil.DoChildren
end in
let e = Cil.visitCilExpr o e in
e, !env_ref
method !vstmt_aux stmt =
- Options.debug ~level:4 "proceeding stmt (sid %d) %a@."
+ Options.debug ~level:4 "proceeding stmt (sid %d) %a@."
stmt.sid Stmt.pretty stmt;
let kf = Extlib.the self#current_kf in
let is_main = self#is_main kf in
@@ -478,10 +520,13 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
| Loop _ -> Env.push_loop env
| _ -> env
in
- let env =
+ let env =
if self#is_first_stmt kf stmt then
(* JS: should be done in the new project? *)
- let env = if generate then allocate_function env kf else env in
+ let env =
+ if generate then Memory.store env kf (Kernel_function.get_formals kf)
+ else env
+ in
(* translate the precondition of the function *)
if Dup_functions.is_generated (Extlib.the self#current_kf) then
Project.on prj (Translate.translate_pre_spec kf Kglobal env) !funspec
@@ -490,25 +535,37 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
else
env
in
+
let env, new_annots =
Annotations.fold_code_annot
- (fun _ old_a (env, new_annots) ->
+ (fun _ old_a (env, new_annots) ->
let a =
(* [VP] Don't use Visitor here, as it will fill the queue in the
middle of the computation... *)
Cil.visitCilCodeAnnotation (self :> Cil.cilVisitor) old_a
in
- let env =
+ let env =
Project.on
prj
(Translate.translate_pre_code_annotation kf stmt env)
- a
+ a
in
env, a :: new_annots)
(Cil.get_original_stmt self#behavior stmt)
(env, [])
in
+
+ (* Add [__e_acsl_store_duplicate] calls for local variables which
+ * declarations are bypassed by gotos. Note: should be done before
+ * [vinst] method (which adds initializers) is executed, otherwise
+ * init calls appear before store calls. *)
+ let duplicates = Exit_points.store_vars stmt in
+ let env =
+ if generate then Memory.duplicate_store ~before:stmt env kf duplicates
+ else env
+ in
function_env := env;
+
let mk_block stmt =
(* be careful: since this function is called in a post action, [env] has
been modified from the time where pre actions have been executed.
@@ -524,39 +581,50 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
env
in
let mk_post_env env =
- (* [fold_right] to preserve order of generation of pre_conditions *)
+ (* [fold_right] to preserve order of generation of pre_conditions *)
Project.on
prj
(List.fold_right
- (fun a env ->
+ (fun a env ->
Translate.translate_post_code_annotation kf stmt env a)
new_annots)
env
in
(* handle loop invariants *)
let new_stmt, env, must_mv = Loops.preserve_invariant prj env kf stmt in
- let new_stmt, env =
- if self#is_return kf stmt then
+ let new_stmt, env =
+ (* Remove local variables which scopes ended via goto/break/continue. *)
+ let del_vars = Exit_points.delete_vars stmt in
+ let env =
+ if generate then Memory.delete_from_set ~before:stmt env kf del_vars
+ else env
+ in
+ if self#is_return kf stmt then
(* must generate the post_block before including [stmt] (the 'return')
since no code is executed after it. However, since this statement
is pure (Cil invariant), that is semantically correct. *)
let env = mk_post_env env in
(* also handle the postcondition of the function and clear the env *)
- let env =
+ let env =
if Dup_functions.is_generated (Extlib.the self#current_kf) then
Project.on
prj
- (Translate.translate_post_spec kf Kglobal env)
- !funspec
+ (Translate.translate_post_spec kf Kglobal env)
+ !funspec
else
env
in
(* de-allocating memory previously allocating by the kf *)
(* JS: should be done in the new project? *)
if generate then
- let env = deallocate_function env kf in
- let b, env =
- Env.pop_and_get env new_stmt ~global_clear:true Env.After
+ (* Remove recorded function arguments *)
+ let fargs = Kernel_function.get_formals kf in
+ let env =
+ if generate then Memory.delete_from_list env kf fargs
+ else env
+ in
+ let b, env =
+ Env.pop_and_get env new_stmt ~global_clear:true Env.After
in
if is_main && Mmodel_analysis.use_model () then begin
let stmts = b.bstmts in
@@ -627,8 +695,8 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
| Var vi, NoOffset -> vi.vglob || vi.vformal
| _ -> false
in
-(* Options.feedback "%a? %a (%b && %b)"
- Printer.pp_lval assigned_lv
+(* Options.feedback "%a? %a (%b && %b)"
+ Printer.pp_lval assigned_lv
Printer.pp_lval checked_lv
(not (may_safely_ignore assigned_lv))
(Pre_analysis.must_model_lval ~kf ~stmt checked_lv);*)
@@ -649,10 +717,10 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
method !vinst = function
| Set(old_lv, _, _) ->
if generate then
- Cil.DoChildrenPost
- (function
- | [ Set(new_lv, _, loc) ] as l ->
- self#add_initializer loc old_lv new_lv;
+ Cil.DoChildrenPost
+ (function
+ | [ Set(new_lv, _, loc) ] as l ->
+ self#add_initializer loc old_lv new_lv;
l
| _ -> assert false)
else
@@ -661,9 +729,9 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
if not generate || Misc.is_generated_kf (Extlib.the self#current_kf) then
Cil.DoChildren
else
- Cil.DoChildrenPost
- (function
- | [ Call(Some new_ret, _, _, loc) ] as l ->
+ Cil.DoChildrenPost
+ (function
+ | [ Call(Some new_ret, _, _, loc) ] as l ->
self#add_initializer loc old_ret new_ret;
l
| _ -> assert false)
@@ -671,7 +739,7 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
Cil.DoChildren
method !vblock blk =
- let handle_memory new_blk =
+ let handle_memory new_blk =
match new_blk.blocals with
| [] -> new_blk
| _ :: _ ->
@@ -690,7 +758,7 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
| { skind = Return _ } as ret :: ((potential_clean :: tl) as l) ->
(* keep the return (enclosed in a generated block) at the end;
preceded by clean if any *)
- let init, tl =
+ let init, tl =
if self#is_main kf && Mmodel_analysis.use_model () then
[ potential_clean; ret ], tl
else
@@ -698,15 +766,15 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
in
blk.bstmts <-
List.fold_left (fun acc v -> v :: acc) (add_locals init) tl
- | { skind = Block b } :: _ ->
+ | { skind = Block b } :: _ ->
insert_in_innermost_last_block b (List.rev b.bstmts)
- | l -> blk.bstmts <-
+ | l -> blk.bstmts <-
List.fold_left (fun acc v -> v :: acc) (add_locals []) l
in
insert_in_innermost_last_block new_blk (List.rev new_blk.bstmts);
new_blk.bstmts <-
List.fold_left
- (fun acc vi ->
+ (fun acc vi ->
if Mmodel_analysis.must_model_vi vi then
let vi = Cil.get_varinfo self#behavior vi in
Misc.mk_store_stmt vi :: acc
@@ -764,11 +832,11 @@ end
let do_visit ?(prj=Project.current ()) generate =
(* The main visitor proceeds by tracking declarations belonging to the
E-ACSL runtime library and then using these declarations to generate
- statements used in instrumentation. The following code reorders AST
- so declarations belonging to E-ACSL library appear atop of any location
+ statements used in instrumentation. The following code reorders AST
+ so declarations belonging to E-ACSL library appear atop of any location
requiring instrumentation. *)
- Misc.reorder_ast ();
- Options.feedback ~level:2 "%s annotations in %a."
+ Misc.reorder_ast ();
+ Options.feedback ~level:2 "%s annotations in %a."
(if generate then "translating" else "checking")
Project.pretty prj;
let vis =