diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index ba4ed51a737cc1bb81fdd3fb34e757f03e6e1484..b020050ff06d634375a36266d21e48328125af97 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -13,11 +13,9 @@
- grep TODO *.ml*
- Gestion du mode -lib-entry
-- init du main dans une fonction séparée
-- l'init du main doit être généré même quand il n'y a pas de main
-- mkcall ne devrait pas générer de nouvelles variables pour une même fonction
- variable GMP potentiellement initialisé mais non utilisé en présence de \at
(voir test result.i, cas -e-acsl-gmp-only)
+- générer les delete des globals dans une fonction séparée, comme pour les init.
##############
# KNOWN BUGS #
@@ -37,6 +35,7 @@
(même problème que Jessie: cf. BTS #72)
(voir aussi result.i et ./at_stmt_contract.i)
- interprétation des tableaux
+- \initialized sur des chaînes littérales (voir global_literal_string.i)
#########
# TESTS #
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/global_literal_string.i b/src/plugins/e-acsl/tests/e-acsl-runtime/global_literal_string.i
index 0657e8f77191e59355741eaa4d2a6358ecf473a8..a6922ebb83c5f2848d912dd03b91fa1b236a3b46 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/global_literal_string.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/global_literal_string.i
@@ -23,6 +23,7 @@ int G2 = 2;
int main(void) {
/*@ assert S[G2] == 'o'; */
+ // /*@ assert \initialized(S); */
return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_global_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_global_literal_string.c
index 4699f7dffe90c8113c1f7e95dce1d1ea1bb9e350..29a5e7f8d1b962a2dbba1c0b0ac654a32285cce2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_global_literal_string.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_global_literal_string.c
@@ -68,7 +68,6 @@ void f(void)
char *S = (char *)"foo";
int IDX = 1;
int G2 = 2;
-char *U = (char *)"baz";
int main(void)
{
int __retres;
@@ -80,4 +79,5 @@ int main(void)
return (__retres);
}
+char *U = (char *)"baz";
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_global_literal_string2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_global_literal_string2.c
index 51e1e65ffdcb6379c2e1e120f1f0b6fcf3683e9d..c088b49324bd715aac810d042b3f7977c0222c09 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_global_literal_string2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_global_literal_string2.c
@@ -100,7 +100,6 @@ void f(void)
char *S = (char *)"foo";
int IDX = 1;
int G2 = 2;
-char *U = (char *)"baz";
int main(void)
{
int __retres;
@@ -124,4 +123,5 @@ int main(void)
return (__retres);
}
+char *U = (char *)"baz";
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index dc24be6d75e583ccd62240b9772faa1d7b1efff1..d448f90008a4cb79e4597c58e7f2654df18379d3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -160,14 +160,20 @@ int *f(int *x)
}
+void e_acsl_global_init(void)
+{
+ _store_block((void *)(& X),4U);
+ _full_init((void *)(& X));
+ return;
+}
+
int main(void)
{
int __retres;
int *a;
int *b;
int n;
- _store_block((void *)(& X),4U);
- _full_init((void *)(& X));
+ e_acsl_global_init();
_store_block((void *)(& n),4U);
_store_block((void *)(& b),4U);
_store_block((void *)(& a),4U);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index dc24be6d75e583ccd62240b9772faa1d7b1efff1..d448f90008a4cb79e4597c58e7f2654df18379d3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
@@ -160,14 +160,20 @@ int *f(int *x)
}
+void e_acsl_global_init(void)
+{
+ _store_block((void *)(& X),4U);
+ _full_init((void *)(& X));
+ return;
+}
+
int main(void)
{
int __retres;
int *a;
int *b;
int n;
- _store_block((void *)(& X),4U);
- _full_init((void *)(& X));
+ e_acsl_global_init();
_store_block((void *)(& n),4U);
_store_block((void *)(& b),4U);
_store_block((void *)(& a),4U);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.1.res.oracle
index 0e2046b47203ae2401bb4d250bdb9c763c3a2a5f..163c8f7544bd8741afcce108f6d999b91ce018d4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.1.res.oracle
@@ -66,7 +66,7 @@ tests/e-acsl-runtime/global_literal_string.i:25:[value] Assertion got status val
Called from tests/e-acsl-runtime/global_literal_string.i:25.
[value] Done for function __gmpz_clear
[value] computing for function __clean <- main.
- Called from tests/e-acsl-runtime/global_literal_string.i:26.
+ Called from tests/e-acsl-runtime/global_literal_string.i:27.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] Done for function __clean
@@ -179,7 +179,6 @@ void f(void)
char *S = (char *)"foo";
int IDX = 1;
int G2 = 2;
-char *U = (char *)"baz";
int main(void)
{
int __retres;
@@ -203,4 +202,5 @@ int main(void)
return (__retres);
}
+char *U = (char *)"baz";
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.res.oracle
index 0a08119fe7ef989fb02dc7c3ef34f1719d3ec661..7780e23770134a43e1a96ac372b57b679bb43be4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.res.oracle
@@ -42,7 +42,7 @@ tests/e-acsl-runtime/global_literal_string.i:25:[value] Assertion got status val
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
[value] computing for function __clean <- main.
- Called from tests/e-acsl-runtime/global_literal_string.i:26.
+ Called from tests/e-acsl-runtime/global_literal_string.i:27.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] Done for function __clean
@@ -123,7 +123,6 @@ void f(void)
char *S = (char *)"foo";
int IDX = 1;
int G2 = 2;
-char *U = (char *)"baz";
int main(void)
{
int __retres;
@@ -135,4 +134,5 @@ int main(void)
return (__retres);
}
+char *U = (char *)"baz";
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index 3047592d3c0c9cdb3fffbb11cccc0004a3eefc51..de0321dd47403a3b6f416cccf89491623b0df691 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -27,14 +27,18 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] computing for function _store_block <- main.
+[value] computing for function e_acsl_global_init <- main.
+ Called from :0.
+[value] computing for function _store_block <- e_acsl_global_init <- main.
Called from tests/e-acsl-runtime/valid.c:13.
[value] using specification for function _store_block
[value] Done for function _store_block
-[value] computing for function _full_init <- main.
+[value] computing for function _full_init <- e_acsl_global_init <- main.
Called from tests/e-acsl-runtime/valid.c:13.
[value] using specification for function _full_init
[value] Done for function _full_init
+[value] Recording results for e_acsl_global_init
+[value] Done for function e_acsl_global_init
[value] computing for function _store_block <- main.
Called from tests/e-acsl-runtime/valid.c:26.
[value] Done for function _store_block
@@ -316,6 +320,7 @@ tests/e-acsl-runtime/valid.c:37:[value] Non-termination in evaluation of functio
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
+[value] Values at end of function e_acsl_global_init:
[value] Values at end of function e_acsl_assert:
S___fc_stdout[0].__fc_stdio_fpos ∈ [--..--]
[0].__fc_stdio_buffer ∈
@@ -535,14 +540,20 @@ int *f(int *x)
}
+void e_acsl_global_init(void)
+{
+ _store_block((void *)(& X),4U);
+ _full_init((void *)(& X));
+ return;
+}
+
int main(void)
{
int __retres;
int *a;
int *b;
int n;
- _store_block((void *)(& X),4U);
- _full_init((void *)(& X));
+ e_acsl_global_init();
_store_block((void *)(& n),4U);
_store_block((void *)(& b),4U);
_store_block((void *)(& a),4U);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index 3047592d3c0c9cdb3fffbb11cccc0004a3eefc51..de0321dd47403a3b6f416cccf89491623b0df691 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -27,14 +27,18 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] computing for function _store_block <- main.
+[value] computing for function e_acsl_global_init <- main.
+ Called from :0.
+[value] computing for function _store_block <- e_acsl_global_init <- main.
Called from tests/e-acsl-runtime/valid.c:13.
[value] using specification for function _store_block
[value] Done for function _store_block
-[value] computing for function _full_init <- main.
+[value] computing for function _full_init <- e_acsl_global_init <- main.
Called from tests/e-acsl-runtime/valid.c:13.
[value] using specification for function _full_init
[value] Done for function _full_init
+[value] Recording results for e_acsl_global_init
+[value] Done for function e_acsl_global_init
[value] computing for function _store_block <- main.
Called from tests/e-acsl-runtime/valid.c:26.
[value] Done for function _store_block
@@ -316,6 +320,7 @@ tests/e-acsl-runtime/valid.c:37:[value] Non-termination in evaluation of functio
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
+[value] Values at end of function e_acsl_global_init:
[value] Values at end of function e_acsl_assert:
S___fc_stdout[0].__fc_stdio_fpos ∈ [--..--]
[0].__fc_stdio_buffer ∈
@@ -535,14 +540,20 @@ int *f(int *x)
}
+void e_acsl_global_init(void)
+{
+ _store_block((void *)(& X),4U);
+ _full_init((void *)(& X));
+ return;
+}
+
int main(void)
{
int __retres;
int *a;
int *b;
int n;
- _store_block((void *)(& X),4U);
- _full_init((void *)(& X));
+ e_acsl_global_init();
_store_block((void *)(& n),4U);
_store_block((void *)(& b),4U);
_store_block((void *)(& a),4U);
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 3d3ec83a7a922e76a42856832b4eb6a645f1fc31..cc16f673d268b19e23c5b5a0cf8b3c71403ffe2c 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -175,45 +175,99 @@ class e_acsl_visitor prj generate = object (self)
visitor. *)
if generate then Project.clear ~selection ~project:prj ();
(* extend the main with forward initialization and put it at end *)
- (match main_fct with
- | Some main ->
- if not (Options.Check.get ()) then
- let stmts =
- Varinfo.Hashtbl.fold
- (fun old_vi i acc ->
- let new_vi = Cil.get_varinfo self#behavior old_vi in
- let model blk =
- if Pre_analysis.must_model_vi old_vi then
- mk_store_stmt new_vi :: mk_full_init_stmt new_vi :: blk
- else
- acc
- in
- match i with
- | None -> model acc
- | Some i ->
- let b =
- Cabs2cil.blockInit (Var new_vi, NoOffset) i new_vi.vtype
+ if not (Options.Check.get ()) then begin
+ let must_init =
+ try
+ Varinfo.Hashtbl.iter
+ (fun old_vi i -> match i with None | Some _ ->
+ if Pre_analysis.must_model_vi old_vi then raise Exit)
+ global_vars;
+ false
+ with Exit ->
+ true
+ in
+ if must_init then
+ let build_initializer () =
+ let return =
+ Cil.mkStmt ~valid_sid:true (Return(None, Location.unknown))
+ in
+ let stmts =
+ Varinfo.Hashtbl.fold
+ (fun old_vi i acc ->
+ let new_vi = Cil.get_varinfo self#behavior old_vi in
+ let model blk =
+ if Pre_analysis.must_model_vi old_vi then
+ mk_store_stmt new_vi :: mk_full_init_stmt new_vi :: blk
+ else
+ acc
in
- model (Cil.mkStmt ~valid_sid:true (Block b) :: acc))
- global_vars
- main.sbody.bstmts
- in
- main.sbody.bstmts <- stmts;
- let new_globals =
- List.fold_right
- (fun g acc -> match g with
- | GFun({ svar = vi }, _) when Varinfo.equal vi main.svar -> acc
- | _ -> g :: acc)
- f.globals
- [ GFun(main, Location.unknown) ]
+ match i with
+ | None -> model acc
+ | Some i ->
+ let b =
+ Cabs2cil.blockInit
+ (Var new_vi, NoOffset)
+ i
+ new_vi.vtype
+ in
+ model (Cil.mkStmt ~valid_sid:true (Block b) :: acc))
+ global_vars
+ [ return ]
+ in
+ let blk = Cil.mkBlock stmts in
+ let fname = "e_acsl_global_init" in
+ let vi =
+ Cil.makeGlobalVar ~logic:false ~generated:true
+ fname
+ (TFun(Cil.voidType, Some [], false, []))
+ in
+ vi.vdefined <- true;
+ let spec = Cil.empty_funspec () in
+ let fundec =
+ { svar = vi;
+ sformals = [];
+ slocals = [];
+ smaxid = 0;
+ sbody = blk;
+ smaxstmtid = None;
+ sallstmts = [];
+ sspec = spec }
+ in
+ let fct = Definition(fundec, Location.unknown) in
+ let kf =
+ { fundec = fct; return_stmt = Some return; spec = spec }
+ in
+ Globals.Functions.register kf;
+ Globals.Functions.replace_by_definition
+ spec fundec Location.unknown;
+ let cil_fct = GFun(fundec, Location.unknown) in
+ match main_fct with
+ | Some main ->
+ let exp = Cil.evar ~loc:Location.unknown vi in
+ let stmt =
+ Cil.mkStmtOneInstr ~valid_sid:true
+ (Call(None, exp, [], Location.unknown))
+ in
+ vi.vreferenced <- true;
+ main.sbody.bstmts <- stmt :: main.sbody.bstmts;
+ let new_globals =
+ List.fold_right
+ (fun g acc -> match g with
+ | GFun({ svar = vi }, _) when Varinfo.equal vi main.svar ->
+ acc
+ | _ -> g :: acc)
+ f.globals
+ [ cil_fct; GFun(main, Location.unknown) ]
+ in
+ f.globals <- new_globals
+ | None ->
+ Kernel.warning "no entry point specified:@ \
+you must call function `%s' by yourself"
+ fname;
+ f.globals <- f.globals @ [ cil_fct ]
in
- f.globals <- new_globals
- | None ->
- Varinfo.Hashtbl.iter
- (fun _ i -> match i with
- | None -> ()
- | Some _ -> Kernel.abort "entry point required")
- global_vars);
+ Project.on prj build_initializer ()
+ end;
f)
method vglob_aux g =