From 84aedec868d15cb2cb20cea2d739ee79a5b066ab Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 22 Nov 2012 15:26:43 +0000
Subject: [PATCH] [E-ACSL] generate initialization of globals in a separated
function
---
src/plugins/e-acsl/TODO | 5 +-
.../e-acsl-runtime/global_literal_string.i | 1 +
.../oracle/gen_global_literal_string.c | 2 +-
.../oracle/gen_global_literal_string2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_valid.c | 10 +-
.../tests/e-acsl-runtime/oracle/gen_valid2.c | 10 +-
.../oracle/global_literal_string.1.res.oracle | 4 +-
.../oracle/global_literal_string.res.oracle | 4 +-
.../e-acsl-runtime/oracle/valid.1.res.oracle | 19 ++-
.../e-acsl-runtime/oracle/valid.res.oracle | 19 ++-
src/plugins/e-acsl/visit.ml | 128 +++++++++++++-----
11 files changed, 146 insertions(+), 58 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index ba4ed51a737..b020050ff06 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 0657e8f7719..a6922ebb83c 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 4699f7dffe9..29a5e7f8d1b 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 51e1e65ffdc..c088b49324b 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 dc24be6d75e..d448f90008a 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 dc24be6d75e..d448f90008a 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 0e2046b4720..163c8f7544b 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 0a08119fe7e..7780e237701 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 3047592d3c0..de0321dd474 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 3047592d3c0..de0321dd474 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 3d3ec83a7a9..cc16f673d26 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 =
--
GitLab