diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index 04cb8cbdf7534223386e6d7ad5e7ab96680c50fc..15d4cac23157437357e95845df2697bc0d418868 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -36,7 +36,7 @@ int main(void)
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int t[7] = {1, 4, 4, 5, 5, 5, 7};
__e_acsl_store_block((void *)(t),(size_t)28);
- __e_acsl_full_init((void *)(t));
+ __e_acsl_full_init((void *)(& t));
int n = __gen_e_acsl_sorted(t,7);
/*@ assert n ≡ 1; */
__e_acsl_assert(n == 1,(char *)"Assertion",(char *)"main",(char *)"n == 1",
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 847be00d2729b5edcb71933b1e8656473daeabcf..b8273d8fe62fad816e8a98579fdff5eab734b89d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -37,7 +37,7 @@ int main(void)
__e_acsl_store_block((void *)(& av),(size_t)4);
ArrayInt Accel = {1, 2, 3, 4, 5};
__e_acsl_store_block((void *)(Accel),(size_t)20);
- __e_acsl_full_init((void *)(Accel));
+ __e_acsl_full_init((void *)(& Accel));
__gen_e_acsl_atp_NORMAL_computeAverageAccel(& Accel,& av);
__retres = 0;
__e_acsl_delete_block((void *)(& av));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
index cda25d31466dad9c290dc6e5870580e699913ebc..d616deab77b69cd695ddae705aa16fcba506a23d 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
@@ -62,7 +62,7 @@ int main(void)
}
int a[4] = {1, 2, 3, 4};
__e_acsl_store_block((void *)(a),(size_t)16);
- __e_acsl_full_init((void *)(a));
+ __e_acsl_full_init((void *)(& a));
__e_acsl_full_init((void *)(& pa));
pa = (int *)(& a);
/*@ assert \base_addr((int *)a) ≡ \base_addr(pa); */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
index a26e60fdf22c9643de34d842124db5e412e8bf71..ff65273e6fdea736066d7924a505856a50f9c6d1 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
@@ -77,7 +77,7 @@ int main(void)
}
int a[4] = {1, 2, 3, 4};
__e_acsl_store_block((void *)(a),(size_t)16);
- __e_acsl_full_init((void *)(a));
+ __e_acsl_full_init((void *)(& a));
int *pa = (int *)(& a);
__e_acsl_store_block((void *)(& pa),(size_t)8);
__e_acsl_full_init((void *)(& pa));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
index e2289b74086b7f54ca23111674f7e2ab14e58df1..617b202e126d1c1dcc236e2c6fa7fd74c4e08ca6 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
@@ -48,7 +48,7 @@ int main(void)
}
int a[4] = {1, 2, 3, 4};
__e_acsl_store_block((void *)(a),(size_t)16);
- __e_acsl_full_init((void *)(a));
+ __e_acsl_full_init((void *)(& a));
/*@ assert \offset((int *)a) ≡ 0; */
{
int __gen_e_acsl_offset_5;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
index ecf41c7d55ec8f48443d951445a2cc4d0f5e1320..9905156012e38f80d2b53e035a64bde39be56bcd 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
@@ -9,7 +9,7 @@ int main(void)
__e_acsl_full_init((void *)(& x));
int t[3] = {2, 3, 4};
__e_acsl_store_block((void *)(t),(size_t)12);
- __e_acsl_full_init((void *)(t));
+ __e_acsl_full_init((void *)(& t));
int *p = & x;
__e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 87fa598c447d74499a9dd942d8fe8bab5d5ea3d7..408339a86df360db46d4fab5a41c652183a325ba 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -579,6 +579,14 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
been modified from the time where pre actions have been executed.
Use [function_env] to get it back. *)
let env = !function_env in
+ let env =
+ if generate then
+ (* Add initialization statements and store_block statements stemming
+ from Local_init *)
+ self#add_initializers stmt env kf
+ else
+ env
+ in
let env =
if stmt.ghost && generate then begin
stmt.ghost <- false;
@@ -688,15 +696,6 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
~global_clear:false
Env.Before
in
- (match stmt.skind with
- | Instr (Local_init (vi, _, _)) when
- Mmodel_analysis.must_model_vi ~bhv:self#behavior ~kf vi ->
- let vi = Cil.get_varinfo self#behavior vi in
- (* must generate the new stmts after the declaration of [vi] *)
- post_block.bstmts <-
- post_block.bstmts @
- [Misc.mk_store_stmt vi; Misc.mk_full_init_stmt vi]
- | _ -> ());
let post_block = Cil.transient_block post_block in
Misc.mk_block prj new_stmt post_block, env
end else
@@ -710,55 +709,46 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in
Cil.ChangeDoChildrenPost(stmt, mk_block)
- method private add_initializer loc checked_lv assigned_lv =
+ method private add_initializer loc ?vi lv ?(post=false) stmt env kf =
assert generate;
- let kf = Extlib.the self#current_kf in
- let stmt = Extlib.the self#current_stmt in
let may_safely_ignore = function
| Var vi, NoOffset -> vi.vglob || vi.vformal
| _ -> false
in
-
- if not (may_safely_ignore assigned_lv) &&
- Mmodel_analysis.must_model_lval ~kf ~stmt checked_lv
- then
- let new_stmt =
- (* must be in the new project to build a new stmt *)
- Project.on
- prj
- (Misc.mk_initialize ~loc)
- assigned_lv
- in
+ if not (may_safely_ignore lv) && Mmodel_analysis.must_model_lval ~kf lv then
let before = Cil.memo_stmt self#behavior stmt in
+ let new_stmt = Project.on prj (Misc.mk_initialize ~loc) lv in
let new_stmt = Cil.memo_stmt self#behavior new_stmt in
- function_env := Env.add_stmt ~before !function_env new_stmt
-
- 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;
- l
- | _ -> assert false)
- else
- Cil.DoChildren
- | Local_init _ ->
- (* initialization is registered in vstmt. *)
- Cil.DoChildren
- | Call(Some old_ret, _, _, _) ->
- if not generate || Misc.is_generated_kf (Extlib.the self#current_kf) then
- Cil.DoChildren
+ let env = Env.add_stmt ~post ~before env new_stmt in
+ let env = match vi with
+ | None -> env
+ | Some vi ->
+ let new_stmt = Project.on prj Misc.mk_store_stmt vi in
+ let new_stmt = Cil.memo_stmt self#behavior new_stmt in
+ Env.add_stmt ~post ~before env new_stmt
+ in
+ env
else
- Cil.DoChildrenPost
- (function
- | [ Call(Some new_ret, _, _, loc) ] as l ->
- self#add_initializer loc old_ret new_ret;
- l
- | _ -> assert false)
- | _ ->
- Cil.DoChildren
+ env
+
+ method private add_initializers stmt env kf =
+ let do_instr instr =
+ match instr with
+ | Set(lv, _, loc) ->
+ self#add_initializer loc lv stmt env kf
+ | Local_init(vi, _, loc) ->
+ let lv = (Var(vi), NoOffset) in
+ self#add_initializer loc ~vi lv ~post:true stmt env kf
+ | Call (Some lv, _, _, loc) ->
+ if not (Misc.is_generated_kf kf) then
+ self#add_initializer loc lv ~post:false stmt env kf
+ else env
+ | _ -> env
+ in
+ match stmt.skind with
+ | Instr(i) -> do_instr i
+ | _ -> env
+
method !vblock blk =
let handle_memory new_blk =