From 9390f2d11408eca1b3ecbcaec484eca4a1bb9f23 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 25 Apr 2013 20:06:17 +0000
Subject: [PATCH] [E-ACSL] monitor only pointers and arrays
---
src/plugins/e-acsl/pre_analysis.ml | 6 ++++--
.../tests/e-acsl-runtime/oracle/gen_bts1390.c | 5 -----
.../tests/e-acsl-runtime/oracle/gen_bts13902.c | 5 -----
.../tests/e-acsl-runtime/oracle/gen_bts1399.c | 2 --
.../tests/e-acsl-runtime/oracle/gen_bts13992.c | 2 --
.../tests/e-acsl-runtime/oracle/gen_localvar.c | 2 --
.../tests/e-acsl-runtime/oracle/gen_localvar2.c | 2 --
.../tests/e-acsl-runtime/oracle/gen_ptr_init.c | 2 --
.../tests/e-acsl-runtime/oracle/gen_ptr_init2.c | 2 --
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c | 2 --
.../tests/e-acsl-runtime/oracle/gen_valid2.c | 2 --
.../tests/e-acsl-runtime/oracle/gen_valid_alias.c | 5 -----
.../tests/e-acsl-runtime/oracle/gen_valid_alias2.c | 5 -----
.../tests/e-acsl-runtime/oracle/gen_vector.c | 14 ++++++--------
.../tests/e-acsl-runtime/oracle/gen_vector2.c | 14 ++++++--------
.../e-acsl-runtime/oracle/valid_alias.1.res.oracle | 2 +-
.../e-acsl-runtime/oracle/valid_alias.res.oracle | 2 +-
.../e-acsl-runtime/oracle/vector.1.res.oracle | 7 ++++---
.../tests/e-acsl-runtime/oracle/vector.res.oracle | 7 ++++---
src/plugins/e-acsl/tests/e-acsl-runtime/vector.c | 3 ++-
20 files changed, 28 insertions(+), 63 deletions(-)
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 2519fb0064d..2272cd6fbf1 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -347,10 +347,10 @@ module rec Transfer
let state = Env.default_varinfos state in
let extend_to_expr state lhost e =
let add_vi state vi =
- if Varinfo.Set.mem vi state then
+ if is_ptr_or_array_exp e && Varinfo.Set.mem vi state then
match base_addr e with
| None -> state
- | Some vi -> Varinfo.Set.add vi state
+ | Some vi_e -> Varinfo.Set.add vi_e state
else
state
in
@@ -423,6 +423,8 @@ module rec Transfer
in
Dataflow.Done (Some state)
| _ ->
+ Options.warning "function pointers may introduce too limited \
+instrumentation.";
(* imprecise function call: keep each argument *)
Dataflow.Done
(Some
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
index b627514fc2b..dd75426e271 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
@@ -119,8 +119,6 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
void *__retres;
__store_block((void *)(& __retres),4U);
__store_block((void *)(& buf),4U);
- __store_block((void *)(& c),4U);
- __store_block((void *)(& n),4U);
{
int __e_acsl_forall_2;
unsigned int __e_acsl_k;
@@ -146,7 +144,6 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
e_acsl_end_loop3: /* internal */ ;
__e_acsl_at_4 = __e_acsl_forall_2;
}
- __store_block((void *)(& __e_acsl_at_3),4U);
__e_acsl_at_3 = c;
__store_block((void *)(& __e_acsl_at_2),4U);
__e_acsl_at_2 = buf;
@@ -220,8 +217,6 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
(char *)"\\old(\\forall integer k; 0 <= k && k < n ==> (int)*((char *)buf+k) != c) ==>\n\\result == (void *)0",
16);
__delete_block((void *)(& buf));
- __delete_block((void *)(& c));
- __delete_block((void *)(& n));
__delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
index 94bb2b9325d..a63bb3b6309 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
@@ -174,8 +174,6 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
void *__retres;
__store_block((void *)(& __retres),4U);
__store_block((void *)(& buf),4U);
- __store_block((void *)(& c),4U);
- __store_block((void *)(& n),4U);
{
int __e_acsl_forall_2;
mpz_t __e_acsl_k;
@@ -232,7 +230,6 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_at_4 = __e_acsl_forall_2;
__gmpz_clear(__e_acsl_k);
}
- __store_block((void *)(& __e_acsl_at_3),4U);
__e_acsl_at_3 = c;
__store_block((void *)(& __e_acsl_at_2),4U);
__e_acsl_at_2 = buf;
@@ -365,8 +362,6 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
(char *)"\\old(\\forall integer k; 0 <= k && k < n ==> (int)*((char *)buf+k) != c) ==>\n\\result == (void *)0",
16);
__delete_block((void *)(& buf));
- __delete_block((void *)(& c));
- __delete_block((void *)(& n));
__delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
index c272c755172..6b1383de20e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
@@ -135,9 +135,7 @@ void *__e_acsl_malloc(size_t size)
{
void *__retres;
__store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
__retres = __malloc(size);
- __delete_block((void *)(& size));
__delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
index 92292d85014..41010eccee5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
@@ -182,9 +182,7 @@ void *__e_acsl_malloc(size_t size)
{
void *__retres;
__store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
__retres = __malloc(size);
- __delete_block((void *)(& size));
__delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
index 9908ad514ec..d861adcd1f8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
@@ -107,9 +107,7 @@ void *__e_acsl_malloc(size_t size)
{
void *__retres;
__store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
__retres = __malloc(size);
- __delete_block((void *)(& size));
__delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
index 9908ad514ec..d861adcd1f8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
@@ -107,9 +107,7 @@ void *__e_acsl_malloc(size_t size)
{
void *__retres;
__store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
__retres = __malloc(size);
- __delete_block((void *)(& size));
__delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
index 8f6be093616..14648a95ec4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
@@ -100,9 +100,7 @@ void *__e_acsl_malloc(size_t size)
{
void *__retres;
__store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
__retres = __malloc(size);
- __delete_block((void *)(& size));
__delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
index 8f6be093616..14648a95ec4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
@@ -100,9 +100,7 @@ void *__e_acsl_malloc(size_t size)
{
void *__retres;
__store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
__retres = __malloc(size);
- __delete_block((void *)(& size));
__delete_block((void *)(& __retres));
return __retres;
}
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 81f667be94f..6e1b00a2313 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
@@ -124,9 +124,7 @@ void *__e_acsl_malloc(size_t size)
{
void *__retres;
__store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
__retres = __malloc(size);
- __delete_block((void *)(& size));
__delete_block((void *)(& __retres));
return __retres;
}
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 81f667be94f..6e1b00a2313 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
@@ -124,9 +124,7 @@ void *__e_acsl_malloc(size_t size)
{
void *__retres;
__store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
__retres = __malloc(size);
- __delete_block((void *)(& size));
__delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
index c2f4f1fbc07..39bfc7e30e1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
@@ -132,9 +132,7 @@ void *__e_acsl_malloc(size_t size)
{
void *__retres;
__store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
__retres = __malloc(size);
- __delete_block((void *)(& size));
__delete_block((void *)(& __retres));
return __retres;
}
@@ -180,10 +178,8 @@ int main(void)
int *a;
int *b;
int n;
- __store_block((void *)(& n),4U);
__store_block((void *)(& b),4U);
__store_block((void *)(& a),4U);
- __full_init((void *)(& n));
n = 0;
/*@ assert ¬\valid(a) ∧ ¬\valid(b); */
{
@@ -293,7 +289,6 @@ int main(void)
(char *)"!\\valid(a) && !\\valid(b)",19);
}
__retres = 0;
- __delete_block((void *)(& n));
__delete_block((void *)(& b));
__delete_block((void *)(& a));
__clean();
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
index 6365593033b..5c79ab7a567 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
@@ -148,9 +148,7 @@ void *__e_acsl_malloc(size_t size)
{
void *__retres;
__store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
__retres = __malloc(size);
- __delete_block((void *)(& size));
__delete_block((void *)(& __retres));
return __retres;
}
@@ -196,10 +194,8 @@ int main(void)
int *a;
int *b;
int n;
- __store_block((void *)(& n),4U);
__store_block((void *)(& b),4U);
__store_block((void *)(& a),4U);
- __full_init((void *)(& n));
n = 0;
/*@ assert ¬\valid(a) ∧ ¬\valid(b); */
{
@@ -307,7 +303,6 @@ int main(void)
(char *)"!\\valid(a) && !\\valid(b)",19);
}
__retres = 0;
- __delete_block((void *)(& n));
__delete_block((void *)(& b));
__delete_block((void *)(& a));
__clean();
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
index 2b9123b2a6a..7c4d9feda33 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
@@ -125,9 +125,7 @@ void *__e_acsl_malloc(size_t size)
{
void *__retres;
__store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
__retres = __malloc(size);
- __delete_block((void *)(& size));
__delete_block((void *)(& __retres));
return __retres;
}
@@ -170,7 +168,6 @@ int *new_inversed(int len, int *v)
int i;
int *p;
__store_block((void *)(& p),4U);
- __store_block((void *)(& v),4U);
__full_init((void *)(& p));
p = (int *)__e_acsl_malloc(sizeof(int) * (unsigned int)len);
i = 0;
@@ -179,7 +176,6 @@ int *new_inversed(int len, int *v)
*(p + i) = *(v + ((len - i) - 1));
i ++;
}
- __delete_block((void *)(& v));
__delete_block((void *)(& p));
return p;
}
@@ -187,23 +183,25 @@ int *new_inversed(int len, int *v)
int main(void)
{
int __retres;
+ int x;
int v1[3];
int *v2;
__store_block((void *)(& v2),4U);
__store_block((void *)(v1),12U);
+ x = 3;
__initialize((void *)(v1),sizeof(int));
v1[0] = 1;
__initialize((void *)(& v1[1]),sizeof(int));
v1[1] = 2;
__initialize((void *)(& v1[2]),sizeof(int));
- v1[2] = 3;
+ v1[2] = x;
LAST = v1[2];
/*@ assert \initialized(&v1[2]); */
{
int __e_acsl_initialized;
__e_acsl_initialized = __initialized((void *)(& v1[2]),sizeof(int));
e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(&v1[2])",25);
+ (char *)"\\initialized(&v1[2])",26);
}
__full_init((void *)(& v2));
v2 = new_inversed(3,v1);
@@ -213,11 +211,11 @@ int main(void)
int __e_acsl_initialized_2;
__e_acsl_initialized_2 = __initialized((void *)(v2 + 2),sizeof(int));
e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(v2+2)",28);
+ (char *)"\\initialized(v2+2)",29);
}
/*@ assert LAST ≡ 1; */
e_acsl_assert(LAST == 1,(char *)"Assertion",(char *)"main",
- (char *)"LAST == 1",29);
+ (char *)"LAST == 1",30);
__e_acsl_free((void *)v2);
__retres = 0;
__delete_block((void *)(& v2));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
index abb78f1e956..3756d1802cf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
@@ -145,9 +145,7 @@ void *__e_acsl_malloc(size_t size)
{
void *__retres;
__store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
__retres = __malloc(size);
- __delete_block((void *)(& size));
__delete_block((void *)(& __retres));
return __retres;
}
@@ -190,7 +188,6 @@ int *new_inversed(int len, int *v)
int i;
int *p;
__store_block((void *)(& p),4U);
- __store_block((void *)(& v),4U);
__full_init((void *)(& p));
p = (int *)__e_acsl_malloc(sizeof(int) * (unsigned int)len);
i = 0;
@@ -199,7 +196,6 @@ int *new_inversed(int len, int *v)
*(p + i) = *(v + ((len - i) - 1));
i ++;
}
- __delete_block((void *)(& v));
__delete_block((void *)(& p));
return p;
}
@@ -207,23 +203,25 @@ int *new_inversed(int len, int *v)
int main(void)
{
int __retres;
+ int x;
int v1[3];
int *v2;
__store_block((void *)(& v2),4U);
__store_block((void *)(v1),12U);
+ x = 3;
__initialize((void *)(v1),sizeof(int));
v1[0] = 1;
__initialize((void *)(& v1[1]),sizeof(int));
v1[1] = 2;
__initialize((void *)(& v1[2]),sizeof(int));
- v1[2] = 3;
+ v1[2] = x;
LAST = v1[2];
/*@ assert \initialized(&v1[2]); */
{
int __e_acsl_initialized;
__e_acsl_initialized = __initialized((void *)(& v1[2]),sizeof(int));
e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(&v1[2])",25);
+ (char *)"\\initialized(&v1[2])",26);
}
__full_init((void *)(& v2));
v2 = new_inversed(3,v1);
@@ -234,7 +232,7 @@ int main(void)
__e_acsl_initialized_2 = __initialized((void *)(v2 + (long)2),
sizeof(int));
e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(v2+2)",28);
+ (char *)"\\initialized(v2+2)",29);
}
/*@ assert LAST ≡ 1; */
{
@@ -246,7 +244,7 @@ int main(void)
__e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_LAST),
(__mpz_struct const *)(__e_acsl));
e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"LAST == 1",29);
+ (char *)"LAST == 1",30);
__gmpz_clear(__e_acsl_LAST);
__gmpz_clear(__e_acsl);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index fa36eac9c68..359ee4a6b87 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
@@ -27,7 +27,6 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\alloc
__fc_heap_status ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
-[value] using specification for function __full_init
tests/e-acsl-runtime/valid_alias.c:12:[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.
@@ -42,6 +41,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] all evaluations are invalid for fu
(void *)b
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __full_init
[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.)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index 8dda7f0f775..8badb6e0c19 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
@@ -27,7 +27,6 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\alloc
__fc_heap_status ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
-[value] using specification for function __full_init
tests/e-acsl-runtime/valid_alias.c:12:[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.
@@ -42,6 +41,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] all evaluations are invalid for fu
(void *)b
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __full_init
[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.)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
index 4cbe715e4e6..7d4344f8717 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
@@ -29,7 +29,7 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate'
LAST ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __initialize
-tests/e-acsl-runtime/vector.c:25:[value] Assertion got status valid.
+tests/e-acsl-runtime/vector.c:26:[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 valid.
@@ -40,9 +40,9 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
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/vector.c:16:[value] entering loop for the first time
-tests/e-acsl-runtime/vector.c:28:[value] Assertion got status unknown.
tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
-tests/e-acsl-runtime/vector.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
+tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown.
+tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
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.
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
@@ -62,6 +62,7 @@ FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior dealloca
[value] Values at end of function main:
__fc_heap_status ∈ [--..--]
LAST ∈ {1; 2; 3} or UNINITIALIZED
+ x ∈ {3}
v1[0] ∈ {1}
[1] ∈ {2}
[2] ∈ {3}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
index 1d5f127b3f4..3b69442f242 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
@@ -29,7 +29,7 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate'
LAST ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __initialize
-tests/e-acsl-runtime/vector.c:25:[value] Assertion got status valid.
+tests/e-acsl-runtime/vector.c:26:[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 valid.
@@ -40,9 +40,9 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
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/vector.c:16:[value] entering loop for the first time
-tests/e-acsl-runtime/vector.c:28:[value] Assertion got status unknown.
tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
-tests/e-acsl-runtime/vector.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
+tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown.
+tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
[value] using specification for function __gmpz_init_set_si
share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:63:[value] Function __gmpz_init_set_si: postcondition got status valid.
@@ -71,6 +71,7 @@ FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior dealloca
[value] Values at end of function main:
__fc_heap_status ∈ [--..--]
LAST ∈ {1; 2; 3} or UNINITIALIZED
+ x ∈ {3}
v1[0] ∈ {1}
[1] ∈ {2}
[2] ∈ {3}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
index a2870eb277c..d86ef57b989 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
@@ -19,7 +19,8 @@ int* new_inversed(int len, int *v) {
}
int main(void) {
- int v1[3]= { 1, 2, 3}, *v2;
+ int x = 3;
+ int v1[3]= { 1, 2, x }, *v2;
// @ assert \valid(&v1[2]);
LAST = v1[2];
//@ assert \initialized(v1+2);
--
GitLab