diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 7224d5519e39957161ade8c2d5719d564b076592..9d13aea4bcfe717f7187970ba50c9fab8e864c49 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -367,29 +367,30 @@ let transfer ~from env = match from.env_stack, env.env_stack with
{ env with env_stack = { local with block_info = new_blk } :: tl }
| _, _ ->
assert false
-
+
type where = Before | Middle | After
-let pop_and_get env stmt ~global_clear where =
-(* Options.feedback "pop_and_get (%d)" (List.length env.env_stack);*)
+let pop_and_get ?(split=false) env stmt ~global_clear where =
+ let split = split && stmt.labels = [] in
+(* Options.feedback "pop_and_get from %a (%b)" Printer.pp_stmt stmt split;*)
let local_env, tl = top false env in
- let clear =
+ let clear =
if global_clear then begin
Varname.clear ();
env.global_mpz_tbl.clear_stmts @ local_env.mpz_tbl.clear_stmts
end else
local_env.mpz_tbl.clear_stmts
in
-(* Options.feedback "clearing %d mpz (global_clear: %b)"
+(* Options.feedback "clearing %d mpz (global_clear: %b)"
(List.length clear) global_clear;*)
let block = local_env.block_info in
- let b =
- let pre_stmts, stmt =
+ let b =
+ let pre_stmts, stmt =
let rec extract stmt acc = function
- | [] -> acc, stmt
- | _ :: tl ->
- match stmt.skind with
- | Block { bstmts = [ fst; snd ] } -> extract snd (fst :: acc) tl
- | _ ->
+ | [] -> acc, stmt
+ | _ :: tl ->
+ match stmt.skind with
+ | Block { bstmts = [ fst; snd ] } -> extract snd (fst :: acc) tl
+ | _ ->
Kernel.fatal
"experting a block containing 2 statements instead of %a"
Printer.pp_stmt stmt
@@ -401,15 +402,43 @@ let pop_and_get env stmt ~global_clear where =
| Instr(Skip _) -> l
| _ -> stmt :: l
in
- let stmts = match where with
+ let stmts =
+ match where with
| Before -> cat stmt (acc_list_rev (List.rev clear) new_s)
| Middle -> acc_list_rev (cat stmt (List.rev clear)) new_s
- | After -> acc_list_rev (acc_list_rev (cat stmt []) clear) new_s
+ | After ->
+ (* if [split], do not put the given [stmt] in the generated block *)
+ let stmts = if split then [] else cat stmt [] in
+ acc_list_rev (acc_list_rev stmts clear) new_s
in
Cil.mkBlock (acc_list_rev stmts pre_stmts)
in
b.blocals <- acc_list_rev b.blocals block.new_block_vars;
- b, { env with env_stack = tl }
+ let b =
+ (* blocks with local cannot be transient (see doc in cil.ml),
+ while transient blocks prevent the E-ACSL labeling strategy from working
+ properly: no transient block in that cases. *)
+ if b.blocals = [] && stmt.labels = [] then Cil.transient_block b
+ else b
+ in
+ let final_blk =
+ (* if [split], put the generated code in a distinct sub-block and
+ add the given [stmt] afterwards. This way, we have the guarantee that
+ the final block does not contain any local, so may be transient. *)
+ if split then
+ match stmt.skind with
+ | Instr (Skip _) -> b
+ | _ ->
+ let sblock = Cil.mkStmt ~valid_sid:true (Block b) in
+ Cil.transient_block (Cil.mkBlock [ sblock; stmt ])
+ else
+ b
+ in
+ (* remove superflous brackets inside the generated block *)
+ let final_blk = Cil.flatten_transient_sub_blocks final_blk in
+ (* remove the non-scoping mark of the outermost block *)
+ let final_blk = Cil.block_of_transient final_blk in
+ final_blk, { env with env_stack = tl }
let get_generated_variables env = List.rev env.new_global_vars
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index 51d40665385a737a24d99e6e8d560ecd6bbf46c4..a55f8cc239e070013c58f7189907e0513df07eb9 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -84,12 +84,15 @@ val push: t -> t
(** Push a new local context in the environment *)
type where = Before | Middle | After
-val pop_and_get: t -> stmt -> global_clear:bool -> where -> block * t
+val pop_and_get:
+ ?split:bool -> t -> stmt -> global_clear:bool -> where -> block * t
(** Pop the last local context and get back the corresponding new block
containing the given [stmt] at the given place ([Before] is before the code
corresponding to annotations, [After] is after this code and [Middle] is
between the stmt corresponding to annotations and the ones for freeing the
- memory. *)
+ memory. When [where] is [After], set [split] to true in order to generate
+ one block which contains exactly 2 stmt: one for [stmt] and one sub-block
+ for the generated stmts. *)
val pop: t -> t
(** Pop the last local context (ignore the corresponding new block if any *)
diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
index 979eb21e4ca0934a1ef2d85cc704a5ea8b1f0c82..c7328e163a18a2e55ac9ee2be62c12ecef0fe30f 100644
--- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -157,7 +157,17 @@ first \fIframa-c\fP executable found in the system path is used.
.B -G, --gcc=\fI<FILE>
the name of the \fBGCC\fP executable. By default the first \fIgcc\fP
executable found in the system path is used.
-
+.TP
+.B --then
+Separate with a \fB-then\fP the first \fBFrama-C\fP options from the actual
+launch of the \fBE-ACSL\fP plugin. Prepends \fB-e-acsl-prepare\fP to the list
+of options passed to \fBFrama-C\fP.
+.TP
+.B --e-acsl-extra=\fI<OPTS>
+Adds \fI<OPTS>\fP to the list of options that will be given to the \fBE-ACSL\fP
+analysis. Only useful when \fB--then\fP is in use, in which case \fI<OPTS>\fP
+will be placed after the \fB-then\fP on \fBFrama-C\fP's command-line. Otherwise,
+equivalent to \fB--frama-c-extra\fP
.SH EXIT STATUS
.TP
.B 0
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index b2f47a295b54b1d2d1d62a8871a4d47a2fa7afae..c9415e14d91f9ec10c0580b98167edd965b8729f 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -159,8 +159,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
~global_clear:false
Env.After
in
- (* TODO: could be optimised if [pop_and_get] would return a list of
- stmts *)
+ let blk = Cil.flatten_transient_sub_blocks blk in
[ mkStmt ~valid_sid:true (Block blk) ], env
| (t1, rel1, logic_x, rel2, t2) :: tl ->
let ctx =
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 455049c6c481295b3aff003ad8a2b3e512da7286..72934fa95e21b91987c0c4ab07f054c51d9a9c0f 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -194,7 +194,7 @@ LONGOPTIONS="help,compile,compile-only,debug:,ocode:,oexec:,verbose:,
frama-c-only,extra-cpp-args:,frama-c-stdlib,full-mmodel,gmp,quiet,logfile:,
ld-flags:,cpp-flags:,frama-c-extra:,memory-model:,
frama-c:,gcc:,e-acsl-share:,instrumented-only,rte:,oexec-e-acsl:,check
- print-mmodels,rt-debug,rte-select:"
+ print-mmodels,rt-debug,rte-select:,then,e-acsl-extra:"
SHORTOPTIONS="h,c,C,d:,D,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,I:,G:,X,a:,V"
# Prefix for an error message due to wrong arguments
ERROR="ERROR parsing arguments:"
@@ -225,6 +225,7 @@ OPTION_INSTRUMENTED_ONLY= # Do not compile original code
OPTION_RTE= # Enable assertion generation
OPTION_CHECK= # Check AST integrity
OPTION_RTE_SELECT= # Generate assertions for these functions only
+OPTION_THEN= # Adds -then in front of -e-acsl in FC command.
# Supported memory model names
SUPPORTED_MMODELS="bittree,segment"
@@ -453,6 +454,17 @@ do
echo $SUPPORTED_MMODELS
exit 0
;;
+ #Separate extra Frama-C flags from e-acsl launch with -then.
+ --then)
+ shift;
+ OPTION_THEN=-then
+ FRAMAC_FLAGS="-e-acsl-prepare $FRAMAC_FLAGS"
+ ;;
+ --e-acsl-extra)
+ shift;
+ OPTION_EACSL="$1 $OPTION_EACSL"
+ shift;
+ ;;
esac
done
shift;
@@ -520,6 +532,10 @@ if [ -n "$OPTION_EACSL_SHARE" ]; then
EACSL_SHARE="$OPTION_EACSL_SHARE"
fi
+if [ -n "$OPTION_THEN" ]; then
+ FRAMAC_FLAGS="-e-acsl-share=$EACSL_SHARE $FRAMAC_FLAGS";
+fi
+
# Select optimization flags for both instrumented and noon-instrumented code
# compilation
if [ -n "$OPTION_RT_DEBUG" ]; then
@@ -581,6 +597,7 @@ fi
# Build E-ACSL plugin argument string
if [ -n "$OPTION_EACSL" ]; then
EACSL_FLAGS="
+ $OPTION_THEN
$OPTION_EACSL
$OPTION_GMP
$OPTION_FULL_MMODEL
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 5717cea664861ca0917acd17d42a8851651ba87e..caa221c7af4e0b90fcc074663440e0a315d67ca1 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -135,14 +135,14 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
(void *)(& Mtmin_out));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
(char *)"bar",(char *)"\\valid(Mtmin_out)",19);
- __gen_e_acsl_at_6 = Mwmin;
- __gen_e_acsl_at_5 = Mtmin_in;
- __gen_e_acsl_at_4 = Mwmin;
- __gen_e_acsl_at_3 = Mtmin_in;
- __gen_e_acsl_at_2 = Mtmin_in;
- __gen_e_acsl_at = Mtmin_out;
- bar(Mtmin_in,Mwmin,Mtmin_out);
}
+ __gen_e_acsl_at_6 = Mwmin;
+ __gen_e_acsl_at_5 = Mtmin_in;
+ __gen_e_acsl_at_4 = Mwmin;
+ __gen_e_acsl_at_3 = Mtmin_in;
+ __gen_e_acsl_at_2 = Mtmin_in;
+ __gen_e_acsl_at = Mtmin_out;
+ bar(Mtmin_in,Mwmin,Mtmin_out);
{
int __gen_e_acsl_valid_read;
int __gen_e_acsl_valid_read_2;
@@ -248,11 +248,11 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
(void *)(& Mtmax_out));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
(char *)"foo",(char *)"\\valid(Mtmax_out)",7);
- __gen_e_acsl_at_3 = Mwmax;
- __gen_e_acsl_at_2 = Mtmax_in;
- __gen_e_acsl_at = Mtmax_out;
- foo(Mtmax_in,Mwmax,Mtmax_out);
}
+ __gen_e_acsl_at_3 = Mwmax;
+ __gen_e_acsl_at_2 = Mtmax_in;
+ __gen_e_acsl_at = Mtmax_out;
+ foo(Mtmax_in,Mwmax,Mtmax_out);
{
int __gen_e_acsl_valid_read;
int __gen_e_acsl_valid_read_2;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
index 4a502b1e822ebad506c270209e3dc14b42d87397..ce014ccd5a215298c2a3c9c4ae1dd555b8370ba5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
@@ -12,10 +12,8 @@ int fact(int n)
__retres = 1;
goto return_label;
}
- { /* sequence */
- tmp = __gen_e_acsl_fact(n - 1);
- ;
- }
+ tmp = __gen_e_acsl_fact(n - 1);
+ ;
__retres = n * tmp;
return_label: return __retres;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
index 6e3a6dfa88ee40d0fd1d3c907dee3889c686d5da..d7ada2c7115bd789170d9402edb44f320bf154f5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -36,8 +36,8 @@ void __gen_e_acsl_loop(void)
(char *)"\\valid(global_i_ptr)",10);
__e_acsl_assert(global_i_ptr == & global_i,(char *)"Precondition",
(char *)"loop",(char *)"global_i_ptr == &global_i",11);
- loop();
}
+ loop();
return;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
index 8849e28f584d838d51d8ca051fbd5b9802932821..c403fd5ceeb4ef6966cf42bd8689e7278b27f9d7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -11,32 +11,32 @@ int main(void)
__e_acsl_full_init((void *)(& a));
goto lbl_1;
lbl_2:
- /*@ 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),(void *)p,
- (void *)(& p));
- __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)",10);
+ /*@ 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),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
}
- __retres = 0;
- goto return_label;
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(p)",10);
+ }
+ __retres = 0;
+ goto return_label;
lbl_1: __e_acsl_full_init((void *)(& p));
p = & a;
goto lbl_2;
return_label:
- __e_acsl_delete_block((void *)(& p));
- __e_acsl_delete_block((void *)(& a));
- __e_acsl_memory_clean();
- return __retres;
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_delete_block((void *)(& a));
+ __e_acsl_memory_clean();
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
index 6a1f48467405e520ce022c13c0ce394a8edcf3f6..bdf3b4a98f0e0b17165e86ea70c856883623a54f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -11,32 +11,32 @@ int main(void)
__e_acsl_full_init((void *)(& a));
goto lbl_1;
lbl_2:
- /*@ 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),(void *)p,
- (void *)(& p));
- __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)",13);
+ /*@ 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),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
}
- __retres = 0;
- goto return_label;
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(p)",13);
+ }
+ __retres = 0;
+ goto return_label;
lbl_1: __e_acsl_full_init((void *)(& p));
p = & a;
goto lbl_2;
return_label:
- __e_acsl_delete_block((void *)(& p));
- __e_acsl_delete_block((void *)(& a));
- __e_acsl_memory_clean();
- return __retres;
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_delete_block((void *)(& a));
+ __e_acsl_memory_clean();
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
index 1be5aa98ba9199f85d66a4d0da156a02c667e2b9..7421ceccaa3d08fdffe92c36a3c6dd22ceb647ab 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
@@ -33,27 +33,27 @@ int main(void)
__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),
- (void *)p,(void *)(& p));
- __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);
+ /*@ 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),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
- __retres = 0;
- __e_acsl_delete_block((void *)(& p));
- __e_acsl_memory_clean();
- return __retres;
+ 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/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index 26fe680be04f9f5a32ed9b49e43e941e3a6751a8..680fca00da0f006892963bba43099c5448d5de8b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -90,12 +90,10 @@ int main(void)
int i = 4;
while (1) {
int tmp;
- { /* sequence */
- tmp = i;
- /*@ assert Value: signed_overflow: -2147483648 ≤ i - 1; */
- i --;
- ;
- }
+ tmp = i;
+ /*@ assert Value: signed_overflow: -2147483648 ≤ i - 1; */
+ i --;
+ ;
if (! tmp) break;
{
char *s = (char *)__gen_e_acsl_literal_string_3;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
index c56a8ba6a99fc28deda2c79dc3146c59fe5c74f0..db197044b2847d2a17979216d517bef48bd619bb 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
@@ -19,10 +19,8 @@ int main(int argc, char **argv)
int __retres;
__e_acsl_memory_init(& argc,& argv,(size_t)8);
__e_acsl_globals_init();
- { /* sequence */
- argc = __gen_e_acsl_atoi((char const *)n);
- a = argc;
- }
+ argc = __gen_e_acsl_atoi((char const *)n);
+ a = argc;
__retres = 0;
__e_acsl_delete_block((void *)(& n));
__e_acsl_memory_clean();
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 0be34f3867c94a594016eb9589084e0d1dd513c4..50e175fcb044acba4e3d318107f89dc288c160a6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -47,61 +47,60 @@ void g(int *p, int *q)
__e_acsl_initialize((void *)q,sizeof(int));
*q = 0;
L1:
- {
- int __gen_e_acsl_valid_read_3;
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
- (void *)q,
- (void *)(& q));
- __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(q)",28);
- __gen_e_acsl_at_3 = *q;
- }
- {
- int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
+ {
+ int __gen_e_acsl_valid_read_3;
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
(void *)q,(void *)(& q));
- __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(q)",26);
- __gen_e_acsl_at = *q;
- }
- __e_acsl_initialize((void *)p,sizeof(int));
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(q)",28);
+ __gen_e_acsl_at_3 = *q;
+ }
+ {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
+ __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(q)",26);
+ __gen_e_acsl_at = *q;
+ }
+ __e_acsl_initialize((void *)p,sizeof(int));
*p = 2;
__e_acsl_initialize((void *)(p + 1),sizeof(int));
*(p + 1) = 3;
__e_acsl_initialize((void *)q,sizeof(int));
*q = 1;
L2:
- {
- int __gen_e_acsl_valid_read_2;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
- sizeof(int),(void *)p,
- (void *)(& p));
- __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
- 26);
- __gen_e_acsl_at_2 = *(p + __gen_e_acsl_at);
- }
- A = 4;
+ {
+ int __gen_e_acsl_valid_read_2;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
+ sizeof(int),(void *)p,
+ (void *)(& p));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
+ 26);
+ __gen_e_acsl_at_2 = *(p + __gen_e_acsl_at);
+ }
+ A = 4;
/*@ assert \at(*(p + \at(*q,L1)),L2) ≡ 2; */
__e_acsl_assert(__gen_e_acsl_at_2 == 2,(char *)"Assertion",(char *)"g",
(char *)"\\at(*(p + \\at(*q,L1)),L2) == 2",26);
L3:
- /*@ assert \at(*(p + \at(*q,L1)),Here) ≡ 2; */
- {
- int __gen_e_acsl_valid_read_4;
- __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at_3),
- sizeof(int),(void *)p,
- (void *)(& p));
- __e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at_3)",
- 28);
- __e_acsl_assert(*(p + __gen_e_acsl_at_3) == 2,(char *)"Assertion",
- (char *)"g",
- (char *)"\\at(*(p + \\at(*q,L1)),Here) == 2",28);
- }
- __e_acsl_delete_block((void *)(& q));
- __e_acsl_delete_block((void *)(& p));
- return;
+ /*@ assert \at(*(p + \at(*q,L1)),Here) ≡ 2; */
+ {
+ int __gen_e_acsl_valid_read_4;
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at_3),
+ sizeof(int),(void *)p,
+ (void *)(& p));
+ __e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at_3)",
+ 28);
+ __e_acsl_assert(*(p + __gen_e_acsl_at_3) == 2,(char *)"Assertion",
+ (char *)"g",(char *)"\\at(*(p + \\at(*q,L1)),Here) == 2",
+ 28);
+ }
+ __e_acsl_delete_block((void *)(& q));
+ __e_acsl_delete_block((void *)(& p));
+ return;
}
/*@ ensures \result ≡ \old(x); */
@@ -129,14 +128,14 @@ int main(void)
__e_acsl_full_init((void *)(& x));
x = __gen_e_acsl_h(0);
L:
- __gen_e_acsl_at_3 = (long)x;
- __gen_e_acsl_at_2 = x + 1L;
- __gen_e_acsl_at = x;
- /*@ assert x ≡ 0; */
- __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",
- (char *)"x == 0",43);
- __e_acsl_full_init((void *)(& x));
- x = 1;
+ __gen_e_acsl_at_3 = (long)x;
+ __gen_e_acsl_at_2 = x + 1L;
+ __gen_e_acsl_at = x;
+ /*@ assert x ≡ 0; */
+ __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",
+ 43);
+ __e_acsl_full_init((void *)(& x));
+ x = 1;
__e_acsl_full_init((void *)(& x));
x = 2;
__gen_e_acsl_f();
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 832354a78aa7c3b9a7165766abfc17b58e1206e8..5b54cad0dde4309b9fc5cd75328f89681d8810fd 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
@@ -26,16 +26,16 @@ void f(void)
}
A = 1;
F:
- __gmpz_init_set(__gen_e_acsl_at_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
- {
- __e_acsl_mpz_t __gen_e_acsl_A_2;
- __gmpz_init_set_si(__gen_e_acsl_A_2,(long)A);
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_A_2));
- __gmpz_clear(__gen_e_acsl_A_2);
- }
- A = 2;
+ __gmpz_init_set(__gen_e_acsl_at_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
+ {
+ __e_acsl_mpz_t __gen_e_acsl_A_2;
+ __gmpz_init_set_si(__gen_e_acsl_A_2,(long)A);
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_A_2));
+ __gmpz_clear(__gen_e_acsl_A_2);
+ }
+ A = 2;
/*@ assert \at(A,Pre) ≡ 0; */
{
__e_acsl_mpz_t __gen_e_acsl_;
@@ -104,45 +104,44 @@ void g(int *p, int *q)
__e_acsl_initialize((void *)q,sizeof(int));
*q = 0;
L1:
- {
- int __gen_e_acsl_valid_read_3;
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
- (void *)q,
- (void *)(& q));
- __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(q)",28);
- __gen_e_acsl_at_3 = *q;
- }
- {
- int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
+ {
+ int __gen_e_acsl_valid_read_3;
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
(void *)q,(void *)(& q));
- __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(q)",26);
- __gen_e_acsl_at = *q;
- }
- __e_acsl_initialize((void *)p,sizeof(int));
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(q)",28);
+ __gen_e_acsl_at_3 = *q;
+ }
+ {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
+ __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(q)",26);
+ __gen_e_acsl_at = *q;
+ }
+ __e_acsl_initialize((void *)p,sizeof(int));
*p = 2;
__e_acsl_initialize((void *)(p + 1),sizeof(int));
*(p + 1) = 3;
__e_acsl_initialize((void *)q,sizeof(int));
*q = 1;
L2:
- {
- int __gen_e_acsl_valid_read_2;
- __e_acsl_mpz_t __gen_e_acsl_;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
- sizeof(int),(void *)p,
- (void *)(& p));
- __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
- 26);
- __gmpz_init_set_si(__gen_e_acsl_,(long)*(p + __gen_e_acsl_at));
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gmpz_clear(__gen_e_acsl_);
- }
- A = 4;
+ {
+ int __gen_e_acsl_valid_read_2;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
+ sizeof(int),(void *)p,
+ (void *)(& p));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
+ 26);
+ __gmpz_init_set_si(__gen_e_acsl_,(long)*(p + __gen_e_acsl_at));
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ A = 4;
/*@ assert \at(*(p + \at(*q,L1)),L2) ≡ 2; */
{
__e_acsl_mpz_t __gen_e_acsl__2;
@@ -155,24 +154,24 @@ void g(int *p, int *q)
__gmpz_clear(__gen_e_acsl__2);
}
L3:
- /*@ assert \at(*(p + \at(*q,L1)),Here) ≡ 2; */
- {
- __e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_eq_2;
- __gmpz_init_set_si(__gen_e_acsl__3,(long)*(p + __gen_e_acsl_at_3));
- __gmpz_init_set_si(__gen_e_acsl__4,2L);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"g",
- (char *)"\\at(*(p + \\at(*q,L1)),Here) == 2",28);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl__4);
- }
- __e_acsl_delete_block((void *)(& q));
- __e_acsl_delete_block((void *)(& p));
- __gmpz_clear(__gen_e_acsl_at_2);
- return;
+ /*@ assert \at(*(p + \at(*q,L1)),Here) ≡ 2; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_eq_2;
+ __gmpz_init_set_si(__gen_e_acsl__3,(long)*(p + __gen_e_acsl_at_3));
+ __gmpz_init_set_si(__gen_e_acsl__4,2L);
+ __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"g",
+ (char *)"\\at(*(p + \\at(*q,L1)),Here) == 2",28);
+ __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl__4);
+ }
+ __e_acsl_delete_block((void *)(& q));
+ __e_acsl_delete_block((void *)(& p));
+ __gmpz_clear(__gen_e_acsl_at_2);
+ return;
}
/*@ ensures \result ≡ \old(x); */
@@ -199,52 +198,52 @@ int main(void)
__e_acsl_full_init((void *)(& x));
x = __gen_e_acsl_h(0);
L:
- {
- __e_acsl_mpz_t __gen_e_acsl_x_4;
- __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
- __gmpz_init_set(__gen_e_acsl_at,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4));
- __gmpz_clear(__gen_e_acsl_x_4);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_x_3;
- __e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
- __gmpz_init_set_si(__gen_e_acsl__3,1L);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gmpz_clear(__gen_e_acsl_x_3);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl_add);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
- __gmpz_init_set(__gen_e_acsl_at,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2));
- __gmpz_clear(__gen_e_acsl_x_2);
- }
- /*@ assert x ≡ 0; */
- {
- __e_acsl_mpz_t __gen_e_acsl_x;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",
- (char *)"main",(char *)"x == 0",43);
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_);
- }
- __e_acsl_full_init((void *)(& x));
- x = 1;
+ {
+ __e_acsl_mpz_t __gen_e_acsl_x_4;
+ __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
+ __gmpz_init_set(__gen_e_acsl_at,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4));
+ __gmpz_clear(__gen_e_acsl_x_4);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_x_3;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl__3,1L);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gmpz_clear(__gen_e_acsl_x_3);
+ __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_x_2;
+ __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
+ __gmpz_init_set(__gen_e_acsl_at,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2));
+ __gmpz_clear(__gen_e_acsl_x_2);
+ }
+ /*@ assert x ≡ 0; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_eq;
+ __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"x == 0",43);
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ __e_acsl_full_init((void *)(& x));
+ x = 1;
__e_acsl_full_init((void *)(& x));
x = 2;
__gen_e_acsl_f();
diff --git a/src/plugins/e-acsl/tests/runtime/local_init.c b/src/plugins/e-acsl/tests/runtime/local_init.c
new file mode 100644
index 0000000000000000000000000000000000000000..77f64afba262be597862db14820e8533c1092801
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/local_init.c
@@ -0,0 +1,19 @@
+/* run.config
+ COMMENT: test of a local initializer which contains an annotation
+ LOG: gen_@PTEST_NAME@.c
+ OPT: -e-acsl-prepare -val -lib-entry -then -e-acsl -then-last -load-script tests/print.cmxs -print -ocode @PTEST_DIR@/result/gen_@PTEST_NAME@.c
+ EXEC: ./scripts/testrun.sh @PTEST_NAME@ runtime "" "--frama-c=@frama-c@ -F -val -F -lib-entry --then --e-acsl-extra=-no-lib-entry --e-acsl-extra=-no-val"
+*/
+
+int X = 0;
+int *p = &X;
+
+int f(void) {
+ int x = *p; // Eva add an alarms on this statement
+ return x;
+}
+
+int main(void) {
+ f();
+ return 0;
+}
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
index f612e32bb617a9e94948ba8fbd26efa3e35d23e5..8481525907067cad87c0fe93152002544a903d48 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
@@ -32,26 +32,26 @@ int goto_bts(void)
__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),
- (void *)p,(void *)(& p));
- __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);
+ /*@ 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),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
- __retres = 0;
- __e_acsl_delete_block((void *)(& p));
- return __retres;
+ 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)
@@ -87,136 +87,132 @@ int goto_valid(void)
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_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),
- (void *)p,(void *)(& p));
- __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),
- (void *)q,(void *)(& q));
- __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),
- (void *)r,(void *)(& r));
- __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); */
+ /*@ 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),
- (void *)p,(void *)(& p));
- __gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
+ 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),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
}
- else __gen_e_acsl_and_4 = 0;
- __e_acsl_assert(! __gen_e_acsl_and_4,(char *)"Assertion",
- (char *)"goto_valid",(char *)"!\\valid(p)",56);
+ 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_5;
- int __gen_e_acsl_and_5;
- __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& 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_5) {
- int __gen_e_acsl_valid_5;
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_2;
/*@ assert Value: dangling_pointer: ¬\dangling(&q); */
- __gen_e_acsl_valid_5 = __e_acsl_valid((void *)q,sizeof(int),
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
(void *)q,(void *)(& q));
- __gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
- else __gen_e_acsl_and_5 = 0;
- __e_acsl_assert(! __gen_e_acsl_and_5,(char *)"Assertion",
- (char *)"goto_valid",(char *)"!\\valid(q)",57);
+ 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_6;
- int __gen_e_acsl_and_6;
- __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& 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_6) {
- int __gen_e_acsl_valid_6;
+ if (__gen_e_acsl_initialized_3) {
+ int __gen_e_acsl_valid_3;
/*@ assert Value: dangling_pointer: ¬\dangling(&r); */
- __gen_e_acsl_valid_6 = __e_acsl_valid((void *)r,sizeof(int),
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)r,sizeof(int),
(void *)r,(void *)(& r));
- __gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
+ __gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
}
- else __gen_e_acsl_and_6 = 0;
- __e_acsl_assert(! __gen_e_acsl_and_6,(char *)"Assertion",
- (char *)"goto_valid",(char *)"!\\valid(r)",58);
+ else __gen_e_acsl_and_3 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_3,(char *)"Assertion",
+ (char *)"goto_valid",(char *)"!\\valid(r)",48);
}
- __retres = 0;
- __e_acsl_delete_block((void *)(& r));
- __e_acsl_delete_block((void *)(& q));
- __e_acsl_delete_block((void *)(& p));
- return __retres;
+ __e_acsl_delete_block((void *)(& a1));
+ goto SECOND;
+ __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),(void *)p,
+ (void *)(& p));
+ __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),(void *)q,
+ (void *)(& q));
+ __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),(void *)r,
+ (void *)(& r));
+ __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)
@@ -235,81 +231,79 @@ int switch_valid(void)
s = & i;
switch (i) {
default:
+ {
+ int a1 = 0;
+ __e_acsl_store_block((void *)(& a1),(size_t)4);
+ __e_acsl_full_init((void *)(& a1));
+ __e_acsl_full_init((void *)(& p));
+ p = & a1;
{
- int a1 = 0;
- __e_acsl_store_block((void *)(& a1),(size_t)4);
- __e_acsl_full_init((void *)(& a1));
- __e_acsl_full_init((void *)(& p));
- p = & a1;
+ int a2 = 0;
+ __e_acsl_store_block((void *)(& a2),(size_t)4);
+ __e_acsl_full_init((void *)(& a2));
+ __e_acsl_full_init((void *)(& q));
+ q = & a2;
+ /*@ assert \valid(p); */
{
- int a2 = 0;
- __e_acsl_store_block((void *)(& a2),(size_t)4);
- __e_acsl_full_init((void *)(& a2));
- __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),
- (void *)p,(void *)(& p));
- __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),
- (void *)q,(void *)(& q));
- __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);
+ 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),
+ (void *)p,(void *)(& p));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
}
- /*@ 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),
- (void *)s,(void *)(& s));
- __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);
+ 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),
+ (void *)q,(void *)(& q));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
- __e_acsl_delete_block((void *)(& a1));
- __e_acsl_delete_block((void *)(& a2));
- break;
- __e_acsl_delete_block((void *)(& a2));
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_2,(char *)"Assertion",
+ (char *)"switch_valid",(char *)"\\valid(q)",77);
}
- { /* sequence */
- __e_acsl_full_init((void *)(& q));
- q = & i;
- __e_acsl_full_init((void *)(& p));
- p = q;
+ /*@ 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),
+ (void *)s,(void *)(& s));
+ __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_full_init((void *)(& s));
- s = (int *)0;
__e_acsl_delete_block((void *)(& a1));
+ __e_acsl_delete_block((void *)(& a2));
+ break;
+ __e_acsl_delete_block((void *)(& a2));
}
+ __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); */
{
@@ -528,11 +522,9 @@ void continue_valid(void)
int i = 0;
while (1) {
int tmp;
- { /* sequence */
- tmp = i;
- i ++;
- ;
- }
+ tmp = i;
+ i ++;
+ ;
if (! tmp) break;
{
/*@ assert ¬\valid(p); */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
index 7b7b067ff37416636bcd53121428533ced6e242e..d2f07efc1d2ea9c95f5fc44008831978b1e86a2d 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
@@ -316,8 +316,8 @@ void __gen_e_acsl_k(void)
else __gen_e_acsl_implies_3 = X + (long)Y == 5L;
__e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
(char *)"k",(char *)"X == 3 && Y == 2 ==> X + Y == 5",43);
- k();
}
+ k();
return;
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
index 93c05dc46f74f6be4e4da41a339acf6a2638c0c7..f1c3f7afb6dfb98de5654eed151989e3ef9098e8 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
@@ -10,21 +10,21 @@ int __gen_e_acsl_main(void)
int __retres;
goto L1;
L1:
- /*@ assert X ≡ 0; */
- __e_acsl_assert(X == 0,(char *)"Assertion",(char *)"main",
- (char *)"X == 0",10);
- X = 1;
+ /*@ assert X ≡ 0; */
+ __e_acsl_assert(X == 0,(char *)"Assertion",(char *)"main",(char *)"X == 0",
+ 10);
+ X = 1;
goto L2;
L2:
- /*@ requires X ≡ 1;
- ensures X ≡ 2; */
- {
- __e_acsl_assert(X == 1,(char *)"Precondition",(char *)"main",
- (char *)"X == 1",12);
- X = 2;
- __e_acsl_assert(X == 2,(char *)"Postcondition",(char *)"main",
- (char *)"X == 2",12);
- }
+ /*@ requires X ≡ 1;
+ ensures X ≡ 2; */
+ {
+ __e_acsl_assert(X == 1,(char *)"Precondition",(char *)"main",
+ (char *)"X == 1",12);
+ X = 2;
+ __e_acsl_assert(X == 2,(char *)"Postcondition",(char *)"main",
+ (char *)"X == 2",12);
+ }
if (X) {
X = 3;
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
index aad0f8d74aec802eedb5c98cdc99b72a16e0405f..6fd208997af1ee105c57e1c393f0ce0edab7f2b1 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
@@ -29,31 +29,34 @@ int search(int elt)
int k;
k = 0;
{
- int __gen_e_acsl_forall;
- int __gen_e_acsl_i;
- int __gen_e_acsl_and;
- __gen_e_acsl_forall = 1;
- __gen_e_acsl_i = 0;
- while (1) {
- if (__gen_e_acsl_i < k) ; else break;
- __e_acsl_assert(__gen_e_acsl_i < 10,(char *)"RTE",(char *)"search",
- (char *)"index_bound: __gen_e_acsl_i < 10",18);
- __e_acsl_assert(0 <= __gen_e_acsl_i,(char *)"RTE",(char *)"search",
- (char *)"index_bound: 0 <= __gen_e_acsl_i",18);
- if (A[__gen_e_acsl_i] < elt) ;
- else {
- __gen_e_acsl_forall = 0;
- goto e_acsl_end_loop1;
+ {
+ int __gen_e_acsl_forall;
+ int __gen_e_acsl_i;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_forall = 1;
+ __gen_e_acsl_i = 0;
+ while (1) {
+ if (__gen_e_acsl_i < k) ; else break;
+ __e_acsl_assert(__gen_e_acsl_i < 10,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: __gen_e_acsl_i < 10",18);
+ __e_acsl_assert(0 <= __gen_e_acsl_i,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: 0 <= __gen_e_acsl_i",18);
+ if (A[__gen_e_acsl_i] < elt) ;
+ else {
+ __gen_e_acsl_forall = 0;
+ goto e_acsl_end_loop1;
+ }
+ __gen_e_acsl_i ++;
}
- __gen_e_acsl_i ++;
+ e_acsl_end_loop1: ;
+ __e_acsl_assert(__gen_e_acsl_forall,(char *)"Invariant",
+ (char *)"search",
+ (char *)"\\forall integer i; 0 <= i < k ==> A[i] < elt",
+ 18);
+ if (0 <= k) __gen_e_acsl_and = k <= 10; else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Invariant",(char *)"search",
+ (char *)"0 <= k <= 10",17);
}
- e_acsl_end_loop1: ;
- __e_acsl_assert(__gen_e_acsl_forall,(char *)"Invariant",(char *)"search",
- (char *)"\\forall integer i; 0 <= i < k ==> A[i] < elt",
- 18);
- if (0 <= k) __gen_e_acsl_and = k <= 10; else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,(char *)"Invariant",(char *)"search",
- (char *)"0 <= k <= 10",17);
/*@ loop invariant 0 ≤ k ≤ 10;
loop invariant ∀ ℤ i; 0 ≤ i < k ⇒ A[i] < elt;
*/
@@ -174,50 +177,50 @@ int __gen_e_acsl_search(int elt)
(char *)"search",
(char *)"\\forall integer i; 0 <= i < 9 ==> A[i] <= A[i + 1]",
7);
- {
- int __gen_e_acsl_forall_2;
- int __gen_e_acsl_j_2;
- __gen_e_acsl_forall_2 = 1;
- __gen_e_acsl_j_2 = 0;
- while (1) {
- if (__gen_e_acsl_j_2 < 10) ; else break;
- __e_acsl_assert(__gen_e_acsl_j_2 < 10,(char *)"RTE",(char *)"search",
- (char *)"index_bound: __gen_e_acsl_j_2 < 10",12);
- __e_acsl_assert(0 <= __gen_e_acsl_j_2,(char *)"RTE",(char *)"search",
- (char *)"index_bound: 0 <= __gen_e_acsl_j_2",12);
- if (A[__gen_e_acsl_j_2] != elt) ;
- else {
- __gen_e_acsl_forall_2 = 0;
- goto e_acsl_end_loop5;
- }
- __gen_e_acsl_j_2 ++;
+ }
+ {
+ int __gen_e_acsl_forall_2;
+ int __gen_e_acsl_j_2;
+ __gen_e_acsl_forall_2 = 1;
+ __gen_e_acsl_j_2 = 0;
+ while (1) {
+ if (__gen_e_acsl_j_2 < 10) ; else break;
+ __e_acsl_assert(__gen_e_acsl_j_2 < 10,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: __gen_e_acsl_j_2 < 10",12);
+ __e_acsl_assert(0 <= __gen_e_acsl_j_2,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: 0 <= __gen_e_acsl_j_2",12);
+ if (A[__gen_e_acsl_j_2] != elt) ;
+ else {
+ __gen_e_acsl_forall_2 = 0;
+ goto e_acsl_end_loop5;
}
- e_acsl_end_loop5: ;
- __gen_e_acsl_at_2 = __gen_e_acsl_forall_2;
+ __gen_e_acsl_j_2 ++;
}
- {
- int __gen_e_acsl_exists;
- int __gen_e_acsl_j;
- __gen_e_acsl_exists = 0;
- __gen_e_acsl_j = 0;
- while (1) {
- if (__gen_e_acsl_j < 10) ; else break;
- __e_acsl_assert(__gen_e_acsl_j < 10,(char *)"RTE",(char *)"search",
- (char *)"index_bound: __gen_e_acsl_j < 10",9);
- __e_acsl_assert(0 <= __gen_e_acsl_j,(char *)"RTE",(char *)"search",
- (char *)"index_bound: 0 <= __gen_e_acsl_j",9);
- if (! (A[__gen_e_acsl_j] == elt)) ;
- else {
- __gen_e_acsl_exists = 1;
- goto e_acsl_end_loop4;
- }
- __gen_e_acsl_j ++;
+ e_acsl_end_loop5: ;
+ __gen_e_acsl_at_2 = __gen_e_acsl_forall_2;
+ }
+ {
+ int __gen_e_acsl_exists;
+ int __gen_e_acsl_j;
+ __gen_e_acsl_exists = 0;
+ __gen_e_acsl_j = 0;
+ while (1) {
+ if (__gen_e_acsl_j < 10) ; else break;
+ __e_acsl_assert(__gen_e_acsl_j < 10,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: __gen_e_acsl_j < 10",9);
+ __e_acsl_assert(0 <= __gen_e_acsl_j,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: 0 <= __gen_e_acsl_j",9);
+ if (! (A[__gen_e_acsl_j] == elt)) ;
+ else {
+ __gen_e_acsl_exists = 1;
+ goto e_acsl_end_loop4;
}
- e_acsl_end_loop4: ;
- __gen_e_acsl_at = __gen_e_acsl_exists;
+ __gen_e_acsl_j ++;
}
- __retres = search(elt);
+ e_acsl_end_loop4: ;
+ __gen_e_acsl_at = __gen_e_acsl_exists;
}
+ __retres = search(elt);
{
int __gen_e_acsl_implies;
int __gen_e_acsl_implies_2;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
index 9e517c9ce5af02cd174e8b4a87c129e9c4b01516..30d11105244eb9351f2f097bfdd4c5bdb92f9651 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
@@ -40,45 +40,45 @@ int main(int argc, char const **argv)
goto RET;
}
AGAIN:
+ {
+ int a;
+ __e_acsl_store_block((void *)(& a),(size_t)4);
+ __e_acsl_full_init((void *)(& a));
+ a = 1;
+ /*@ assert \valid(&a); */
{
- int a;
- __e_acsl_store_block((void *)(& a),(size_t)4);
- __e_acsl_full_init((void *)(& a));
- a = 1;
- /*@ assert \valid(&a); */
- {
- int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
- (void *)(& a),(void *)(& a));
- __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",
- (char *)"main",(char *)"\\valid(&a)",25);
- }
- if (t == 2) {
- __gen_e_acsl_printf_va_2(__gen_e_acsl_literal_string,t,
- (char *)__gen_e_acsl_literal_string_3);
- __e_acsl_delete_block((void *)(& a));
- goto UP;
- }
- else t ++;
- int b = 15;
- __e_acsl_store_block((void *)(& b),(size_t)4);
- __e_acsl_full_init((void *)(& b));
- /*@ assert \valid(&b); */
- {
- int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int),
- (void *)(& b),(void *)(& b));
- __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
- (char *)"main",(char *)"\\valid(&b)",36);
- }
- __gen_e_acsl_printf_va_3(__gen_e_acsl_literal_string,t,
- (char *)__gen_e_acsl_literal_string_4);
- __e_acsl_delete_block((void *)(& a));
- __e_acsl_delete_block((void *)(& b));
- goto AGAIN;
- __e_acsl_delete_block((void *)(& b));
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
+ (void *)(& a),(void *)(& a));
+ __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&a)",25);
+ }
+ if (t == 2) {
+ __gen_e_acsl_printf_va_2(__gen_e_acsl_literal_string,t,
+ (char *)__gen_e_acsl_literal_string_3);
__e_acsl_delete_block((void *)(& a));
+ goto UP;
}
+ else t ++;
+ int b = 15;
+ __e_acsl_store_block((void *)(& b),(size_t)4);
+ __e_acsl_full_init((void *)(& b));
+ /*@ assert \valid(&b); */
+ {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int),
+ (void *)(& b),(void *)(& b));
+ __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
+ (char *)"main",(char *)"\\valid(&b)",36);
+ }
+ __gen_e_acsl_printf_va_3(__gen_e_acsl_literal_string,t,
+ (char *)__gen_e_acsl_literal_string_4);
+ __e_acsl_delete_block((void *)(& a));
+ __e_acsl_delete_block((void *)(& b));
+ goto AGAIN;
+ __e_acsl_delete_block((void *)(& b));
+ __e_acsl_delete_block((void *)(& a));
+ }
RET: __retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_init.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_init.c
new file mode 100644
index 0000000000000000000000000000000000000000..3975152cb4081982cd4b55ada9d3b32463a6fff7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_init.c
@@ -0,0 +1,38 @@
+/* Generated by Frama-C */
+#include "stdlib.h"
+int X = 0;
+int *p = & X;
+int f(void)
+{
+ /*@ assert Value: mem_access: \valid_read(p); */
+ {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
+ __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"Assertion",(char *)"f",
+ (char *)"Value: mem_access: \\valid_read(p)",12);
+ }
+ int x = *p;
+ return x;
+}
+
+void __e_acsl_globals_init(void)
+{
+ __e_acsl_store_block((void *)(& p),(size_t)4);
+ __e_acsl_full_init((void *)(& p));
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)4);
+ __e_acsl_globals_init();
+ f();
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
index 876d034eec1c449b5258eb5f0fea233c0c230098..106da5a584157f745b8e9098899dc533a84e5e66 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
@@ -68,26 +68,29 @@ int main(void)
requires x + y ≡ 5;
*/
{
- int __gen_e_acsl_implies;
- int __gen_e_acsl_and;
- int __gen_e_acsl_implies_2;
- int __gen_e_acsl_and_2;
- int __gen_e_acsl_implies_3;
- if (! (x == 1)) __gen_e_acsl_implies = 1;
- else __gen_e_acsl_implies = x == 0;
- __e_acsl_assert(__gen_e_acsl_implies,(char *)"Precondition",
- (char *)"main",(char *)"x == 1 ==> x == 0",33);
- if (x == 3) __gen_e_acsl_and = y == 2; else __gen_e_acsl_and = 0;
- if (! __gen_e_acsl_and) __gen_e_acsl_implies_2 = 1;
- else __gen_e_acsl_implies_2 = x == 3;
- __e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Precondition",
- (char *)"main",(char *)"x == 3 && y == 2 ==> x == 3",37);
- if (x == 3) __gen_e_acsl_and_2 = y == 2; else __gen_e_acsl_and_2 = 0;
- if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1;
- else __gen_e_acsl_implies_3 = x + (long)y == 5L;
- __e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
- (char *)"main",(char *)"x == 3 && y == 2 ==> x + y == 5",
- 38);
+ {
+ int __gen_e_acsl_implies;
+ int __gen_e_acsl_and;
+ int __gen_e_acsl_implies_2;
+ int __gen_e_acsl_and_2;
+ int __gen_e_acsl_implies_3;
+ if (! (x == 1)) __gen_e_acsl_implies = 1;
+ else __gen_e_acsl_implies = x == 0;
+ __e_acsl_assert(__gen_e_acsl_implies,(char *)"Precondition",
+ (char *)"main",(char *)"x == 1 ==> x == 0",33);
+ if (x == 3) __gen_e_acsl_and = y == 2; else __gen_e_acsl_and = 0;
+ if (! __gen_e_acsl_and) __gen_e_acsl_implies_2 = 1;
+ else __gen_e_acsl_implies_2 = x == 3;
+ __e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Precondition",
+ (char *)"main",(char *)"x == 3 && y == 2 ==> x == 3",
+ 37);
+ if (x == 3) __gen_e_acsl_and_2 = y == 2; else __gen_e_acsl_and_2 = 0;
+ if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1;
+ else __gen_e_acsl_implies_3 = x + (long)y == 5L;
+ __e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
+ (char *)"main",
+ (char *)"x == 3 && y == 2 ==> x + y == 5",38);
+ }
x += y;
}
/*@ requires x ≡ 5; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_init.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/local_init.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..88cee4a0c74964b9aa8d0e1c7fb86f7fea60b9bc
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle
@@ -0,0 +1,30 @@
+[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
+[kernel] Parsing tests/runtime/local_init.c (with preprocessing)
+[value] Analyzing an incomplete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value:initial-state] Values of globals at initialization
+ __fc_random_counter ∈ [--..--]
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __fc_mblen_state ∈ [--..--]
+ __fc_mbtowc_state ∈ [--..--]
+ __fc_wctomb_state ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __e_acsl_heap_allocation_size ∈ [--..--]
+ X ∈ [--..--]
+ p ∈ {{ NULL ; &S_p[0] }}
+ S_p[0..1] ∈ [--..--]
+tests/runtime/local_init.c:12:[value] warning: out of bounds read. assert \valid_read(p);
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value:final-states] Values at end of function f:
+ x ∈ [--..--]
+[value:final-states] Values at end of function main:
+ __retres ∈ {0}
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index a159cdea254416f7429a1357bf7b2fcfd9261655..81c69a3726d955c7d99ca0d2698db9bed4cf424f 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -647,7 +647,8 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
else
acc)
global_vars
- [ Misc.mk_call ~loc (Misc.mk_api_name "memory_clean") []; ret ]
+ [ Misc.mk_call ~loc (Misc.mk_api_name "memory_clean") [];
+ ret ]
in
b.bstmts <- List.rev l @ delete_stmts
end;
@@ -664,13 +665,12 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(* must generate [pre_block] which includes [stmt] before generating
[post_block] *)
let pre_block, env =
- Env.pop_and_get env new_stmt ~global_clear:false Env.After
- in
- let pre_block =
- if pre_block.blocals = [] then
- Cil.transient_block pre_block
- else
- pre_block
+ Env.pop_and_get
+ ~split:true
+ env
+ new_stmt
+ ~global_clear:false
+ Env.After
in
let env = mk_post_env (Env.push env) in
let post_block, env =
@@ -681,14 +681,14 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
Env.Before
in
(match stmt.skind with
- | Instr (Local_init (vi, _, _)) when
- Mmodel_analysis.old_must_model_vi self#behavior ~kf vi ->
- let vi = Cil.get_varinfo self#behavior vi in
- post_block.bstmts <-
- post_block.bstmts @
- [Misc.mk_store_stmt vi; Misc.mk_full_init_stmt vi]
- | _ -> ());
- let post_block = Cil.flatten_transient_sub_blocks post_block in
+ | Instr (Local_init (vi, _, _)) when
+ Mmodel_analysis.old_must_model_vi 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