From fe218b787bedef0a708d8255b88289788016bf66 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 27 May 2013 09:10:21 +0000
Subject: [PATCH] [E-ACSL] fixed bug with series of addresses
---
src/plugins/e-acsl/pre_analysis.ml | 17 +++--
.../tests/e-acsl-runtime/oracle/gen_valid.c | 75 +++++++++++++++----
.../tests/e-acsl-runtime/oracle/gen_valid2.c | 75 +++++++++++++++----
.../e-acsl-runtime/oracle/valid.1.res.oracle | 63 +++++++++-------
.../e-acsl-runtime/oracle/valid.res.oracle | 63 +++++++++-------
.../e-acsl/tests/e-acsl-runtime/valid.c | 9 +++
6 files changed, 208 insertions(+), 94 deletions(-)
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 529771ac518..a9104e50699 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -386,9 +386,10 @@ module rec Transfer
the data before the branch (not considering the exception handlers) *)
let doInstr _stmt instr state =
let state = Env.default_varinfos state in
- let extend_to_expr state lhost e =
+ let extend_to_expr always state lhost e =
let add_vi state vi =
- if is_ptr_or_array_exp e && Varinfo.Hptset.mem vi state then
+ if is_ptr_or_array_exp e && (always || Varinfo.Hptset.mem vi state)
+ then
match base_addr e with
| None -> state
| Some vi_e ->
@@ -409,11 +410,11 @@ module rec Transfer
in
match instr with
| Set((lhost, _) as lv, e, _) ->
- (* if [e] contains an address from a base to be monitored, then also
- monitor the host *)
+ (* if [e] contains an address from a base, then also monitor the host *)
let rec extend_from_addr state e = match e.enode with
| AddrOf(lhost, _) ->
- extend_to_expr state lhost (Cil.new_exp ~loc:e.eloc (Lval lv))
+ extend_to_expr true state lhost (Cil.new_exp ~loc:e.eloc (Lval lv)),
+ true
| BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
if is_ptr_or_array_exp e1 then extend_from_addr state e1
else begin
@@ -421,10 +422,10 @@ module rec Transfer
extend_from_addr state e2
end
| CastE(_, e) | Info(e, _) -> extend_from_addr state e
- | _ -> state
+ | _ -> state, false
in
- let state = extend_from_addr state e in
- Dataflow.Done (Some (extend_to_expr state lhost e))
+ let state, always = extend_from_addr state e in
+ Dataflow.Done (Some (extend_to_expr always state lhost e))
| Call(result, f_exp, l, _) ->
(match f_exp.enode with
| Lval(Var vi, NoOffset) ->
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 7d71b584e2f..de02e1e1933 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
@@ -230,6 +230,52 @@ int *__e_acsl_f(int *x)
}
}
+void g(void)
+{
+ int m;
+ int *u;
+ int **p;
+ __store_block((void *)(& p),8U);
+ __store_block((void *)(& u),8U);
+ __store_block((void *)(& m),4U);
+ __full_init((void *)(& p));
+ p = & u;
+ __full_init((void *)(& u));
+ u = & m;
+ __full_init((void *)(& m));
+ m = 123;
+ /*@ assert \valid(*p); */
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and_2;
+ __e_acsl_initialized = __initialized((void *)p,(size_t)sizeof(int *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_initialized_2;
+ int __e_acsl_and;
+ int __e_acsl_valid;
+ __e_acsl_initialized_2 = __initialized((void *)(& p),
+ (size_t)sizeof(int **));
+ if (__e_acsl_initialized_2) {
+ int __e_acsl_valid_read;
+ __e_acsl_valid_read = __valid_read((void *)p,(size_t)sizeof(int *));
+ __e_acsl_and = __e_acsl_valid_read;
+ }
+ else __e_acsl_and = 0;
+ e_acsl_assert(__e_acsl_and,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(p)",30);
+ __e_acsl_valid = __valid((void *)*p,(size_t)sizeof(int));
+ __e_acsl_and_2 = __e_acsl_valid;
+ }
+ else __e_acsl_and_2 = 0;
+ e_acsl_assert(__e_acsl_and_2,(char *)"Assertion",(char *)"g",
+ (char *)"\\valid(*p)",30);
+ }
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& u));
+ __delete_block((void *)(& m));
+ return;
+}
+
void e_acsl_global_init(void)
{
__store_block((void *)(& Z),4U);
@@ -287,7 +333,7 @@ int main(void)
}
else __e_acsl_and_4 = 0;
e_acsl_assert(__e_acsl_and_4,(char *)"Assertion",(char *)"main",
- (char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",27);
+ (char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",35);
}
__full_init((void *)(& a));
a = (int *)__e_acsl_malloc((unsigned int)sizeof(int));
@@ -326,7 +372,7 @@ int main(void)
}
else __e_acsl_and_8 = 0;
e_acsl_assert(__e_acsl_and_8,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && !\\valid(b)) && !\\valid(X)",29);
+ (char *)"(\\valid(a) && !\\valid(b)) && !\\valid(X)",37);
}
X = a;
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ \valid(X); */
@@ -364,7 +410,7 @@ int main(void)
}
else __e_acsl_and_12 = 0;
e_acsl_assert(__e_acsl_and_12,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && !\\valid(b)) && \\valid(X)",31);
+ (char *)"(\\valid(a) && !\\valid(b)) && \\valid(X)",39);
}
__full_init((void *)(& b));
b = __e_acsl_f(& n);
@@ -403,7 +449,7 @@ int main(void)
}
else __e_acsl_and_16 = 0;
e_acsl_assert(__e_acsl_and_16,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",33);
+ (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",41);
}
X = b;
/*@ assert (\valid(a) ∧ \valid(b)) ∧ \valid(X); */
@@ -441,7 +487,7 @@ int main(void)
}
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);
+ (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",43);
}
__full_init((void *)(& c));
c = & a;
@@ -465,13 +511,13 @@ int main(void)
}
else __e_acsl_and_21 = 0;
e_acsl_assert(__e_acsl_and_21,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(c)",38);
+ (char *)"mem_access: \\valid_read(c)",46);
__e_acsl_valid_16 = __valid((void *)*c,(size_t)sizeof(int));
__e_acsl_and_22 = __e_acsl_valid_16;
}
else __e_acsl_and_22 = 0;
e_acsl_assert(__e_acsl_and_22,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(*c)",38);
+ (char *)"\\valid(*c)",46);
}
/*@ assert \valid(*(*d)); */
{
@@ -480,7 +526,7 @@ int main(void)
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)",39);
+ (char *)"mem_access: \\valid_read(d)",47);
__e_acsl_initialized_13 = __initialized((void *)*d,(size_t)sizeof(int *));
if (__e_acsl_initialized_13) {
int __e_acsl_initialized_14;
@@ -504,14 +550,14 @@ int main(void)
}
else __e_acsl_and_23 = 0;
e_acsl_assert(__e_acsl_and_23,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(d)",39);
+ (char *)"mem_access: \\valid_read(d)",47);
__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)",39);
+ (char *)"mem_access: \\valid_read(*d)",47);
__e_acsl_initialized_16 = __initialized((void *)(& d),
(size_t)sizeof(int ***));
if (__e_acsl_initialized_16) {
@@ -522,13 +568,13 @@ int main(void)
}
else __e_acsl_and_25 = 0;
e_acsl_assert(__e_acsl_and_25,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(d)",39);
+ (char *)"mem_access: \\valid_read(d)",47);
__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);
+ (char *)"\\valid(*(*d))",47);
}
__e_acsl_free((void *)a);
/*@ assert (¬\valid(a) ∧ \valid(b)) ∧ \valid(X); */
@@ -566,15 +612,16 @@ int main(void)
}
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);
+ (char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",49);
}
/*@ assert \valid(&Z); */
{
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);
+ (char *)"\\valid(&Z)",50);
}
+ g();
__retres = 0;
__delete_block((void *)(& Z));
__delete_block((void *)(& X));
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 7d71b584e2f..de02e1e1933 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
@@ -230,6 +230,52 @@ int *__e_acsl_f(int *x)
}
}
+void g(void)
+{
+ int m;
+ int *u;
+ int **p;
+ __store_block((void *)(& p),8U);
+ __store_block((void *)(& u),8U);
+ __store_block((void *)(& m),4U);
+ __full_init((void *)(& p));
+ p = & u;
+ __full_init((void *)(& u));
+ u = & m;
+ __full_init((void *)(& m));
+ m = 123;
+ /*@ assert \valid(*p); */
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and_2;
+ __e_acsl_initialized = __initialized((void *)p,(size_t)sizeof(int *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_initialized_2;
+ int __e_acsl_and;
+ int __e_acsl_valid;
+ __e_acsl_initialized_2 = __initialized((void *)(& p),
+ (size_t)sizeof(int **));
+ if (__e_acsl_initialized_2) {
+ int __e_acsl_valid_read;
+ __e_acsl_valid_read = __valid_read((void *)p,(size_t)sizeof(int *));
+ __e_acsl_and = __e_acsl_valid_read;
+ }
+ else __e_acsl_and = 0;
+ e_acsl_assert(__e_acsl_and,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(p)",30);
+ __e_acsl_valid = __valid((void *)*p,(size_t)sizeof(int));
+ __e_acsl_and_2 = __e_acsl_valid;
+ }
+ else __e_acsl_and_2 = 0;
+ e_acsl_assert(__e_acsl_and_2,(char *)"Assertion",(char *)"g",
+ (char *)"\\valid(*p)",30);
+ }
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& u));
+ __delete_block((void *)(& m));
+ return;
+}
+
void e_acsl_global_init(void)
{
__store_block((void *)(& Z),4U);
@@ -287,7 +333,7 @@ int main(void)
}
else __e_acsl_and_4 = 0;
e_acsl_assert(__e_acsl_and_4,(char *)"Assertion",(char *)"main",
- (char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",27);
+ (char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",35);
}
__full_init((void *)(& a));
a = (int *)__e_acsl_malloc((unsigned int)sizeof(int));
@@ -326,7 +372,7 @@ int main(void)
}
else __e_acsl_and_8 = 0;
e_acsl_assert(__e_acsl_and_8,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && !\\valid(b)) && !\\valid(X)",29);
+ (char *)"(\\valid(a) && !\\valid(b)) && !\\valid(X)",37);
}
X = a;
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ \valid(X); */
@@ -364,7 +410,7 @@ int main(void)
}
else __e_acsl_and_12 = 0;
e_acsl_assert(__e_acsl_and_12,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && !\\valid(b)) && \\valid(X)",31);
+ (char *)"(\\valid(a) && !\\valid(b)) && \\valid(X)",39);
}
__full_init((void *)(& b));
b = __e_acsl_f(& n);
@@ -403,7 +449,7 @@ int main(void)
}
else __e_acsl_and_16 = 0;
e_acsl_assert(__e_acsl_and_16,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",33);
+ (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",41);
}
X = b;
/*@ assert (\valid(a) ∧ \valid(b)) ∧ \valid(X); */
@@ -441,7 +487,7 @@ int main(void)
}
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);
+ (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",43);
}
__full_init((void *)(& c));
c = & a;
@@ -465,13 +511,13 @@ int main(void)
}
else __e_acsl_and_21 = 0;
e_acsl_assert(__e_acsl_and_21,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(c)",38);
+ (char *)"mem_access: \\valid_read(c)",46);
__e_acsl_valid_16 = __valid((void *)*c,(size_t)sizeof(int));
__e_acsl_and_22 = __e_acsl_valid_16;
}
else __e_acsl_and_22 = 0;
e_acsl_assert(__e_acsl_and_22,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(*c)",38);
+ (char *)"\\valid(*c)",46);
}
/*@ assert \valid(*(*d)); */
{
@@ -480,7 +526,7 @@ int main(void)
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)",39);
+ (char *)"mem_access: \\valid_read(d)",47);
__e_acsl_initialized_13 = __initialized((void *)*d,(size_t)sizeof(int *));
if (__e_acsl_initialized_13) {
int __e_acsl_initialized_14;
@@ -504,14 +550,14 @@ int main(void)
}
else __e_acsl_and_23 = 0;
e_acsl_assert(__e_acsl_and_23,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(d)",39);
+ (char *)"mem_access: \\valid_read(d)",47);
__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)",39);
+ (char *)"mem_access: \\valid_read(*d)",47);
__e_acsl_initialized_16 = __initialized((void *)(& d),
(size_t)sizeof(int ***));
if (__e_acsl_initialized_16) {
@@ -522,13 +568,13 @@ int main(void)
}
else __e_acsl_and_25 = 0;
e_acsl_assert(__e_acsl_and_25,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(d)",39);
+ (char *)"mem_access: \\valid_read(d)",47);
__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);
+ (char *)"\\valid(*(*d))",47);
}
__e_acsl_free((void *)a);
/*@ assert (¬\valid(a) ∧ \valid(b)) ∧ \valid(X); */
@@ -566,15 +612,16 @@ int main(void)
}
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);
+ (char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",49);
}
/*@ assert \valid(&Z); */
{
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);
+ (char *)"\\valid(&Z)",50);
}
+ g();
__retres = 0;
__delete_block((void *)(& Z));
__delete_block((void *)(& X));
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 9d8a811e00e..c2ee6c6a921 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
@@ -9,14 +9,14 @@
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
+tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
@@ -30,17 +30,17 @@ tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `\allocate' i
Z ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/valid.c:27:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
[value] using specification for function __initialized
share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
-tests/e-acsl-runtime/valid.c:27:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
-tests/e-acsl-runtime/valid.c:27:[kernel] warning: completely indeterminate value in a.
-tests/e-acsl-runtime/valid.c:27:[value] all evaluations are invalid for function call argument
+tests/e-acsl-runtime/valid.c:35:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
+tests/e-acsl-runtime/valid.c:35:[kernel] warning: completely indeterminate value in a.
+tests/e-acsl-runtime/valid.c:35:[value] all evaluations are invalid for function call argument
(void *)a
-tests/e-acsl-runtime/valid.c:27:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
-tests/e-acsl-runtime/valid.c:27:[kernel] warning: completely indeterminate value in b.
-tests/e-acsl-runtime/valid.c:27:[value] all evaluations are invalid for function call argument
+tests/e-acsl-runtime/valid.c:35:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
+tests/e-acsl-runtime/valid.c:35:[kernel] warning: completely indeterminate value in b.
+tests/e-acsl-runtime/valid.c:35:[value] all evaluations are invalid for function call argument
(void *)b
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
@@ -48,16 +48,16 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/valid.c:29:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid.
share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
-tests/e-acsl-runtime/valid.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
-tests/e-acsl-runtime/valid.c:29:[kernel] warning: completely indeterminate value in b.
-tests/e-acsl-runtime/valid.c:29:[value] all evaluations are invalid for function call argument
+tests/e-acsl-runtime/valid.c:37:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
+tests/e-acsl-runtime/valid.c:37:[kernel] warning: completely indeterminate value in b.
+tests/e-acsl-runtime/valid.c:37:[value] all evaluations are invalid for function call argument
(void *)b
-tests/e-acsl-runtime/valid.c:31:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:31:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
-tests/e-acsl-runtime/valid.c:31:[kernel] warning: completely indeterminate value in b.
-tests/e-acsl-runtime/valid.c:31:[value] all evaluations are invalid for function call argument
+tests/e-acsl-runtime/valid.c:39:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:39:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
+tests/e-acsl-runtime/valid.c:39:[kernel] warning: completely indeterminate value in b.
+tests/e-acsl-runtime/valid.c:39:[value] all evaluations are invalid for function call argument
(void *)b
tests/e-acsl-runtime/valid.c:15:[value] Function __e_acsl_f: precondition got status valid.
tests/e-acsl-runtime/valid.c:15:[value] Function f: precondition got status valid.
@@ -70,19 +70,20 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
tests/e-acsl-runtime/valid.c:21:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status valid.
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.
+tests/e-acsl-runtime/valid.c:41:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:43:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:46:[value] Assertion got status valid.
[value] using specification for function __valid_read
-tests/e-acsl-runtime/valid.c:39:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:47:[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: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
+tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
+tests/e-acsl-runtime/valid.c:49:[kernel] warning: completely indeterminate value in a.
+tests/e-acsl-runtime/valid.c:49:[value] all evaluations are invalid for function call argument
(void *)a
-tests/e-acsl-runtime/valid.c:42:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:50:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:30:[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
@@ -98,6 +99,10 @@ tests/e-acsl-runtime/valid.c:42:[value] Assertion got status valid.
y ∈ {{ &n }}
[value] Values at end of function __e_acsl_f:
__retres ∈ {{ &n }}
+[value] Values at end of function g:
+ m ∈ {123}
+ u ∈ {{ &m }}
+ p ∈ {{ &u }}
[value] Values at end of function main:
__fc_heap_status ∈ [--..--]
X ∈ {{ &n }}
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 9d8a811e00e..c2ee6c6a921 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
@@ -9,14 +9,14 @@
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
+tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
@@ -30,17 +30,17 @@ tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `\allocate' i
Z ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/valid.c:27:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
[value] using specification for function __initialized
share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
-tests/e-acsl-runtime/valid.c:27:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
-tests/e-acsl-runtime/valid.c:27:[kernel] warning: completely indeterminate value in a.
-tests/e-acsl-runtime/valid.c:27:[value] all evaluations are invalid for function call argument
+tests/e-acsl-runtime/valid.c:35:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
+tests/e-acsl-runtime/valid.c:35:[kernel] warning: completely indeterminate value in a.
+tests/e-acsl-runtime/valid.c:35:[value] all evaluations are invalid for function call argument
(void *)a
-tests/e-acsl-runtime/valid.c:27:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
-tests/e-acsl-runtime/valid.c:27:[kernel] warning: completely indeterminate value in b.
-tests/e-acsl-runtime/valid.c:27:[value] all evaluations are invalid for function call argument
+tests/e-acsl-runtime/valid.c:35:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
+tests/e-acsl-runtime/valid.c:35:[kernel] warning: completely indeterminate value in b.
+tests/e-acsl-runtime/valid.c:35:[value] all evaluations are invalid for function call argument
(void *)b
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
@@ -48,16 +48,16 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/valid.c:29:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid.
share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
-tests/e-acsl-runtime/valid.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
-tests/e-acsl-runtime/valid.c:29:[kernel] warning: completely indeterminate value in b.
-tests/e-acsl-runtime/valid.c:29:[value] all evaluations are invalid for function call argument
+tests/e-acsl-runtime/valid.c:37:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
+tests/e-acsl-runtime/valid.c:37:[kernel] warning: completely indeterminate value in b.
+tests/e-acsl-runtime/valid.c:37:[value] all evaluations are invalid for function call argument
(void *)b
-tests/e-acsl-runtime/valid.c:31:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:31:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
-tests/e-acsl-runtime/valid.c:31:[kernel] warning: completely indeterminate value in b.
-tests/e-acsl-runtime/valid.c:31:[value] all evaluations are invalid for function call argument
+tests/e-acsl-runtime/valid.c:39:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:39:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
+tests/e-acsl-runtime/valid.c:39:[kernel] warning: completely indeterminate value in b.
+tests/e-acsl-runtime/valid.c:39:[value] all evaluations are invalid for function call argument
(void *)b
tests/e-acsl-runtime/valid.c:15:[value] Function __e_acsl_f: precondition got status valid.
tests/e-acsl-runtime/valid.c:15:[value] Function f: precondition got status valid.
@@ -70,19 +70,20 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
tests/e-acsl-runtime/valid.c:21:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status valid.
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.
+tests/e-acsl-runtime/valid.c:41:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:43:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:46:[value] Assertion got status valid.
[value] using specification for function __valid_read
-tests/e-acsl-runtime/valid.c:39:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:47:[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: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
+tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
+tests/e-acsl-runtime/valid.c:49:[kernel] warning: completely indeterminate value in a.
+tests/e-acsl-runtime/valid.c:49:[value] all evaluations are invalid for function call argument
(void *)a
-tests/e-acsl-runtime/valid.c:42:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:50:[value] Assertion got status valid.
+tests/e-acsl-runtime/valid.c:30:[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
@@ -98,6 +99,10 @@ tests/e-acsl-runtime/valid.c:42:[value] Assertion got status valid.
y ∈ {{ &n }}
[value] Values at end of function __e_acsl_f:
__retres ∈ {{ &n }}
+[value] Values at end of function g:
+ m ∈ {123}
+ u ∈ {{ &m }}
+ p ∈ {{ &u }}
[value] Values at end of function main:
__fc_heap_status ∈ [--..--]
X ∈ {{ &n }}
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 5753dd2f5d0..aabd0f4977a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
@@ -22,6 +22,14 @@ int *f(int *x) {
return y;
}
+void g(void) {
+ int m, *u, **p;
+ p=&u;
+ u=&m;
+ m=123;
+ //@ assert \valid(*p);
+}
+
int main(void) {
int *a, *b, **c, ***d, n = 0;
/*@ assert ! \valid(a) && ! \valid(b) && ! \valid(X); */
@@ -40,5 +48,6 @@ int main(void) {
free(a);
/*@ assert ! \valid(a) && \valid(b) && \valid(X); */
/*@ assert \valid(&Z); */
+ g();
return 0;
}
--
GitLab