diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 040ac21002e44507049561813eae547892137e6b..8494d38a80eae803d5fc8e2c1204b8b0119eb405 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -37,6 +37,8 @@
- ne pas appeler __malloc et __free quand pas nÈcessaire. NÈcessite d'avoir
malloc, __malloc, __e_acsl_malloc, __e_acsl__malloc (idem pour free)
- analysis: optimize it by performing no join over sets anymore
+- analysis: fixed incorrectness in presence of recursive functions
+- RTE: potential duplication (e.g. with **p)
##############
# KNOWN BUGS #
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 85f7b2bdc748ef22663a971020c768c7513d8460..f2b9c3db37f66ca8ce0c3e658b39aa27fc49a44e 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -161,10 +161,17 @@ module rec Transfer
let ty = Cil.typeOf e in
is_ptr_or_array ty
- let rec register_term_lval kf varinfos (thost, _) = match thost with
+ let rec register_term_lval kf varinfos (thost, _) =
+ let add_vi kf vi =
+ Options.feedback ~level:4 ~dkey "monitoring %a from annotation of %a."
+ Printer.pp_varinfo vi
+ Kernel_function.pretty kf;
+ Varinfo.Set.add vi varinfos
+ in
+ match thost with
| TVar { lv_origin = None } -> varinfos
- | TVar { lv_origin = Some vi } -> Varinfo.Set.add vi varinfos
- | TResult _ -> Varinfo.Set.add (Misc.result_vi kf) varinfos
+ | TVar { lv_origin = Some vi } -> add_vi kf vi
+ | TResult _ -> add_vi kf (Misc.result_vi kf)
| TMem t -> register_term kf varinfos t
and register_term kf varinfos term = match term.term_node with
@@ -343,7 +350,12 @@ module rec Transfer
if is_ptr_or_array_exp e && Varinfo.Set.mem vi state then
match base_addr e with
| None -> state
- | Some vi_e -> Varinfo.Set.add vi_e state
+ | Some vi_e ->
+ Options.feedback ~level:4 ~dkey
+ "monitoring %a from %a."
+ Printer.pp_varinfo vi_e
+ Printer.pp_lval (lhost, NoOffset);
+ Varinfo.Set.add vi_e state
else
state
in
diff --git a/src/plugins/e-acsl/pre_visit.ml b/src/plugins/e-acsl/pre_visit.ml
index 1fe72a66a82f26306b7a4291718582cca759fbac..f62adb6f482638ce9ec44698125ac3762919d5b7 100644
--- a/src/plugins/e-acsl/pre_visit.ml
+++ b/src/plugins/e-acsl/pre_visit.ml
@@ -346,7 +346,9 @@ class dup_functions_visitor prj = object (self)
f.globals <- self#insert_libc f.globals;
f)
- initializer reset ()
+ initializer
+ Project.copy ~selection:(Plugin.get_selection ()) prj;
+ reset ()
end
@@ -357,7 +359,6 @@ let dup_functions () =
"e_acsl_dup_functions"
(new dup_functions_visitor)
in
- Project.copy ~selection:(Plugin.get_selection ()) prj;
Queue.iter (fun f -> f ()) actions;
prj
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 3c3134c100d8ee631e8b6c8fb0cf03cb5df35d8b..7280c80ad88ae623ee86cb1818fcd6e02d1cab43 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
@@ -87,6 +87,10 @@ extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
+ size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -123,7 +127,7 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& __retres),8U);
__retres = __malloc(size);
__delete_block((void *)(& __retres));
return __retres;
@@ -151,7 +155,7 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __store_block((void *)(& p),4U);
+ __store_block((void *)(& p),8U);
__store_block((void *)(& __e_acsl_at),4U);
__e_acsl_at = p != (void *)0;
__free(p);
@@ -171,16 +175,16 @@ int Z;
int *f(int *x)
{
int *y;
- __store_block((void *)(& y),4U);
+ __store_block((void *)(& y),8U);
/*@ assert ¬\valid(y); */
{
int __e_acsl_initialized;
int __e_acsl_and;
- __store_block((void *)(& x),4U);
- __e_acsl_initialized = __initialized((void *)(& y),sizeof(int *));
+ __store_block((void *)(& x),8U);
+ __e_acsl_initialized = __initialized((void *)(& y),(size_t)sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = __valid((void *)y,sizeof(int));
+ __e_acsl_valid = __valid((void *)y,(size_t)sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else __e_acsl_and = 0;
@@ -192,7 +196,7 @@ int *f(int *x)
/*@ assert \valid(x); */
{
int __e_acsl_valid_2;
- __e_acsl_valid_2 = __valid((void *)x,sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)x,(size_t)sizeof(int));
e_acsl_assert(__e_acsl_valid_2,(char *)"Assertion",(char *)"f",
(char *)"\\valid(x)",21);
}
@@ -206,18 +210,18 @@ int *f(int *x)
int *__e_acsl_f(int *x)
{
int *__retres;
- __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& __retres),8U);
{
int __e_acsl_valid;
- __store_block((void *)(& x),4U);
- __e_acsl_valid = __valid((void *)x,sizeof(int));
+ __store_block((void *)(& x),8U);
+ __e_acsl_valid = __valid((void *)x,(size_t)sizeof(int));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"f",
(char *)"\\valid(x)",15);
__retres = f(x);
}
{
int __e_acsl_valid_2;
- __e_acsl_valid_2 = __valid((void *)__retres,sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)__retres,(size_t)sizeof(int));
e_acsl_assert(__e_acsl_valid_2,(char *)"Postcondition",(char *)"f",
(char *)"\\valid(\\result)",16);
__delete_block((void *)(& x));
@@ -229,7 +233,7 @@ int *__e_acsl_f(int *x)
void e_acsl_global_init(void)
{
__store_block((void *)(& Z),4U);
- __store_block((void *)(& X),4U);
+ __store_block((void *)(& X),8U);
return;
}
@@ -238,11 +242,15 @@ int main(void)
int __retres;
int *a;
int *b;
+ int **c;
+ int ***d;
int n;
e_acsl_global_init();
__store_block((void *)(& n),4U);
- __store_block((void *)(& b),4U);
- __store_block((void *)(& a),4U);
+ __store_block((void *)(& d),8U);
+ __store_block((void *)(& c),8U);
+ __store_block((void *)(& b),8U);
+ __store_block((void *)(& a),8U);
__full_init((void *)(& n));
n = 0;
/*@ assert (¬\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
@@ -251,20 +259,21 @@ int main(void)
int __e_acsl_and;
int __e_acsl_and_3;
int __e_acsl_and_4;
- __e_acsl_initialized = __initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized = __initialized((void *)(& a),(size_t)sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = __valid((void *)a,sizeof(int));
+ __e_acsl_valid = __valid((void *)a,(size_t)sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else __e_acsl_and = 0;
if (! __e_acsl_and) {
int __e_acsl_initialized_2;
int __e_acsl_and_2;
- __e_acsl_initialized_2 = __initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_2 = __initialized((void *)(& b),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_2) {
int __e_acsl_valid_2;
- __e_acsl_valid_2 = __valid((void *)b,sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)b,(size_t)sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_2;
}
else __e_acsl_and_2 = 0;
@@ -273,7 +282,7 @@ int main(void)
else __e_acsl_and_3 = 0;
if (__e_acsl_and_3) {
int __e_acsl_valid_3;
- __e_acsl_valid_3 = __valid((void *)X,sizeof(int));
+ __e_acsl_valid_3 = __valid((void *)X,(size_t)sizeof(int));
__e_acsl_and_4 = ! __e_acsl_valid_3;
}
else __e_acsl_and_4 = 0;
@@ -281,27 +290,29 @@ int main(void)
(char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",27);
}
__full_init((void *)(& a));
- a = (int *)__e_acsl_malloc(sizeof(int));
+ a = (int *)__e_acsl_malloc((unsigned int)sizeof(int));
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
{
int __e_acsl_initialized_3;
int __e_acsl_and_5;
int __e_acsl_and_7;
int __e_acsl_and_8;
- __e_acsl_initialized_3 = __initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_3 = __initialized((void *)(& a),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_3) {
int __e_acsl_valid_4;
- __e_acsl_valid_4 = __valid((void *)a,sizeof(int));
+ __e_acsl_valid_4 = __valid((void *)a,(size_t)sizeof(int));
__e_acsl_and_5 = __e_acsl_valid_4;
}
else __e_acsl_and_5 = 0;
if (__e_acsl_and_5) {
int __e_acsl_initialized_4;
int __e_acsl_and_6;
- __e_acsl_initialized_4 = __initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_4 = __initialized((void *)(& b),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_4) {
int __e_acsl_valid_5;
- __e_acsl_valid_5 = __valid((void *)b,sizeof(int));
+ __e_acsl_valid_5 = __valid((void *)b,(size_t)sizeof(int));
__e_acsl_and_6 = __e_acsl_valid_5;
}
else __e_acsl_and_6 = 0;
@@ -310,7 +321,7 @@ int main(void)
else __e_acsl_and_7 = 0;
if (__e_acsl_and_7) {
int __e_acsl_valid_6;
- __e_acsl_valid_6 = __valid((void *)X,sizeof(int));
+ __e_acsl_valid_6 = __valid((void *)X,(size_t)sizeof(int));
__e_acsl_and_8 = ! __e_acsl_valid_6;
}
else __e_acsl_and_8 = 0;
@@ -324,20 +335,22 @@ int main(void)
int __e_acsl_and_9;
int __e_acsl_and_11;
int __e_acsl_and_12;
- __e_acsl_initialized_5 = __initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_5 = __initialized((void *)(& a),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_5) {
int __e_acsl_valid_7;
- __e_acsl_valid_7 = __valid((void *)a,sizeof(int));
+ __e_acsl_valid_7 = __valid((void *)a,(size_t)sizeof(int));
__e_acsl_and_9 = __e_acsl_valid_7;
}
else __e_acsl_and_9 = 0;
if (__e_acsl_and_9) {
int __e_acsl_initialized_6;
int __e_acsl_and_10;
- __e_acsl_initialized_6 = __initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_6 = __initialized((void *)(& b),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_6) {
int __e_acsl_valid_8;
- __e_acsl_valid_8 = __valid((void *)b,sizeof(int));
+ __e_acsl_valid_8 = __valid((void *)b,(size_t)sizeof(int));
__e_acsl_and_10 = __e_acsl_valid_8;
}
else __e_acsl_and_10 = 0;
@@ -346,7 +359,7 @@ int main(void)
else __e_acsl_and_11 = 0;
if (__e_acsl_and_11) {
int __e_acsl_valid_9;
- __e_acsl_valid_9 = __valid((void *)X,sizeof(int));
+ __e_acsl_valid_9 = __valid((void *)X,(size_t)sizeof(int));
__e_acsl_and_12 = __e_acsl_valid_9;
}
else __e_acsl_and_12 = 0;
@@ -361,20 +374,22 @@ int main(void)
int __e_acsl_and_13;
int __e_acsl_and_15;
int __e_acsl_and_16;
- __e_acsl_initialized_7 = __initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_7 = __initialized((void *)(& a),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_7) {
int __e_acsl_valid_10;
- __e_acsl_valid_10 = __valid((void *)a,sizeof(int));
+ __e_acsl_valid_10 = __valid((void *)a,(size_t)sizeof(int));
__e_acsl_and_13 = __e_acsl_valid_10;
}
else __e_acsl_and_13 = 0;
if (__e_acsl_and_13) {
int __e_acsl_initialized_8;
int __e_acsl_and_14;
- __e_acsl_initialized_8 = __initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_8 = __initialized((void *)(& b),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_8) {
int __e_acsl_valid_11;
- __e_acsl_valid_11 = __valid((void *)b,sizeof(int));
+ __e_acsl_valid_11 = __valid((void *)b,(size_t)sizeof(int));
__e_acsl_and_14 = __e_acsl_valid_11;
}
else __e_acsl_and_14 = 0;
@@ -383,7 +398,7 @@ int main(void)
else __e_acsl_and_15 = 0;
if (__e_acsl_and_15) {
int __e_acsl_valid_12;
- __e_acsl_valid_12 = __valid((void *)X,sizeof(int));
+ __e_acsl_valid_12 = __valid((void *)X,(size_t)sizeof(int));
__e_acsl_and_16 = __e_acsl_valid_12;
}
else __e_acsl_and_16 = 0;
@@ -397,20 +412,22 @@ int main(void)
int __e_acsl_and_17;
int __e_acsl_and_19;
int __e_acsl_and_20;
- __e_acsl_initialized_9 = __initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_9 = __initialized((void *)(& a),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_9) {
int __e_acsl_valid_13;
- __e_acsl_valid_13 = __valid((void *)a,sizeof(int));
+ __e_acsl_valid_13 = __valid((void *)a,(size_t)sizeof(int));
__e_acsl_and_17 = __e_acsl_valid_13;
}
else __e_acsl_and_17 = 0;
if (__e_acsl_and_17) {
int __e_acsl_initialized_10;
int __e_acsl_and_18;
- __e_acsl_initialized_10 = __initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_10 = __initialized((void *)(& b),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_10) {
int __e_acsl_valid_14;
- __e_acsl_valid_14 = __valid((void *)b,sizeof(int));
+ __e_acsl_valid_14 = __valid((void *)b,(size_t)sizeof(int));
__e_acsl_and_18 = __e_acsl_valid_14;
}
else __e_acsl_and_18 = 0;
@@ -419,60 +436,151 @@ int main(void)
else __e_acsl_and_19 = 0;
if (__e_acsl_and_19) {
int __e_acsl_valid_15;
- __e_acsl_valid_15 = __valid((void *)X,sizeof(int));
+ __e_acsl_valid_15 = __valid((void *)X,(size_t)sizeof(int));
__e_acsl_and_20 = __e_acsl_valid_15;
}
else __e_acsl_and_20 = 0;
e_acsl_assert(__e_acsl_and_20,(char *)"Assertion",(char *)"main",
(char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",35);
}
- __e_acsl_free((void *)a);
- /*@ assert (¬\valid(a) ∧ \valid(b)) ∧ \valid(X); */
+ __full_init((void *)(& c));
+ c = & a;
+ __full_init((void *)(& d));
+ d = & c;
+ /*@ assert \valid(*c); */
{
int __e_acsl_initialized_11;
- int __e_acsl_and_21;
- int __e_acsl_and_23;
- int __e_acsl_and_24;
- __e_acsl_initialized_11 = __initialized((void *)(& a),sizeof(int *));
+ int __e_acsl_and_22;
+ __e_acsl_initialized_11 = __initialized((void *)c,(size_t)sizeof(int *));
if (__e_acsl_initialized_11) {
- int __e_acsl_valid_16;
- __e_acsl_valid_16 = __valid((void *)a,sizeof(int));
- __e_acsl_and_21 = __e_acsl_valid_16;
- }
- else __e_acsl_and_21 = 0;
- if (! __e_acsl_and_21) {
int __e_acsl_initialized_12;
- int __e_acsl_and_22;
- __e_acsl_initialized_12 = __initialized((void *)(& b),sizeof(int *));
+ int __e_acsl_and_21;
+ int __e_acsl_valid_16;
+ __e_acsl_initialized_12 = __initialized((void *)(& c),
+ (size_t)sizeof(int **));
if (__e_acsl_initialized_12) {
- int __e_acsl_valid_17;
- __e_acsl_valid_17 = __valid((void *)b,sizeof(int));
- __e_acsl_and_22 = __e_acsl_valid_17;
+ int __e_acsl_valid_read;
+ __e_acsl_valid_read = __valid_read((void *)c,(size_t)sizeof(int *));
+ __e_acsl_and_21 = __e_acsl_valid_read;
}
- else __e_acsl_and_22 = 0;
- __e_acsl_and_23 = __e_acsl_and_22;
+ else __e_acsl_and_21 = 0;
+ e_acsl_assert(__e_acsl_and_21,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(c)",0);
+ __e_acsl_valid_16 = __valid((void *)*c,(size_t)sizeof(int));
+ __e_acsl_and_22 = __e_acsl_valid_16;
}
- else __e_acsl_and_23 = 0;
- if (__e_acsl_and_23) {
+ else __e_acsl_and_22 = 0;
+ e_acsl_assert(__e_acsl_and_22,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(*c)",38);
+ }
+ /*@ assert \valid(*(*d)); */
+ {
+ int __e_acsl_valid_read_2;
+ int __e_acsl_initialized_13;
+ int __e_acsl_and_26;
+ __e_acsl_valid_read_2 = __valid_read((void *)d,(size_t)sizeof(int **));
+ e_acsl_assert(__e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(d)",0);
+ __e_acsl_initialized_13 = __initialized((void *)*d,(size_t)sizeof(int *));
+ if (__e_acsl_initialized_13) {
+ int __e_acsl_initialized_14;
+ int __e_acsl_and_24;
+ int __e_acsl_initialized_16;
+ int __e_acsl_and_25;
+ int __e_acsl_valid_17;
+ __e_acsl_initialized_14 = __initialized((void *)d,
+ (size_t)sizeof(int **));
+ if (__e_acsl_initialized_14) {
+ int __e_acsl_initialized_15;
+ int __e_acsl_and_23;
+ int __e_acsl_valid_read_4;
+ __e_acsl_initialized_15 = __initialized((void *)(& d),
+ (size_t)sizeof(int ***));
+ if (__e_acsl_initialized_15) {
+ int __e_acsl_valid_read_3;
+ __e_acsl_valid_read_3 = __valid_read((void *)d,
+ (size_t)sizeof(int **));
+ __e_acsl_and_23 = __e_acsl_valid_read_3;
+ }
+ else __e_acsl_and_23 = 0;
+ e_acsl_assert(__e_acsl_and_23,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(d)",0);
+ __e_acsl_valid_read_4 = __valid_read((void *)*d,
+ (size_t)sizeof(int *));
+ __e_acsl_and_24 = __e_acsl_valid_read_4;
+ }
+ else __e_acsl_and_24 = 0;
+ e_acsl_assert(__e_acsl_and_24,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(*d)",0);
+ __e_acsl_initialized_16 = __initialized((void *)(& d),
+ (size_t)sizeof(int ***));
+ if (__e_acsl_initialized_16) {
+ int __e_acsl_valid_read_5;
+ __e_acsl_valid_read_5 = __valid_read((void *)d,
+ (size_t)sizeof(int **));
+ __e_acsl_and_25 = __e_acsl_valid_read_5;
+ }
+ else __e_acsl_and_25 = 0;
+ e_acsl_assert(__e_acsl_and_25,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(d)",0);
+ __e_acsl_valid_17 = __valid((void *)*(*d),(size_t)sizeof(int));
+ __e_acsl_and_26 = __e_acsl_valid_17;
+ }
+ else __e_acsl_and_26 = 0;
+ e_acsl_assert(__e_acsl_and_26,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(*(*d))",39);
+ }
+ __e_acsl_free((void *)a);
+ /*@ assert (¬\valid(a) ∧ \valid(b)) ∧ \valid(X); */
+ {
+ int __e_acsl_initialized_17;
+ int __e_acsl_and_27;
+ int __e_acsl_and_29;
+ int __e_acsl_and_30;
+ __e_acsl_initialized_17 = __initialized((void *)(& a),
+ (size_t)sizeof(int *));
+ if (__e_acsl_initialized_17) {
int __e_acsl_valid_18;
- __e_acsl_valid_18 = __valid((void *)X,sizeof(int));
- __e_acsl_and_24 = __e_acsl_valid_18;
+ __e_acsl_valid_18 = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_and_27 = __e_acsl_valid_18;
+ }
+ else __e_acsl_and_27 = 0;
+ if (! __e_acsl_and_27) {
+ int __e_acsl_initialized_18;
+ int __e_acsl_and_28;
+ __e_acsl_initialized_18 = __initialized((void *)(& b),
+ (size_t)sizeof(int *));
+ if (__e_acsl_initialized_18) {
+ int __e_acsl_valid_19;
+ __e_acsl_valid_19 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_and_28 = __e_acsl_valid_19;
+ }
+ else __e_acsl_and_28 = 0;
+ __e_acsl_and_29 = __e_acsl_and_28;
+ }
+ else __e_acsl_and_29 = 0;
+ if (__e_acsl_and_29) {
+ int __e_acsl_valid_20;
+ __e_acsl_valid_20 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_and_30 = __e_acsl_valid_20;
}
- else __e_acsl_and_24 = 0;
- e_acsl_assert(__e_acsl_and_24,(char *)"Assertion",(char *)"main",
- (char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",37);
+ else __e_acsl_and_30 = 0;
+ e_acsl_assert(__e_acsl_and_30,(char *)"Assertion",(char *)"main",
+ (char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",41);
}
/*@ assert \valid(&Z); */
{
- int __e_acsl_valid_19;
- __e_acsl_valid_19 = __valid((void *)(& Z),sizeof(int));
- e_acsl_assert(__e_acsl_valid_19,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(&Z)",38);
+ int __e_acsl_valid_21;
+ __e_acsl_valid_21 = __valid((void *)(& Z),(size_t)sizeof(int));
+ e_acsl_assert(__e_acsl_valid_21,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&Z)",42);
}
__retres = 0;
__delete_block((void *)(& Z));
__delete_block((void *)(& X));
__delete_block((void *)(& n));
+ __delete_block((void *)(& d));
+ __delete_block((void *)(& c));
__delete_block((void *)(& b));
__delete_block((void *)(& a));
__clean();
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 3c3134c100d8ee631e8b6c8fb0cf03cb5df35d8b..7280c80ad88ae623ee86cb1818fcd6e02d1cab43 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
@@ -87,6 +87,10 @@ extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
+ size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -123,7 +127,7 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& __retres),8U);
__retres = __malloc(size);
__delete_block((void *)(& __retres));
return __retres;
@@ -151,7 +155,7 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __store_block((void *)(& p),4U);
+ __store_block((void *)(& p),8U);
__store_block((void *)(& __e_acsl_at),4U);
__e_acsl_at = p != (void *)0;
__free(p);
@@ -171,16 +175,16 @@ int Z;
int *f(int *x)
{
int *y;
- __store_block((void *)(& y),4U);
+ __store_block((void *)(& y),8U);
/*@ assert ¬\valid(y); */
{
int __e_acsl_initialized;
int __e_acsl_and;
- __store_block((void *)(& x),4U);
- __e_acsl_initialized = __initialized((void *)(& y),sizeof(int *));
+ __store_block((void *)(& x),8U);
+ __e_acsl_initialized = __initialized((void *)(& y),(size_t)sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = __valid((void *)y,sizeof(int));
+ __e_acsl_valid = __valid((void *)y,(size_t)sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else __e_acsl_and = 0;
@@ -192,7 +196,7 @@ int *f(int *x)
/*@ assert \valid(x); */
{
int __e_acsl_valid_2;
- __e_acsl_valid_2 = __valid((void *)x,sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)x,(size_t)sizeof(int));
e_acsl_assert(__e_acsl_valid_2,(char *)"Assertion",(char *)"f",
(char *)"\\valid(x)",21);
}
@@ -206,18 +210,18 @@ int *f(int *x)
int *__e_acsl_f(int *x)
{
int *__retres;
- __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& __retres),8U);
{
int __e_acsl_valid;
- __store_block((void *)(& x),4U);
- __e_acsl_valid = __valid((void *)x,sizeof(int));
+ __store_block((void *)(& x),8U);
+ __e_acsl_valid = __valid((void *)x,(size_t)sizeof(int));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"f",
(char *)"\\valid(x)",15);
__retres = f(x);
}
{
int __e_acsl_valid_2;
- __e_acsl_valid_2 = __valid((void *)__retres,sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)__retres,(size_t)sizeof(int));
e_acsl_assert(__e_acsl_valid_2,(char *)"Postcondition",(char *)"f",
(char *)"\\valid(\\result)",16);
__delete_block((void *)(& x));
@@ -229,7 +233,7 @@ int *__e_acsl_f(int *x)
void e_acsl_global_init(void)
{
__store_block((void *)(& Z),4U);
- __store_block((void *)(& X),4U);
+ __store_block((void *)(& X),8U);
return;
}
@@ -238,11 +242,15 @@ int main(void)
int __retres;
int *a;
int *b;
+ int **c;
+ int ***d;
int n;
e_acsl_global_init();
__store_block((void *)(& n),4U);
- __store_block((void *)(& b),4U);
- __store_block((void *)(& a),4U);
+ __store_block((void *)(& d),8U);
+ __store_block((void *)(& c),8U);
+ __store_block((void *)(& b),8U);
+ __store_block((void *)(& a),8U);
__full_init((void *)(& n));
n = 0;
/*@ assert (¬\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
@@ -251,20 +259,21 @@ int main(void)
int __e_acsl_and;
int __e_acsl_and_3;
int __e_acsl_and_4;
- __e_acsl_initialized = __initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized = __initialized((void *)(& a),(size_t)sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = __valid((void *)a,sizeof(int));
+ __e_acsl_valid = __valid((void *)a,(size_t)sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else __e_acsl_and = 0;
if (! __e_acsl_and) {
int __e_acsl_initialized_2;
int __e_acsl_and_2;
- __e_acsl_initialized_2 = __initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_2 = __initialized((void *)(& b),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_2) {
int __e_acsl_valid_2;
- __e_acsl_valid_2 = __valid((void *)b,sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)b,(size_t)sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_2;
}
else __e_acsl_and_2 = 0;
@@ -273,7 +282,7 @@ int main(void)
else __e_acsl_and_3 = 0;
if (__e_acsl_and_3) {
int __e_acsl_valid_3;
- __e_acsl_valid_3 = __valid((void *)X,sizeof(int));
+ __e_acsl_valid_3 = __valid((void *)X,(size_t)sizeof(int));
__e_acsl_and_4 = ! __e_acsl_valid_3;
}
else __e_acsl_and_4 = 0;
@@ -281,27 +290,29 @@ int main(void)
(char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",27);
}
__full_init((void *)(& a));
- a = (int *)__e_acsl_malloc(sizeof(int));
+ a = (int *)__e_acsl_malloc((unsigned int)sizeof(int));
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
{
int __e_acsl_initialized_3;
int __e_acsl_and_5;
int __e_acsl_and_7;
int __e_acsl_and_8;
- __e_acsl_initialized_3 = __initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_3 = __initialized((void *)(& a),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_3) {
int __e_acsl_valid_4;
- __e_acsl_valid_4 = __valid((void *)a,sizeof(int));
+ __e_acsl_valid_4 = __valid((void *)a,(size_t)sizeof(int));
__e_acsl_and_5 = __e_acsl_valid_4;
}
else __e_acsl_and_5 = 0;
if (__e_acsl_and_5) {
int __e_acsl_initialized_4;
int __e_acsl_and_6;
- __e_acsl_initialized_4 = __initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_4 = __initialized((void *)(& b),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_4) {
int __e_acsl_valid_5;
- __e_acsl_valid_5 = __valid((void *)b,sizeof(int));
+ __e_acsl_valid_5 = __valid((void *)b,(size_t)sizeof(int));
__e_acsl_and_6 = __e_acsl_valid_5;
}
else __e_acsl_and_6 = 0;
@@ -310,7 +321,7 @@ int main(void)
else __e_acsl_and_7 = 0;
if (__e_acsl_and_7) {
int __e_acsl_valid_6;
- __e_acsl_valid_6 = __valid((void *)X,sizeof(int));
+ __e_acsl_valid_6 = __valid((void *)X,(size_t)sizeof(int));
__e_acsl_and_8 = ! __e_acsl_valid_6;
}
else __e_acsl_and_8 = 0;
@@ -324,20 +335,22 @@ int main(void)
int __e_acsl_and_9;
int __e_acsl_and_11;
int __e_acsl_and_12;
- __e_acsl_initialized_5 = __initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_5 = __initialized((void *)(& a),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_5) {
int __e_acsl_valid_7;
- __e_acsl_valid_7 = __valid((void *)a,sizeof(int));
+ __e_acsl_valid_7 = __valid((void *)a,(size_t)sizeof(int));
__e_acsl_and_9 = __e_acsl_valid_7;
}
else __e_acsl_and_9 = 0;
if (__e_acsl_and_9) {
int __e_acsl_initialized_6;
int __e_acsl_and_10;
- __e_acsl_initialized_6 = __initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_6 = __initialized((void *)(& b),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_6) {
int __e_acsl_valid_8;
- __e_acsl_valid_8 = __valid((void *)b,sizeof(int));
+ __e_acsl_valid_8 = __valid((void *)b,(size_t)sizeof(int));
__e_acsl_and_10 = __e_acsl_valid_8;
}
else __e_acsl_and_10 = 0;
@@ -346,7 +359,7 @@ int main(void)
else __e_acsl_and_11 = 0;
if (__e_acsl_and_11) {
int __e_acsl_valid_9;
- __e_acsl_valid_9 = __valid((void *)X,sizeof(int));
+ __e_acsl_valid_9 = __valid((void *)X,(size_t)sizeof(int));
__e_acsl_and_12 = __e_acsl_valid_9;
}
else __e_acsl_and_12 = 0;
@@ -361,20 +374,22 @@ int main(void)
int __e_acsl_and_13;
int __e_acsl_and_15;
int __e_acsl_and_16;
- __e_acsl_initialized_7 = __initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_7 = __initialized((void *)(& a),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_7) {
int __e_acsl_valid_10;
- __e_acsl_valid_10 = __valid((void *)a,sizeof(int));
+ __e_acsl_valid_10 = __valid((void *)a,(size_t)sizeof(int));
__e_acsl_and_13 = __e_acsl_valid_10;
}
else __e_acsl_and_13 = 0;
if (__e_acsl_and_13) {
int __e_acsl_initialized_8;
int __e_acsl_and_14;
- __e_acsl_initialized_8 = __initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_8 = __initialized((void *)(& b),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_8) {
int __e_acsl_valid_11;
- __e_acsl_valid_11 = __valid((void *)b,sizeof(int));
+ __e_acsl_valid_11 = __valid((void *)b,(size_t)sizeof(int));
__e_acsl_and_14 = __e_acsl_valid_11;
}
else __e_acsl_and_14 = 0;
@@ -383,7 +398,7 @@ int main(void)
else __e_acsl_and_15 = 0;
if (__e_acsl_and_15) {
int __e_acsl_valid_12;
- __e_acsl_valid_12 = __valid((void *)X,sizeof(int));
+ __e_acsl_valid_12 = __valid((void *)X,(size_t)sizeof(int));
__e_acsl_and_16 = __e_acsl_valid_12;
}
else __e_acsl_and_16 = 0;
@@ -397,20 +412,22 @@ int main(void)
int __e_acsl_and_17;
int __e_acsl_and_19;
int __e_acsl_and_20;
- __e_acsl_initialized_9 = __initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_9 = __initialized((void *)(& a),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_9) {
int __e_acsl_valid_13;
- __e_acsl_valid_13 = __valid((void *)a,sizeof(int));
+ __e_acsl_valid_13 = __valid((void *)a,(size_t)sizeof(int));
__e_acsl_and_17 = __e_acsl_valid_13;
}
else __e_acsl_and_17 = 0;
if (__e_acsl_and_17) {
int __e_acsl_initialized_10;
int __e_acsl_and_18;
- __e_acsl_initialized_10 = __initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_10 = __initialized((void *)(& b),
+ (size_t)sizeof(int *));
if (__e_acsl_initialized_10) {
int __e_acsl_valid_14;
- __e_acsl_valid_14 = __valid((void *)b,sizeof(int));
+ __e_acsl_valid_14 = __valid((void *)b,(size_t)sizeof(int));
__e_acsl_and_18 = __e_acsl_valid_14;
}
else __e_acsl_and_18 = 0;
@@ -419,60 +436,151 @@ int main(void)
else __e_acsl_and_19 = 0;
if (__e_acsl_and_19) {
int __e_acsl_valid_15;
- __e_acsl_valid_15 = __valid((void *)X,sizeof(int));
+ __e_acsl_valid_15 = __valid((void *)X,(size_t)sizeof(int));
__e_acsl_and_20 = __e_acsl_valid_15;
}
else __e_acsl_and_20 = 0;
e_acsl_assert(__e_acsl_and_20,(char *)"Assertion",(char *)"main",
(char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",35);
}
- __e_acsl_free((void *)a);
- /*@ assert (¬\valid(a) ∧ \valid(b)) ∧ \valid(X); */
+ __full_init((void *)(& c));
+ c = & a;
+ __full_init((void *)(& d));
+ d = & c;
+ /*@ assert \valid(*c); */
{
int __e_acsl_initialized_11;
- int __e_acsl_and_21;
- int __e_acsl_and_23;
- int __e_acsl_and_24;
- __e_acsl_initialized_11 = __initialized((void *)(& a),sizeof(int *));
+ int __e_acsl_and_22;
+ __e_acsl_initialized_11 = __initialized((void *)c,(size_t)sizeof(int *));
if (__e_acsl_initialized_11) {
- int __e_acsl_valid_16;
- __e_acsl_valid_16 = __valid((void *)a,sizeof(int));
- __e_acsl_and_21 = __e_acsl_valid_16;
- }
- else __e_acsl_and_21 = 0;
- if (! __e_acsl_and_21) {
int __e_acsl_initialized_12;
- int __e_acsl_and_22;
- __e_acsl_initialized_12 = __initialized((void *)(& b),sizeof(int *));
+ int __e_acsl_and_21;
+ int __e_acsl_valid_16;
+ __e_acsl_initialized_12 = __initialized((void *)(& c),
+ (size_t)sizeof(int **));
if (__e_acsl_initialized_12) {
- int __e_acsl_valid_17;
- __e_acsl_valid_17 = __valid((void *)b,sizeof(int));
- __e_acsl_and_22 = __e_acsl_valid_17;
+ int __e_acsl_valid_read;
+ __e_acsl_valid_read = __valid_read((void *)c,(size_t)sizeof(int *));
+ __e_acsl_and_21 = __e_acsl_valid_read;
}
- else __e_acsl_and_22 = 0;
- __e_acsl_and_23 = __e_acsl_and_22;
+ else __e_acsl_and_21 = 0;
+ e_acsl_assert(__e_acsl_and_21,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(c)",0);
+ __e_acsl_valid_16 = __valid((void *)*c,(size_t)sizeof(int));
+ __e_acsl_and_22 = __e_acsl_valid_16;
}
- else __e_acsl_and_23 = 0;
- if (__e_acsl_and_23) {
+ else __e_acsl_and_22 = 0;
+ e_acsl_assert(__e_acsl_and_22,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(*c)",38);
+ }
+ /*@ assert \valid(*(*d)); */
+ {
+ int __e_acsl_valid_read_2;
+ int __e_acsl_initialized_13;
+ int __e_acsl_and_26;
+ __e_acsl_valid_read_2 = __valid_read((void *)d,(size_t)sizeof(int **));
+ e_acsl_assert(__e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(d)",0);
+ __e_acsl_initialized_13 = __initialized((void *)*d,(size_t)sizeof(int *));
+ if (__e_acsl_initialized_13) {
+ int __e_acsl_initialized_14;
+ int __e_acsl_and_24;
+ int __e_acsl_initialized_16;
+ int __e_acsl_and_25;
+ int __e_acsl_valid_17;
+ __e_acsl_initialized_14 = __initialized((void *)d,
+ (size_t)sizeof(int **));
+ if (__e_acsl_initialized_14) {
+ int __e_acsl_initialized_15;
+ int __e_acsl_and_23;
+ int __e_acsl_valid_read_4;
+ __e_acsl_initialized_15 = __initialized((void *)(& d),
+ (size_t)sizeof(int ***));
+ if (__e_acsl_initialized_15) {
+ int __e_acsl_valid_read_3;
+ __e_acsl_valid_read_3 = __valid_read((void *)d,
+ (size_t)sizeof(int **));
+ __e_acsl_and_23 = __e_acsl_valid_read_3;
+ }
+ else __e_acsl_and_23 = 0;
+ e_acsl_assert(__e_acsl_and_23,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(d)",0);
+ __e_acsl_valid_read_4 = __valid_read((void *)*d,
+ (size_t)sizeof(int *));
+ __e_acsl_and_24 = __e_acsl_valid_read_4;
+ }
+ else __e_acsl_and_24 = 0;
+ e_acsl_assert(__e_acsl_and_24,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(*d)",0);
+ __e_acsl_initialized_16 = __initialized((void *)(& d),
+ (size_t)sizeof(int ***));
+ if (__e_acsl_initialized_16) {
+ int __e_acsl_valid_read_5;
+ __e_acsl_valid_read_5 = __valid_read((void *)d,
+ (size_t)sizeof(int **));
+ __e_acsl_and_25 = __e_acsl_valid_read_5;
+ }
+ else __e_acsl_and_25 = 0;
+ e_acsl_assert(__e_acsl_and_25,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(d)",0);
+ __e_acsl_valid_17 = __valid((void *)*(*d),(size_t)sizeof(int));
+ __e_acsl_and_26 = __e_acsl_valid_17;
+ }
+ else __e_acsl_and_26 = 0;
+ e_acsl_assert(__e_acsl_and_26,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(*(*d))",39);
+ }
+ __e_acsl_free((void *)a);
+ /*@ assert (¬\valid(a) ∧ \valid(b)) ∧ \valid(X); */
+ {
+ int __e_acsl_initialized_17;
+ int __e_acsl_and_27;
+ int __e_acsl_and_29;
+ int __e_acsl_and_30;
+ __e_acsl_initialized_17 = __initialized((void *)(& a),
+ (size_t)sizeof(int *));
+ if (__e_acsl_initialized_17) {
int __e_acsl_valid_18;
- __e_acsl_valid_18 = __valid((void *)X,sizeof(int));
- __e_acsl_and_24 = __e_acsl_valid_18;
+ __e_acsl_valid_18 = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_and_27 = __e_acsl_valid_18;
+ }
+ else __e_acsl_and_27 = 0;
+ if (! __e_acsl_and_27) {
+ int __e_acsl_initialized_18;
+ int __e_acsl_and_28;
+ __e_acsl_initialized_18 = __initialized((void *)(& b),
+ (size_t)sizeof(int *));
+ if (__e_acsl_initialized_18) {
+ int __e_acsl_valid_19;
+ __e_acsl_valid_19 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_and_28 = __e_acsl_valid_19;
+ }
+ else __e_acsl_and_28 = 0;
+ __e_acsl_and_29 = __e_acsl_and_28;
+ }
+ else __e_acsl_and_29 = 0;
+ if (__e_acsl_and_29) {
+ int __e_acsl_valid_20;
+ __e_acsl_valid_20 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_and_30 = __e_acsl_valid_20;
}
- else __e_acsl_and_24 = 0;
- e_acsl_assert(__e_acsl_and_24,(char *)"Assertion",(char *)"main",
- (char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",37);
+ else __e_acsl_and_30 = 0;
+ e_acsl_assert(__e_acsl_and_30,(char *)"Assertion",(char *)"main",
+ (char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",41);
}
/*@ assert \valid(&Z); */
{
- int __e_acsl_valid_19;
- __e_acsl_valid_19 = __valid((void *)(& Z),sizeof(int));
- e_acsl_assert(__e_acsl_valid_19,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(&Z)",38);
+ int __e_acsl_valid_21;
+ __e_acsl_valid_21 = __valid((void *)(& Z),(size_t)sizeof(int));
+ e_acsl_assert(__e_acsl_valid_21,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&Z)",42);
}
__retres = 0;
__delete_block((void *)(& Z));
__delete_block((void *)(& X));
__delete_block((void *)(& n));
+ __delete_block((void *)(& d));
+ __delete_block((void *)(& c));
__delete_block((void *)(& b));
__delete_block((void *)(& a));
__clean();
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 7abc078baee936fadbc1bd7600e380dfa94bd7ef..be593c16aac5219b182612384f516fa5acd8247b 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
@@ -72,14 +72,17 @@ tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status val
tests/e-acsl-runtime/valid.c:16:[value] Function __e_acsl_f: postcondition got status valid.
tests/e-acsl-runtime/valid.c:33:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:38:[value] Assertion got status valid.
+[value] using specification for function __valid_read
+tests/e-acsl-runtime/valid.c:39:[value] Assertion got status valid.
FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
-tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:37:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
-tests/e-acsl-runtime/valid.c:37:[kernel] warning: completely indeterminate value in a.
-tests/e-acsl-runtime/valid.c:37:[value] all evaluations are invalid for function call argument
+tests/e-acsl-runtime/valid.c:41:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:41:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
+tests/e-acsl-runtime/valid.c:41:[kernel] warning: completely indeterminate value in a.
+tests/e-acsl-runtime/valid.c:41:[value] all evaluations are invalid for function call argument
(void *)a
-tests/e-acsl-runtime/valid.c:38:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:42:[value] Assertion got status valid.
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] using specification for function __clean
[value] done for function main
@@ -99,5 +102,7 @@ tests/e-acsl-runtime/valid.c:38:[value] Assertion got status valid.
X ‚àà {{ &n }}
a ‚àà ESCAPINGADDR
b ‚àà {{ &n }}
+ c ‚àà {{ &a }}
+ d ‚àà {{ &c }}
n ‚àà {0}
__retres ‚àà {0}
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 7abc078baee936fadbc1bd7600e380dfa94bd7ef..be593c16aac5219b182612384f516fa5acd8247b 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
@@ -72,14 +72,17 @@ tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status val
tests/e-acsl-runtime/valid.c:16:[value] Function __e_acsl_f: postcondition got status valid.
tests/e-acsl-runtime/valid.c:33:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:38:[value] Assertion got status valid.
+[value] using specification for function __valid_read
+tests/e-acsl-runtime/valid.c:39:[value] Assertion got status valid.
FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
-tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:37:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
-tests/e-acsl-runtime/valid.c:37:[kernel] warning: completely indeterminate value in a.
-tests/e-acsl-runtime/valid.c:37:[value] all evaluations are invalid for function call argument
+tests/e-acsl-runtime/valid.c:41:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:41:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
+tests/e-acsl-runtime/valid.c:41:[kernel] warning: completely indeterminate value in a.
+tests/e-acsl-runtime/valid.c:41:[value] all evaluations are invalid for function call argument
(void *)a
-tests/e-acsl-runtime/valid.c:38:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:42:[value] Assertion got status valid.
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] using specification for function __clean
[value] done for function main
@@ -99,5 +102,7 @@ tests/e-acsl-runtime/valid.c:38:[value] Assertion got status valid.
X ‚àà {{ &n }}
a ‚àà ESCAPINGADDR
b ‚àà {{ &n }}
+ c ‚àà {{ &a }}
+ d ‚àà {{ &c }}
n ‚àà {0}
__retres ‚àà {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
index aaea64d15c43eb3d81b7969f707958e08c83a51a..5753dd2f5d08df716bf9c56a9f171dbc5bd643c8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
@@ -1,8 +1,8 @@
/* run.config
COMMENT: \valid
STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
- EXECNOW: LOG gen_valid.c BIN gen_valid.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid.c > /dev/null && ./gcc_test.sh valid
- EXECNOW: LOG gen_valid2.c BIN gen_valid2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid2.c > /dev/null && ./gcc_test.sh valid2
+ EXECNOW: LOG gen_valid.c BIN gen_valid.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid.c > /dev/null && ./gcc_test.sh valid
+ EXECNOW: LOG gen_valid2.c BIN gen_valid2.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid2.c > /dev/null && ./gcc_test.sh valid2
*/
#include "stdlib.h"
@@ -23,7 +23,7 @@ int *f(int *x) {
}
int main(void) {
- int *a, *b, n = 0;
+ int *a, *b, **c, ***d, n = 0;
/*@ assert ! \valid(a) && ! \valid(b) && ! \valid(X); */
a = malloc(sizeof(int));
/*@ assert \valid(a) && ! \valid(b) && ! \valid(X); */
@@ -33,6 +33,10 @@ int main(void) {
/*@ assert \valid(a) && \valid(b) && \valid(X); */
X = b;
/*@ assert \valid(a) && \valid(b) && \valid(X); */
+ c = &a;
+ d = &c;
+ /*@ assert \valid(*c); */
+ /*@ assert \valid(**d); */
free(a);
/*@ assert ! \valid(a) && \valid(b) && \valid(X); */
/*@ assert \valid(&Z); */
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 2a71139785181fe4b665cd706537c5495ce16583..6f532d96780aa4bbe03ec7af0b120d29b0b7e499 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -622,7 +622,7 @@ and named_predicate_content_to_exp ?name kf env p =
(* optimisation when we know that the initialisation is ok *)
| TAddrOf (TResult _, TNoOffset) -> Cil.one ~loc, env
| TAddrOf (TVar { lv_origin = Some vi }, TNoOffset)
- when vi.vformal || vi.vglob || Misc.is_generated_varinfo vi ->
+ when vi.vformal || vi.vglob || Misc.is_generated_varinfo vi ->
Cil.one ~loc, env
| _ -> mmodel_call_with_size ~loc kf "initialized" Cil.intType env t)
| Pinitialized _ -> not_yet env "labeled \\initialized"
@@ -641,6 +641,7 @@ and named_predicate_to_exp ?name kf ?rte env p =
and translate_rte kf env e =
let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip Location.unknown) in
let l = get_rte kf stmt e in
+ let old_valid = !is_visiting_valid in
let old_kind = Env.annotation_kind env in
let env = Env.set_annotation_kind env Misc.RTE in
let env =
@@ -657,6 +658,7 @@ and translate_rte kf env e =
env
l
in
+ is_visiting_valid := old_valid;
Env.set_annotation_kind env old_kind
and translate_named_predicate kf env p =
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 1434b01c5d2d56f9814b3f3ea7927660edf2bbde..75cc2eb5676e4349955ef988f2cb83050b9a6d35 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -161,7 +161,10 @@ class e_acsl_visitor prj generate = object (self)
let new_vi = Cil.get_varinfo self#behavior old_vi in
let model blk =
if Pre_analysis.must_model_vi old_vi then
- Misc.mk_store_stmt new_vi :: blk
+ Misc.mk_store_stmt new_vi
+ (* :: Misc.mk_full_init_stmt new_vi
+ *) (*TODO TODO*)
+ :: blk
else
stmts
in
@@ -557,6 +560,11 @@ you must call function `%s' by yourself"
| Var vi, NoOffset -> vi.vglob || vi.vformal
| _ -> false
in
+(* Options.feedback "%a? %a (%b && %b)"
+ Printer.pp_lval assigned_lv
+ Printer.pp_lval checked_lv
+ (not (may_safely_ignore assigned_lv))
+ (Pre_analysis.must_model_lval ~kf ~stmt checked_lv);*)
if not (may_safely_ignore assigned_lv) &&
Pre_analysis.must_model_lval ~kf ~stmt checked_lv
then begin