diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle
index efd924c556296cc37747d56a5a72f0bae13e0177..cefeb276e61b9907bda3ef2e074dc0f0f3f7085d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle
@@ -10,7 +10,7 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
- S ∈ {0}
+ S ∈ {{ "foo" }}
__e_acsl_literal_string ∈ {0}
__e_acsl_literal_string_2 ∈ {0}
__e_acsl_literal_string_3 ∈ {0}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
index efd924c556296cc37747d56a5a72f0bae13e0177..cefeb276e61b9907bda3ef2e074dc0f0f3f7085d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
@@ -10,7 +10,7 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
- S ∈ {0}
+ S ∈ {{ "foo" }}
__e_acsl_literal_string ∈ {0}
__e_acsl_literal_string_2 ∈ {0}
__e_acsl_literal_string_3 ∈ {0}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index 918ee7158336f8488f8767940f26c1ccd6a6c5f7..32445cb1f02704a681cefc0a633a3b5df006e254 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -86,7 +86,7 @@ extern size_t __memory_size;
predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
-char *S;
+char *S = (char *)"foo";
int f(void)
{
int __retres;
@@ -155,7 +155,6 @@ void __e_acsl_memory_init(void)
__literal_string((void *)__e_acsl_literal_string_2);
__store_block((void *)(& S),4U);
__full_init((void *)(& S));
- S = (char *)__e_acsl_literal_string;
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
index 5cbdd9a0e2b10458db2c4729b715aa3bd26d603d..ec689d560787bfd68d91ecffbbb85fc06b802764 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
@@ -89,7 +89,7 @@ predicate diffSize{L1, L2}(ℤ i) =
*/
int main(void);
-char *T;
+char *T = (char *)"bar";
int G = 0;
void f(void)
{
@@ -106,8 +106,8 @@ void f(void)
return;
}
-char *S;
-char *S2;
+char *S = (char *)"foo";
+char *S2 = (char *)"foo2";
int IDX = 1;
int G2 = 2;
char *U = (char *)"baz";
@@ -131,13 +131,10 @@ void __e_acsl_memory_init(void)
__literal_string((void *)__e_acsl_literal_string_2);
__store_block((void *)(& S2),4U);
__full_init((void *)(& S2));
- S2 = (char *)__e_acsl_literal_string_4;
__store_block((void *)(& S),4U);
__full_init((void *)(& S));
- S = (char *)__e_acsl_literal_string_3;
__store_block((void *)(& T),4U);
__full_init((void *)(& T));
- T = (char *)__e_acsl_literal_string_2;
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
index d5bb4999c2dc6591705bfcf661b341809840aa94..97cb30890d153325e4c7dbc38086c731c0bd5b83 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
@@ -112,7 +112,7 @@ predicate diffSize{L1, L2}(ℤ i) =
*/
int main(void);
-char *T;
+char *T = (char *)"bar";
int G = 0;
void f(void)
{
@@ -134,8 +134,8 @@ void f(void)
return;
}
-char *S;
-char *S2;
+char *S = (char *)"foo";
+char *S2 = (char *)"foo2";
int IDX = 1;
int G2 = 2;
char *U = (char *)"baz";
@@ -159,13 +159,10 @@ void __e_acsl_memory_init(void)
__literal_string((void *)__e_acsl_literal_string_2);
__store_block((void *)(& S2),4U);
__full_init((void *)(& S2));
- S2 = (char *)__e_acsl_literal_string_4;
__store_block((void *)(& S),4U);
__full_init((void *)(& S));
- S = (char *)__e_acsl_literal_string_3;
__store_block((void *)(& T),4U);
__full_init((void *)(& T));
- T = (char *)__e_acsl_literal_string_2;
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle
index 076a517b7e7e4ec7e44ac0a41bcfc2bdaf065d84..c04d9a8f696904fa8df6921de8706b24764cdf10 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle
@@ -10,10 +10,10 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
- T ∈ {0}
+ T ∈ {{ "bar" }}
G ∈ {0}
- S ∈ {0}
- S2 ∈ {0}
+ S ∈ {{ "foo" }}
+ S2 ∈ {{ "foo2" }}
IDX ∈ {1}
G2 ∈ {2}
U ∈ {{ "baz" }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
index 7f69a2e063cfbc0fe4d453055ab4cd0de56c20b8..dcdcf9a030ef2a43fcafc5365d2b28e72ff0bb33 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
@@ -10,10 +10,10 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
- T ∈ {0}
+ T ∈ {{ "bar" }}
G ∈ {0}
- S ∈ {0}
- S2 ∈ {0}
+ S ∈ {{ "foo" }}
+ S2 ∈ {{ "foo2" }}
IDX ∈ {1}
G2 ∈ {2}
U ∈ {{ "baz" }}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index bbb5bc6fff1713914195892336d5a763fe3ec29c..2c4a785a2ad57ed7ffb38c243791438e83db0b75 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -84,19 +84,19 @@ class e_acsl_visitor prj generate = object (self)
visited *)
val mutable is_initializer = false
- (* Global flag set to a [true] value if a currently visited node
- belongs to a global initialiser and set to [false] otherwise *)
+ (* Global flag set to [true] if a currently visited node
+ belongs to a global initializer and set to [false] otherwise *)
val global_vars: init option Varinfo.Hashtbl.t = Varinfo.Hashtbl.create 7
- (* A hashtable mapping global variables (as Cil_type.varinfo) to their
- initialisers aiming to capture memory allocated by global variable
+ (* Hashtable mapping global variables (as Cil_type.varinfo) to their
+ initializers aiming to capture memory allocated by global variable
declarations and initilisation. At runtime the memory blocks corresponding
- to space occupied by global recorded via a call to [__e_acsl_memory_init]
- instrumented before anything (or almost anything) else in the [main]
- function. Each variable (say V) stored by [global_vars] will be handled in
+ to space occupied by global are recorded via a call to
+ [__e_acsl_memory_init] instrumented before (almost) anything else in the
+ [main] function. Each variable stored by [global_vars] will be handled in
the body of [__e_acsl_memory_init] as follows:
__store_block(...); // Record a memory block used by the variable
- __full_init(...); // ... and mark it as initialised memory
+ __full_init(...); // ... and mark it as initialized memory
NOTE: In [global_vars] keys belong to the original project while values
belong to the new one *)
@@ -144,11 +144,11 @@ class e_acsl_visitor prj generate = object (self)
Varinfo.Hashtbl.fold_sorted
(fun old_vi i (stmts, env) ->
let new_vi = Cil.get_varinfo self#behavior old_vi in
- (* Function that creates an initialisation statement
+ (* [model] creates an initialization statement
of the form [__full_init(...)]) for every global
- variable which needs to be tracked and is not a frama-C
- builtin and further appends it to the given list of
- statements ([blk]) *)
+ variable which needs to be tracked and is not a Frama-C
+ builtin. Further the statement is appended to the provided
+ list of statements ([blk]) *)
let model blk =
if Mmodel_analysis.must_model_vi old_vi then
let blk =
@@ -166,7 +166,7 @@ class e_acsl_visitor prj generate = object (self)
| None -> model stmts, env
| Some (CompoundInit _) -> assert false
| Some (SingleInit e) ->
- let _, env = self#literal_string env e in stmts, env)
+ let _, env = self#literal_string env e in stmts, env)
global_vars
([ return ], env)
in
@@ -184,7 +184,7 @@ class e_acsl_visitor prj generate = object (self)
:: stmts)
stmts
in
- (* Create a new code block with generated sstatements *)
+ (* Create a new code block with generated statements *)
let (b, env), stmts = match stmts with
| [] -> assert false
| stmt :: stmts ->
@@ -194,9 +194,9 @@ class e_acsl_visitor prj generate = object (self)
let stmts = Cil.mkStmt ~valid_sid:true (Block b) :: stmts in
let blk = Cil.mkBlock stmts in
(* Create [__e_acsl_memory_init] function with definition
- for initialisation of global variables *)
+ for initialization of global variables *)
let fname = "__e_acsl_memory_init" in
- let vi = (* Name and type of the function *)
+ let vi =
Cil.makeGlobalVar ~source:true
fname
(TFun(Cil.voidType, Some [], false, []))
@@ -205,7 +205,7 @@ class e_acsl_visitor prj generate = object (self)
(* There is no contract associated with the function *)
let spec = Cil.empty_funspec () in
(* Create function definition which has the list of the
- * generated initialisation statements *)
+ * generated initialization statements *)
let fundec =
{ svar = vi;
sformals = [];
@@ -337,18 +337,17 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in
(match g with
| GVar(vi, _, _) | GVarDecl(vi, _) ->
+ (* Make a unique mapping for each global variable omitting initializers.
+ Initializers (used to capture literal strings) are added to
+ [global_vars] via the [vinit] visitor method (see comments below). *)
Varinfo.Hashtbl.replace global_vars vi None
| _ -> ());
if generate then Cil.DoChildrenPost(fun g -> List.iter do_it g; g)
else Cil.DoChildren
- (* Process global variable initialisers and add mappings from global
- variables to their initialisers to [global_vars]. Note that [add] method
- should be used instead [replace]. This is because a single variable can
- be assicoated with multiple initialisers and all of them need to be
- captured. Also note that the below function captures only [SingleInit]s.
- All compound initialisers (which contain single ones) are unrapped and
- thrown away. *)
+ (* Add mappings from global variables to their initializers to [global_vars].
+ Note that the below function captures only [SingleInit]s. All compound
+ initializers (which contain single ones) are unrapped and thrown away. *)
method !vinit vi _off _i =
if generate then
if Mmodel_analysis.must_model_vi vi then begin
@@ -356,6 +355,9 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
Cil.DoChildrenPost
(fun i ->
(match is_initializer with
+ (* Note the use of [add] instead [replace]. This is because a
+ single variable can be associated with multiple initializers
+ and all of them need to be captured. *)
| true -> Varinfo.Hashtbl.add global_vars vi (Some i)
| false-> ());
is_initializer <- false;
@@ -572,17 +574,16 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
| ret :: l ->
let loc = Stmt.loc stmt in
let delete_stmts =
- Varinfo.Hashtbl.fold
+ Varinfo.Hashtbl.fold_sorted
(fun old_vi i acc ->
if Mmodel_analysis.must_model_vi old_vi then
let new_vi = Cil.get_varinfo self#behavior old_vi in
(* Since there are multiple entries for same variables
- do delete only variables without initialisers, this
+ do delete only variables without initializers, this
ensures that each variable is released once only *)
(match i with
- | None -> Misc.mk_delete_stmt new_vi :: acc
- | _ -> acc
- )
+ | None -> Misc.mk_delete_stmt new_vi :: acc
+ | Some _ -> acc)
else
acc)
global_vars
@@ -723,15 +724,15 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in the code with variables generated by E-ACSL. *)
method !vexpr _ =
if generate then begin
- match is_initializer with
- (* Do not touch global initialisers because they accept only constants *)
- | true -> Cil.DoChildren
- (* Replace literal strings elsewhere *)
- | false -> Cil.DoChildrenPost
- (fun e ->
- let e, env = self#literal_string !function_env e in
- function_env := env;
- e)
+ match is_initializer with
+ (* Do not touch global initializers because they accept only constants *)
+ | true -> Cil.DoChildren
+ (* Replace literal strings elsewhere *)
+ | false -> Cil.DoChildrenPost
+ (fun e ->
+ let e, env = self#literal_string !function_env e in
+ function_env := env;
+ e)
end else
Cil.SkipChildren
@@ -761,7 +762,6 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
Literal_strings.reset ();
self#reset_env ();
Translate.set_original_project (Project.current ())
-
end
let do_visit ?(prj=Project.current ()) generate =