diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index d162a6aa8af1d3950d49a402bad992c1dd71b1b4..a6aaa2ac124cf324726b9b0de001107670a74dd3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
@@ -15,17 +16,6 @@ char *__gen_e_acsl_literal_string_2;
*/
void *__gen_e_acsl_memchr(void const *buf, int c, size_t n);
-/*@ behavior exists:
- assumes ∃ ℤ i; 0 ≤ i < (int)n ∧ (int)*((char *)buf + i) ≡ c;
- ensures
- ∀ int j;
- 0 ≤ j < (int)\offset((char *)\result) ⇒
- (int)*((char *)\old(buf) + j) ≢ \old(c);
-
- behavior not_exists:
- assumes ∀ ℤ k; 0 ≤ k < (int)n ⇒ (int)*((char *)buf + k) ≢ c;
- ensures \result ≡ (void *)0;
- */
void *memchr(void const *buf, int c, size_t n)
{
void *__retres;
@@ -37,7 +27,7 @@ void *memchr(void const *buf, int c, size_t n)
__e_acsl_full_init((void *)(& s));
i = 0;
while ((size_t)i < n) {
- /*@ assert Value: mem_access: \valid_read(s); */
+ /*@ assert Eva: mem_access: \valid_read(s); */
if ((int)*s == c) {
__e_acsl_full_init((void *)(& __retres));
__retres = (void *)s;
@@ -50,10 +40,12 @@ void *memchr(void const *buf, int c, size_t n)
__e_acsl_full_init((void *)(& __retres));
__retres = (void *)0;
return_label:
+ {
__e_acsl_delete_block((void *)(& buf));
__e_acsl_delete_block((void *)(& s));
__e_acsl_delete_block((void *)(& __retres));
return __retres;
+ }
}
/*@ behavior exists:
@@ -75,14 +67,14 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_at;
void *__retres;
__e_acsl_store_block((void *)(& __retres),(size_t)8);
- __e_acsl_store_block((void *)(& buf),(size_t)8);
{
int __gen_e_acsl_forall_2;
unsigned int __gen_e_acsl_k;
__gen_e_acsl_forall_2 = 1;
__gen_e_acsl_k = 0U;
while (1) {
- if (__gen_e_acsl_k < (int)((unsigned int)n)) ; else break;
+ if (__gen_e_acsl_k < (unsigned int)((int)((unsigned int)n))) ;
+ else break;
{
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_k),
@@ -92,7 +84,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"memchr",
(char *)"mem_access: \\valid_read((char *)buf + __gen_e_acsl_k)",
- 11);
+ 12);
if ((int)*((char *)buf + __gen_e_acsl_k) != c) ;
else {
__gen_e_acsl_forall_2 = 0;
@@ -112,7 +104,8 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__gen_e_acsl_exists = 0;
__gen_e_acsl_i = 0U;
while (1) {
- if (__gen_e_acsl_i < (int)((unsigned int)n)) ; else break;
+ if (__gen_e_acsl_i < (unsigned int)((int)((unsigned int)n))) ;
+ else break;
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_i),
@@ -122,7 +115,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",
(char *)"memchr",
(char *)"mem_access: \\valid_read((char *)buf + __gen_e_acsl_i)",
- 8);
+ 9);
if (! ((int)*((char *)buf + __gen_e_acsl_i) == c)) ;
else {
__gen_e_acsl_exists = 1;
@@ -134,6 +127,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
e_acsl_end_loop1: ;
__gen_e_acsl_at = __gen_e_acsl_exists;
}
+ __e_acsl_store_block((void *)(& buf),(size_t)8);
__retres = memchr(buf,c,n);
{
int __gen_e_acsl_implies;
@@ -146,9 +140,9 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__gen_e_acsl_j = 0;
while (1) {
{
- int __gen_e_acsl_offset;
+ unsigned long __gen_e_acsl_offset;
__gen_e_acsl_offset = __e_acsl_offset(__retres);
- if (__gen_e_acsl_j < (int)((unsigned int)__gen_e_acsl_offset))
+ if (__gen_e_acsl_j < (unsigned int)((int)((unsigned int)__gen_e_acsl_offset)))
;
else break;
}
@@ -161,7 +155,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"memchr",
(char *)"mem_access: \\valid_read((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j)",
- 9);
+ 10);
if ((int)*((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j) != __gen_e_acsl_at_3)
;
else {
@@ -177,13 +171,13 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_assert(__gen_e_acsl_implies,(char *)"Postcondition",
(char *)"memchr",
(char *)"\\old(\\exists integer i; 0 <= i < (int)n && (int)*((char *)buf + i) == c) ==>\n(\\forall int j;\n 0 <= j < (int)\\offset((char *)\\result) ==>\n (int)*((char *)\\old(buf) + j) != \\old(c))",
- 9);
+ 10);
if (! __gen_e_acsl_at_4) __gen_e_acsl_implies_2 = 1;
else __gen_e_acsl_implies_2 = __retres == (void *)0;
__e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Postcondition",
(char *)"memchr",
(char *)"\\old(\\forall integer k; 0 <= k < (int)n ==> (int)*((char *)buf + k) != c) ==>\n\\result == (void *)0",
- 12);
+ 13);
__e_acsl_delete_block((void *)(& buf));
__e_acsl_delete_block((void *)(& __retres));
return __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
index b8e45500b0367862bcf1497c46db6e9c5ef19d3e..a8006861e6c56233ae4e40b9ceb6d3d62bbb4183 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
@@ -14,6 +14,8 @@ int fact(int n)
}
tmp = __gen_e_acsl_fact(n - 1);
;
+ /*@ assert Eva: signed_overflow: -2147483648 ≤ n * tmp; */
+ /*@ assert Eva: signed_overflow: n * tmp ≤ 2147483647; */
__retres = n * tmp;
return_label: return __retres;
}
@@ -25,7 +27,7 @@ int main(void)
int x = __gen_e_acsl_fact(5);
/*@ assert x ≡ 120; */
__e_acsl_assert(x == 120,(char *)"Assertion",(char *)"main",
- (char *)"x == 120",13);
+ (char *)"x == 120",14);
__retres = 0;
return __retres;
}
@@ -35,7 +37,7 @@ int __gen_e_acsl_fact(int n)
{
int __retres;
__e_acsl_assert(n > 0,(char *)"Precondition",(char *)"fact",
- (char *)"n > 0",5);
+ (char *)"n > 0",6);
__retres = fact(n);
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
index f4b14fd603b479d80dbb90585b1d1ee98c79546a..071c1a1276c9fe851a6b108888e5e75a49628956 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
@@ -1,4 +1,6 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
struct spongeStateStruct {
unsigned char __attribute__((__aligned__(32))) state[1600 / 8] ;
unsigned char __attribute__((__aligned__(32))) dataQueue[1536 / 8] ;
@@ -8,29 +10,30 @@ typedef struct spongeStateStruct spongeState;
int main(void)
{
int __retres;
- spongeState *state;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& state),8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ spongeState *state = malloc(sizeof(spongeState));
+ __e_acsl_store_block((void *)(& state),(size_t)8);
__e_acsl_full_init((void *)(& state));
- state = (spongeState *)malloc(sizeof(spongeState));
__e_acsl_initialize((void *)(& state->bitsInQueue),sizeof(unsigned int));
state->bitsInQueue = (unsigned int)16;
- /*@ assert ¬\initialized(&state->dataQueue[state->bitsInQueue/8]); */
+ /*@ assert ¬\initialized(&state->dataQueue[state->bitsInQueue / 8]); */
{
int __gen_e_acsl_valid_read;
int __gen_e_acsl_initialized;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& state->bitsInQueue),
- sizeof(unsigned int));
+ sizeof(unsigned int),
+ (void *)(& state->bitsInQueue),
+ (void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(&state->bitsInQueue)",
22);
__gen_e_acsl_initialized = __e_acsl_initialized((void *)(& state->dataQueue[
- state->bitsInQueue / 8UL]),
+ state->bitsInQueue / 8U]),
sizeof(unsigned char __attribute__((
__aligned__(32)))));
__e_acsl_assert(! __gen_e_acsl_initialized,(char *)"Assertion",
(char *)"main",
- (char *)"!\\initialized(&state->dataQueue[state->bitsInQueue/8])",
+ (char *)"!\\initialized(&state->dataQueue[state->bitsInQueue / 8])",
22);
}
free((void *)state);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_array.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_array.c
index a3e45b4666eae33e8c90343149e96681333c9ca2..e5f0d771cd64e8662ae052d763d753d3bbc244e6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_array.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_array.c
@@ -1,30 +1,31 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
int T1[3];
int T2[4];
int main(void)
{
int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
{
- int i;
- i = 0;
+ int i = 0;
while (i < 3) {
T1[i] = i;
i ++;
}
}
{
- int i_0;
- i_0 = 0;
+ int i_0 = 0;
while (i_0 < 4) {
T2[i_0] = 2 * i_0;
i_0 ++;
}
}
/*@ assert T1[0] ≡ T2[0]; */
- __e_acsl_assert(T1[0UL] == T2[0UL],(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(T1[0] == T2[0],(char *)"Assertion",(char *)"main",
(char *)"T1[0] == T2[0]",13);
/*@ assert T1[1] ≢ T2[1]; */
- __e_acsl_assert(T1[1UL] != T2[1UL],(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(T1[1] != T2[1],(char *)"Assertion",(char *)"main",
(char *)"T1[1] != T2[1]",14);
__retres = 0;
return __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_array2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_array2.c
index 8b57d232ff6f7e266949eb4ff2c34cf98f97c0db..6f61fb210e9cf50361b4e61d509f2f193f589969 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_array2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_array2.c
@@ -1,20 +1,21 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
int T1[3];
int T2[4];
int main(void)
{
int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
{
- int i;
- i = 0;
+ int i = 0;
while (i < 3) {
T1[i] = i;
i ++;
}
}
{
- int i_0;
- i_0 = 0;
+ int i_0 = 0;
while (i_0 < 4) {
T2[i_0] = 2 * i_0;
i_0 ++;
@@ -22,13 +23,13 @@ int main(void)
}
/*@ assert T1[0] ≡ T2[0]; */
{
- mpz_t __gen_e_acsl_;
- mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl__2;
int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_,(long)T1[0UL]);
- __gmpz_init_set_si(__gen_e_acsl__2,(long)T2[0UL]);
- __gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
- (__mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init_set_si(__gen_e_acsl_,(long)T1[0]);
+ __gmpz_init_set_si(__gen_e_acsl__2,(long)T2[0]);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
(char *)"T1[0] == T2[0]",13);
__gmpz_clear(__gen_e_acsl_);
@@ -36,13 +37,13 @@ int main(void)
}
/*@ assert T1[1] ≢ T2[1]; */
{
- mpz_t __gen_e_acsl__3;
- mpz_t __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl__4;
int __gen_e_acsl_ne;
- __gmpz_init_set_si(__gen_e_acsl__3,(long)T1[1UL]);
- __gmpz_init_set_si(__gen_e_acsl__4,(long)T2[1UL]);
- __gen_e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__3),
- (__mpz_struct const *)(__gen_e_acsl__4));
+ __gmpz_init_set_si(__gen_e_acsl__3,(long)T1[1]);
+ __gmpz_init_set_si(__gen_e_acsl__4,(long)T2[1]);
+ __gen_e_acsl_ne = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
(char *)"T1[1] != T2[1]",14);
__gmpz_clear(__gen_e_acsl__3);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_cast.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_cast.c
index f3859df710c5ee042defc15cf8f8d46d6767486e..2518d42c41aaf084e4a2bc70af463fd0d9911d9f 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_cast.c
@@ -1,11 +1,12 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
int main(void)
{
int __retres;
- long x;
- int y;
- x = (long)0;
- y = 0;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ long x = (long)0;
+ int y = 0;
/*@ assert (int)x ≡ y; */
__e_acsl_assert((int)x == y,(char *)"Assertion",(char *)"main",
(char *)"(int)x == y",10);
@@ -26,6 +27,10 @@ int main(void)
(char *)"main",
(char *)"(unsigned int)y != (unsigned int)0xfffffffffffffff",
18);
+ int t[2] = {0, 1};
+ /*@ assert (float)x ≡ t[(int)0.1]; */
+ __e_acsl_assert((float)x == (float)t[0],(char *)"Assertion",(char *)"main",
+ (char *)"(float)x == t[(int)0.1]",23);
__retres = 0;
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_cast2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_cast2.c
index f29b5dd326373504c968abef22018576826eaf99..b511e029f6290b2ac2e392a2efe3059d650497c3 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_cast2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_cast2.c
@@ -1,24 +1,25 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
int main(void)
{
int __retres;
- long x;
- int y;
- x = (long)0;
- y = 0;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ long x = (long)0;
+ int y = 0;
/*@ assert (int)x ≡ y; */
{
- mpz_t __gen_e_acsl_x;
- unsigned long __gen_e_acsl_cast;
- mpz_t __gen_e_acsl_;
- mpz_t __gen_e_acsl_y;
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ long __gen_e_acsl_cast;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_y;
int __gen_e_acsl_eq;
__gmpz_init_set_si(__gen_e_acsl_x,x);
- __gen_e_acsl_cast = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_x));
- __gmpz_init_set_ui(__gen_e_acsl_,__gen_e_acsl_cast);
+ __gen_e_acsl_cast = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_x));
+ __gmpz_init_set_si(__gen_e_acsl_,__gen_e_acsl_cast);
__gmpz_init_set_si(__gen_e_acsl_y,(long)y);
- __gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
- (__mpz_struct const *)(__gen_e_acsl_y));
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
(char *)"(int)x == y",10);
__gmpz_clear(__gen_e_acsl_x);
@@ -27,17 +28,17 @@ int main(void)
}
/*@ assert x ≡ (long)y; */
{
- mpz_t __gen_e_acsl_x_2;
- mpz_t __gen_e_acsl_y_2;
- unsigned long __gen_e_acsl_cast_2;
- mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_x_2;
+ __e_acsl_mpz_t __gen_e_acsl_y_2;
+ long __gen_e_acsl_cast_2;
+ __e_acsl_mpz_t __gen_e_acsl__2;
int __gen_e_acsl_eq_2;
__gmpz_init_set_si(__gen_e_acsl_x_2,x);
__gmpz_init_set_si(__gen_e_acsl_y_2,(long)y);
- __gen_e_acsl_cast_2 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_y_2));
- __gmpz_init_set_ui(__gen_e_acsl__2,__gen_e_acsl_cast_2);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_2),
- (__mpz_struct const *)(__gen_e_acsl__2));
+ __gen_e_acsl_cast_2 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
+ __gmpz_init_set_si(__gen_e_acsl__2,__gen_e_acsl_cast_2);
+ __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
(char *)"main",(char *)"x == (long)y",11);
__gmpz_clear(__gen_e_acsl_x_2);
@@ -46,17 +47,17 @@ int main(void)
}
/*@ assert y ≡ (int)0; */
{
- mpz_t __gen_e_acsl_y_3;
- mpz_t __gen_e_acsl__3;
- unsigned long __gen_e_acsl_cast_3;
- mpz_t __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl_y_3;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ long __gen_e_acsl_cast_3;
+ __e_acsl_mpz_t __gen_e_acsl__4;
int __gen_e_acsl_eq_3;
__gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
__gmpz_init_set_si(__gen_e_acsl__3,0L);
- __gen_e_acsl_cast_3 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl__3));
- __gmpz_init_set_ui(__gen_e_acsl__4,__gen_e_acsl_cast_3);
- __gen_e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_y_3),
- (__mpz_struct const *)(__gen_e_acsl__4));
+ __gen_e_acsl_cast_3 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __gmpz_init_set_si(__gen_e_acsl__4,__gen_e_acsl_cast_3);
+ __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
(char *)"main",(char *)"y == (int)0",13);
__gmpz_clear(__gen_e_acsl_y_3);
@@ -65,21 +66,21 @@ int main(void)
}
/*@ assert (unsigned int)y ≡ (unsigned int)0; */
{
- mpz_t __gen_e_acsl_y_4;
+ __e_acsl_mpz_t __gen_e_acsl_y_4;
unsigned long __gen_e_acsl_cast_4;
- mpz_t __gen_e_acsl__5;
- mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ __e_acsl_mpz_t __gen_e_acsl__6;
unsigned long __gen_e_acsl_cast_5;
- mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl__7;
int __gen_e_acsl_eq_4;
__gmpz_init_set_si(__gen_e_acsl_y_4,(long)y);
- __gen_e_acsl_cast_4 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_y_4));
+ __gen_e_acsl_cast_4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_4));
__gmpz_init_set_ui(__gen_e_acsl__5,__gen_e_acsl_cast_4);
__gmpz_init_set_si(__gen_e_acsl__6,0L);
- __gen_e_acsl_cast_5 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl__6));
+ __gen_e_acsl_cast_5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
__gmpz_init_set_ui(__gen_e_acsl__7,__gen_e_acsl_cast_5);
- __gen_e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__5),
- (__mpz_struct const *)(__gen_e_acsl__7));
+ __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
__e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
(char *)"main",
(char *)"(unsigned int)y == (unsigned int)0",14);
@@ -90,17 +91,17 @@ int main(void)
}
/*@ assert y ≢ (int)0xfffffffffffffff; */
{
- mpz_t __gen_e_acsl_y_5;
- mpz_t __gen_e_acsl__8;
- unsigned long __gen_e_acsl_cast_6;
- mpz_t __gen_e_acsl__9;
+ __e_acsl_mpz_t __gen_e_acsl_y_5;
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ long __gen_e_acsl_cast_6;
+ __e_acsl_mpz_t __gen_e_acsl__9;
int __gen_e_acsl_ne;
__gmpz_init_set_si(__gen_e_acsl_y_5,(long)y);
__gmpz_init_set_ui(__gen_e_acsl__8,1152921504606846975UL);
- __gen_e_acsl_cast_6 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl__8));
- __gmpz_init_set_ui(__gen_e_acsl__9,__gen_e_acsl_cast_6);
- __gen_e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_y_5),
- (__mpz_struct const *)(__gen_e_acsl__9));
+ __gen_e_acsl_cast_6 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gmpz_init_set_si(__gen_e_acsl__9,__gen_e_acsl_cast_6);
+ __gen_e_acsl_ne = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
(char *)"y != (int)0xfffffffffffffff",17);
__gmpz_clear(__gen_e_acsl_y_5);
@@ -109,21 +110,21 @@ int main(void)
}
/*@ assert (unsigned int)y ≢ (unsigned int)0xfffffffffffffff; */
{
- mpz_t __gen_e_acsl_y_6;
+ __e_acsl_mpz_t __gen_e_acsl_y_6;
unsigned long __gen_e_acsl_cast_7;
- mpz_t __gen_e_acsl__10;
- mpz_t __gen_e_acsl__11;
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ __e_acsl_mpz_t __gen_e_acsl__11;
unsigned long __gen_e_acsl_cast_8;
- mpz_t __gen_e_acsl__12;
+ __e_acsl_mpz_t __gen_e_acsl__12;
int __gen_e_acsl_ne_2;
__gmpz_init_set_si(__gen_e_acsl_y_6,(long)y);
- __gen_e_acsl_cast_7 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_y_6));
+ __gen_e_acsl_cast_7 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_6));
__gmpz_init_set_ui(__gen_e_acsl__10,__gen_e_acsl_cast_7);
__gmpz_init_set_ui(__gen_e_acsl__11,1152921504606846975UL);
- __gen_e_acsl_cast_8 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl__11));
+ __gen_e_acsl_cast_8 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
__gmpz_init_set_ui(__gen_e_acsl__12,__gen_e_acsl_cast_8);
- __gen_e_acsl_ne_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__10),
- (__mpz_struct const *)(__gen_e_acsl__12));
+ __gen_e_acsl_ne_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
__e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
(char *)"main",
(char *)"(unsigned int)y != (unsigned int)0xfffffffffffffff",
@@ -133,6 +134,39 @@ int main(void)
__gmpz_clear(__gen_e_acsl__11);
__gmpz_clear(__gen_e_acsl__12);
}
+ int t[2] = {0, 1};
+ /*@ assert (float)x ≡ t[(int)0.1]; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl__13;
+ long __gen_e_acsl_cast_9;
+ __e_acsl_mpz_t __gen_e_acsl___gen_e_acsl_cast_9;
+ __e_acsl_mpz_t __gen_e_acsl__14;
+ int __gen_e_acsl_lt;
+ __e_acsl_mpz_t __gen_e_acsl__15;
+ int __gen_e_acsl_le;
+ __gmpz_init_set_si(__gen_e_acsl__13,(long)0.1);
+ __gen_e_acsl_cast_9 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
+ __gmpz_init_set_si(__gen_e_acsl___gen_e_acsl_cast_9,__gen_e_acsl_cast_9);
+ __gmpz_init_set_si(__gen_e_acsl__14,2L);
+ __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl___gen_e_acsl_cast_9),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
+ __e_acsl_assert(__gen_e_acsl_lt < 0,(char *)"RTE",(char *)"main",
+ (char *)"index_bound: __gen_e_acsl_cast_9 < 2",23);
+ __gmpz_init_set_si(__gen_e_acsl__15,0L);
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__15),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl___gen_e_acsl_cast_9));
+ __e_acsl_assert(__gen_e_acsl_le <= 0,(char *)"RTE",(char *)"main",
+ (char *)"index_bound: 0 <= __gen_e_acsl_cast_9",23);
+ /*@ assert Eva: index_bound: 0 ≤ __gen_e_acsl_cast_9; */
+ /*@ assert Eva: index_bound: __gen_e_acsl_cast_9 < 2; */
+ __e_acsl_assert((float)x == (float)t[__gen_e_acsl_cast_9],
+ (char *)"Assertion",(char *)"main",
+ (char *)"(float)x == t[(int)0.1]",23);
+ __gmpz_clear(__gen_e_acsl__13);
+ __gmpz_clear(__gen_e_acsl___gen_e_acsl_cast_9);
+ __gmpz_clear(__gen_e_acsl__14);
+ __gmpz_clear(__gen_e_acsl__15);
+ }
__retres = 0;
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c
index a82eeee300c89084acae75bbe704a1ad52003dbc..fb9c180c46dfceede209d330ed3a35eb3b270354 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c
@@ -1,4 +1,6 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
unsigned long long my_pow(unsigned int x, unsigned int n)
{
unsigned long long __retres;
@@ -8,12 +10,10 @@ unsigned long long my_pow(unsigned int x, unsigned int n)
__retres = (unsigned long long)1;
goto return_label;
}
- { /* sequence */
- tmp_0 = my_pow(x,n / (unsigned int)2);
- tmp = (int)tmp_0;
- }
- /*@ assert Value: signed_overflow: -2147483648 ≤ tmp*tmp; */
- /*@ assert Value: signed_overflow: tmp*tmp ≤ 2147483647; */
+ tmp_0 = my_pow(x,n / (unsigned int)2);
+ tmp = (int)tmp_0;
+ /*@ assert Eva: signed_overflow: -2147483648 ≤ tmp * tmp; */
+ /*@ assert Eva: signed_overflow: tmp * tmp ≤ 2147483647; */
tmp *= tmp;
if (n % (unsigned int)2 == (unsigned int)0) {
__retres = (unsigned long long)tmp;
@@ -26,45 +26,44 @@ unsigned long long my_pow(unsigned int x, unsigned int n)
int main(void)
{
int __retres;
- unsigned long long x;
- x = my_pow((unsigned int)2,(unsigned int)63);
- /*@ assert (2*x+1)%2 ≡ 1; */
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ unsigned long long x = my_pow((unsigned int)2,(unsigned int)63);
+ /*@ assert (2 * x + 1) % 2 ≡ 1; */
{
- mpz_t __gen_e_acsl_;
- mpz_t __gen_e_acsl_x;
- mpz_t __gen_e_acsl_mul;
- mpz_t __gen_e_acsl__2;
- mpz_t __gen_e_acsl_add;
- mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl__3;
int __gen_e_acsl_mod_guard;
- mpz_t __gen_e_acsl_mod;
- unsigned long __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl_mod;
+ long __gen_e_acsl__4;
__gmpz_init_set_si(__gen_e_acsl_,2L);
__gmpz_init(__gen_e_acsl_x);
- __gmpz_import(__gen_e_acsl_x,1UL,1,8UL,0,0UL,(void const *)(& x));
+ __gmpz_import(__gen_e_acsl_x,(size_t)1,1,(size_t)8,0,(size_t)0,
+ (void const *)(& x));
__gmpz_init(__gen_e_acsl_mul);
- __gmpz_mul(__gen_e_acsl_mul,(__mpz_struct const *)(__gen_e_acsl_),
- (__mpz_struct const *)(__gen_e_acsl_x));
+ __gmpz_mul(__gen_e_acsl_mul,(__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x));
__gmpz_init_set_si(__gen_e_acsl__2,1L);
__gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)(__gen_e_acsl_mul),
- (__mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
__gmpz_init_set_si(__gen_e_acsl__3,0L);
- __gen_e_acsl_mod_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
- (__mpz_struct const *)(__gen_e_acsl__3));
+ __gen_e_acsl_mod_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
__gmpz_init(__gen_e_acsl_mod);
/*@ assert E_ACSL: 2 ≢ 0; */
__e_acsl_assert(! (__gen_e_acsl_mod_guard == 0),(char *)"Assertion",
(char *)"main",(char *)"2 == 0",17);
- __gmpz_tdiv_r(__gen_e_acsl_mod,(__mpz_struct const *)(__gen_e_acsl_add),
- (__mpz_struct const *)(__gen_e_acsl_));
- __gen_e_acsl__4 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_mod));
- /*@ assert
- Value: ptr_comparison:
- \pointer_comparable((void *)__gen_e_acsl__4, (void *)1);
- */
- __e_acsl_assert(__gen_e_acsl__4 == 1,(char *)"Assertion",(char *)"main",
- (char *)"(2*x+1)%2 == 1",17);
+ __gmpz_tdiv_r(__gen_e_acsl_mod,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gen_e_acsl__4 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_mod));
+ __e_acsl_assert(__gen_e_acsl__4 == 1L,(char *)"Assertion",(char *)"main",
+ (char *)"(2 * x + 1) % 2 == 1",17);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_x);
__gmpz_clear(__gen_e_acsl_mul);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c
index af00a19e9e5e67004dde13c375597ffc124c084c..203245a06493a161763875b504af3b52ade5466b 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c
@@ -1,4 +1,6 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
unsigned long long my_pow(unsigned int x, unsigned int n)
{
unsigned long long __retres;
@@ -8,12 +10,10 @@ unsigned long long my_pow(unsigned int x, unsigned int n)
__retres = (unsigned long long)1;
goto return_label;
}
- { /* sequence */
- tmp_0 = my_pow(x,n / (unsigned int)2);
- tmp = (int)tmp_0;
- }
- /*@ assert Value: signed_overflow: -2147483648 ≤ tmp*tmp; */
- /*@ assert Value: signed_overflow: tmp*tmp ≤ 2147483647; */
+ tmp_0 = my_pow(x,n / (unsigned int)2);
+ tmp = (int)tmp_0;
+ /*@ assert Eva: signed_overflow: -2147483648 ≤ tmp * tmp; */
+ /*@ assert Eva: signed_overflow: tmp * tmp ≤ 2147483647; */
tmp *= tmp;
if (n % (unsigned int)2 == (unsigned int)0) {
__retres = (unsigned long long)tmp;
@@ -26,46 +26,45 @@ unsigned long long my_pow(unsigned int x, unsigned int n)
int main(void)
{
int __retres;
- unsigned long long x;
- x = my_pow((unsigned int)2,(unsigned int)63);
- /*@ assert (2*x+1)%2 ≡ 1; */
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ unsigned long long x = my_pow((unsigned int)2,(unsigned int)63);
+ /*@ assert (2 * x + 1) % 2 ≡ 1; */
{
- mpz_t __gen_e_acsl_;
- mpz_t __gen_e_acsl_x;
- mpz_t __gen_e_acsl_mul;
- mpz_t __gen_e_acsl__2;
- mpz_t __gen_e_acsl_add;
- mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl__3;
int __gen_e_acsl_mod_guard;
- mpz_t __gen_e_acsl_mod;
+ __e_acsl_mpz_t __gen_e_acsl_mod;
int __gen_e_acsl_eq;
__gmpz_init_set_si(__gen_e_acsl_,2L);
__gmpz_init(__gen_e_acsl_x);
- __gmpz_import(__gen_e_acsl_x,1UL,1,8UL,0,0UL,(void const *)(& x));
+ __gmpz_import(__gen_e_acsl_x,(size_t)1,1,(size_t)8,0,(size_t)0,
+ (void const *)(& x));
__gmpz_init(__gen_e_acsl_mul);
- __gmpz_mul(__gen_e_acsl_mul,(__mpz_struct const *)(__gen_e_acsl_),
- (__mpz_struct const *)(__gen_e_acsl_x));
+ __gmpz_mul(__gen_e_acsl_mul,(__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x));
__gmpz_init_set_si(__gen_e_acsl__2,1L);
__gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)(__gen_e_acsl_mul),
- (__mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
__gmpz_init_set_si(__gen_e_acsl__3,0L);
- __gen_e_acsl_mod_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
- (__mpz_struct const *)(__gen_e_acsl__3));
+ __gen_e_acsl_mod_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
__gmpz_init(__gen_e_acsl_mod);
/*@ assert E_ACSL: 2 ≢ 0; */
__e_acsl_assert(! (__gen_e_acsl_mod_guard == 0),(char *)"Assertion",
(char *)"main",(char *)"2 == 0",17);
- __gmpz_tdiv_r(__gen_e_acsl_mod,(__mpz_struct const *)(__gen_e_acsl_add),
- (__mpz_struct const *)(__gen_e_acsl_));
- __gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_mod),
- (__mpz_struct const *)(__gen_e_acsl__2));
- /*@ assert
- Value: ptr_comparison:
- \pointer_comparable((void *)__gen_e_acsl_eq, (void *)0);
- */
+ __gmpz_tdiv_r(__gen_e_acsl_mod,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mod),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"(2*x+1)%2 == 1",17);
+ (char *)"(2 * x + 1) % 2 == 1",17);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_x);
__gmpz_clear(__gen_e_acsl_mul);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_call.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_call.c
index 9e5ae38764a0272c6d400ab9eb49040b3bf01d0f..bf4446cc44867feef2aae41aa6b2337956b740f4 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_call.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_call.c
@@ -1,35 +1,33 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
/*@ ensures \valid(\result); */
int *__gen_e_acsl_f(int *x, int *y);
-/*@ ensures \valid(\result); */
int *f(int *x, int *y)
{
- __e_acsl_store_block((void *)(& x),8UL);
- __e_acsl_store_block((void *)(& y),8UL);
+ __e_acsl_store_block((void *)(& y),(size_t)8);
+ __e_acsl_store_block((void *)(& x),(size_t)8);
__e_acsl_initialize((void *)y,sizeof(int));
*y = 1;
- __e_acsl_delete_block((void *)(& x));
__e_acsl_delete_block((void *)(& y));
+ __e_acsl_delete_block((void *)(& x));
return x;
}
int main(void)
{
int __retres;
- int x;
int *p;
- int *q;
- int *r;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ int x = 0;
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__e_acsl_full_init((void *)(& x));
- x = 0;
+ int *q = malloc(sizeof(int));
+ __e_acsl_store_block((void *)(& q),(size_t)8);
__e_acsl_full_init((void *)(& q));
- q = (int *)malloc(sizeof(int));
- r = (int *)malloc(sizeof(int));
+ int *r = malloc(sizeof(int));
__e_acsl_full_init((void *)(& p));
p = __gen_e_acsl_f(& x,q);
__e_acsl_full_init((void *)(& q));
@@ -46,17 +44,19 @@ int main(void)
int *__gen_e_acsl_f(int *x, int *y)
{
int *__retres;
- __e_acsl_store_block((void *)(& __retres),8UL);
- __e_acsl_store_block((void *)(& x),8UL);
- __e_acsl_store_block((void *)(& y),8UL);
+ __e_acsl_store_block((void *)(& __retres),(size_t)8);
+ __e_acsl_store_block((void *)(& y),(size_t)8);
+ __e_acsl_store_block((void *)(& x),(size_t)8);
__retres = f(x,y);
{
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)__retres,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)__retres,sizeof(int),
+ (void *)__retres,
+ (void *)(& __retres));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Postcondition",(char *)"f",
(char *)"\\valid(\\result)",10);
- __e_acsl_delete_block((void *)(& x));
__e_acsl_delete_block((void *)(& y));
+ __e_acsl_delete_block((void *)(& x));
__e_acsl_delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_freeable.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_freeable.c
index 4ac268a1f3efa96799795732de71fc47f342dfea..cf5247b2a952dbbff231d47d5ff9a826d58815c2 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_freeable.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_freeable.c
@@ -1,8 +1,10 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
char array[1024];
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(array),1024UL);
+ __e_acsl_store_block((void *)(array),(size_t)1024);
__e_acsl_full_init((void *)(& array));
return;
}
@@ -11,13 +13,13 @@ int main(void)
{
int __retres;
int *p;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
/*@ assert ¬\freeable(p); */
{
int __gen_e_acsl_freeable;
- /*@ assert Value: initialisation: \initialized(&p); */
+ /*@ assert Eva: initialization: \initialized(&p); */
__gen_e_acsl_freeable = __e_acsl_freeable((void *)p);
__e_acsl_assert(! __gen_e_acsl_freeable,(char *)"Assertion",
(char *)"main",(char *)"!\\freeable(p)",15);
@@ -31,12 +33,12 @@ int main(void)
}
__e_acsl_full_init((void *)(& p));
p = (int *)malloc((unsigned long)4 * sizeof(int));
- /*@ assert ¬\freeable(p+1); */
+ /*@ assert ¬\freeable(p + 1); */
{
int __gen_e_acsl_freeable_3;
- __gen_e_acsl_freeable_3 = __e_acsl_freeable((void *)(p + 1UL));
+ __gen_e_acsl_freeable_3 = __e_acsl_freeable((void *)(p + 1));
__e_acsl_assert(! __gen_e_acsl_freeable_3,(char *)"Assertion",
- (char *)"main",(char *)"!\\freeable(p+1)",18);
+ (char *)"main",(char *)"!\\freeable(p + 1)",18);
}
/*@ assert \freeable(p); */
{
@@ -63,7 +65,7 @@ int main(void)
/*@ assert ¬\freeable(&array[5]); */
{
int __gen_e_acsl_freeable_7;
- __gen_e_acsl_freeable_7 = __e_acsl_freeable((void *)(& array[5UL]));
+ __gen_e_acsl_freeable_7 = __e_acsl_freeable((void *)(& array[5]));
__e_acsl_assert(! __gen_e_acsl_freeable_7,(char *)"Assertion",
(char *)"main",(char *)"!\\freeable(&array[5])",25);
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ghost.c
index 16a1a33e734fa6f7da1a5a0f22cbd2cb3a42ad7c..8f13de4aa0b5e7d2f8c3e6d1216c8c6b062ad6fe 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ghost.c
@@ -1,11 +1,13 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
int G = 0;
int *P;
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& P),8UL);
+ __e_acsl_store_block((void *)(& P),(size_t)8);
__e_acsl_full_init((void *)(& P));
- __e_acsl_store_block((void *)(& G),4UL);
+ __e_acsl_store_block((void *)(& G),(size_t)4);
__e_acsl_full_init((void *)(& G));
return;
}
@@ -13,25 +15,26 @@ void __e_acsl_globals_init(void)
int main(void)
{
int __retres;
- int *q;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& q),8UL);
P = & G;
+ int *q = P;
+ __e_acsl_store_block((void *)(& q),(size_t)8);
__e_acsl_full_init((void *)(& q));
- q = P;
{
int __gen_e_acsl_valid_read;
int __gen_e_acsl_valid;
__e_acsl_initialize((void *)P,sizeof(int));
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)P,sizeof(int));
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)P,sizeof(int),
+ (void *)P,(void *)(& P));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(P)",14);
- __gen_e_acsl_valid = __e_acsl_valid((void *)P,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)P,sizeof(int),(void *)P,
+ (void *)(& P));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid(P)",14);
- (*P) ++;
}
+ (*P) ++;
/*@ assert *q ≡ G; */
{
int __gen_e_acsl_initialized;
@@ -40,7 +43,9 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_read_2;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)q,sizeof(int));
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)q,sizeof(int),
+ (void *)q,
+ (void *)(& q));
__gen_e_acsl_and = __gen_e_acsl_valid_read_2;
}
else __gen_e_acsl_and = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
index 3f83c01a9e7347aad7120c2c4556af34f8e5fde9..1358d2061e4feebc47c3492a046a4e53a9296281 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdio.h"
#include "stdlib.h"
int A = 0;
int B;
@@ -31,30 +32,30 @@ int main(void)
__e_acsl_full_init((void *)(& q));
/*@ assert \initialized(&A); */
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(&A)",16);
+ (char *)"\\initialized(&A)",17);
/*@ assert \initialized(&B); */
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(&B)",17);
+ (char *)"\\initialized(&B)",18);
/*@ assert \initialized(p); */
{
int __gen_e_acsl_initialized;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(p)",18);
+ (char *)"main",(char *)"\\initialized(p)",19);
}
/*@ assert \initialized(q); */
{
int __gen_e_acsl_initialized_2;
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_2,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(q)",19);
+ (char *)"main",(char *)"\\initialized(q)",20);
}
int a = 0;
__e_acsl_store_block((void *)(& a),(size_t)4);
__e_acsl_full_init((void *)(& a));
long c[2] = {(long)1, (long)1};
__e_acsl_store_block((void *)(c),(size_t)16);
- __e_acsl_full_init((void *)(c));
+ __e_acsl_full_init((void *)(& c));
__e_acsl_full_init((void *)(& p));
p = & a;
__e_acsl_full_init((void *)(& q));
@@ -65,7 +66,7 @@ int main(void)
__gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& a),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_3,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&a)",30);
+ (char *)"main",(char *)"\\initialized(&a)",31);
}
/*@ assert ¬\initialized(&b); */
{
@@ -73,21 +74,21 @@ int main(void)
__gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& b),
sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_4,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(&b)",31);
+ (char *)"main",(char *)"!\\initialized(&b)",32);
}
/*@ assert \initialized(p); */
{
int __gen_e_acsl_initialized_5;
__gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_5,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(p)",32);
+ (char *)"main",(char *)"\\initialized(p)",33);
}
/*@ assert ¬\initialized(q); */
{
int __gen_e_acsl_initialized_6;
__gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_6,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(q)",33);
+ (char *)"main",(char *)"!\\initialized(q)",34);
}
/*@ assert \initialized(&c); */
{
@@ -95,7 +96,7 @@ int main(void)
__gen_e_acsl_initialized_7 = __e_acsl_initialized((void *)(& c),
sizeof(long [2]));
__e_acsl_assert(__gen_e_acsl_initialized_7,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&c)",34);
+ (char *)"main",(char *)"\\initialized(&c)",35);
}
/*@ assert ¬\initialized(&d); */
{
@@ -103,7 +104,7 @@ int main(void)
__gen_e_acsl_initialized_8 = __e_acsl_initialized((void *)(& d),
sizeof(long [2]));
__e_acsl_assert(! __gen_e_acsl_initialized_8,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(&d)",35);
+ (char *)"main",(char *)"!\\initialized(&d)",36);
}
__e_acsl_full_init((void *)(& b));
b = 0;
@@ -112,7 +113,7 @@ int main(void)
int __gen_e_acsl_initialized_9;
__gen_e_acsl_initialized_9 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_9,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(q)",39);
+ (char *)"main",(char *)"\\initialized(q)",40);
}
/*@ assert \initialized(&b); */
{
@@ -120,7 +121,7 @@ int main(void)
__gen_e_acsl_initialized_10 = __e_acsl_initialized((void *)(& b),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_10,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&b)",40);
+ (char *)"main",(char *)"\\initialized(&b)",41);
}
__e_acsl_full_init((void *)(& r));
r = d;
@@ -130,7 +131,7 @@ int main(void)
__gen_e_acsl_initialized_11 = __e_acsl_initialized((void *)(d),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_11,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized((long *)d)",43);
+ (char *)"main",(char *)"!\\initialized((long *)d)",44);
}
/*@ assert ¬\initialized(&d[1]); */
{
@@ -138,7 +139,7 @@ int main(void)
__gen_e_acsl_initialized_12 = __e_acsl_initialized((void *)(& d[1]),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_12,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(&d[1])",44);
+ (char *)"main",(char *)"!\\initialized(&d[1])",45);
}
/*@ assert ¬\initialized(&d); */
{
@@ -146,7 +147,7 @@ int main(void)
__gen_e_acsl_initialized_13 = __e_acsl_initialized((void *)(& d),
sizeof(long [2]));
__e_acsl_assert(! __gen_e_acsl_initialized_13,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(&d)",45);
+ (char *)"main",(char *)"!\\initialized(&d)",46);
}
/*@ assert ¬\initialized(r); */
{
@@ -154,7 +155,7 @@ int main(void)
__gen_e_acsl_initialized_14 = __e_acsl_initialized((void *)r,
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_14,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(r)",46);
+ (char *)"main",(char *)"!\\initialized(r)",47);
}
/*@ assert ¬\initialized(r + 1); */
{
@@ -162,7 +163,7 @@ int main(void)
__gen_e_acsl_initialized_15 = __e_acsl_initialized((void *)(r + 1),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_15,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(r + 1)",47);
+ (char *)"main",(char *)"!\\initialized(r + 1)",48);
}
__e_acsl_initialize((void *)(d),sizeof(long));
d[0] = (long)1;
@@ -172,7 +173,7 @@ int main(void)
__gen_e_acsl_initialized_16 = __e_acsl_initialized((void *)(d),
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_16,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized((long *)d)",50);
+ (char *)"main",(char *)"\\initialized((long *)d)",51);
}
/*@ assert ¬\initialized(&d[1]); */
{
@@ -180,7 +181,7 @@ int main(void)
__gen_e_acsl_initialized_17 = __e_acsl_initialized((void *)(& d[1]),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_17,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(&d[1])",51);
+ (char *)"main",(char *)"!\\initialized(&d[1])",52);
}
/*@ assert ¬\initialized(&d); */
{
@@ -188,7 +189,7 @@ int main(void)
__gen_e_acsl_initialized_18 = __e_acsl_initialized((void *)(& d),
sizeof(long [2]));
__e_acsl_assert(! __gen_e_acsl_initialized_18,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(&d)",52);
+ (char *)"main",(char *)"!\\initialized(&d)",53);
}
/*@ assert \initialized(r); */
{
@@ -196,7 +197,7 @@ int main(void)
__gen_e_acsl_initialized_19 = __e_acsl_initialized((void *)r,
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_19,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(r)",53);
+ (char *)"main",(char *)"\\initialized(r)",54);
}
/*@ assert ¬\initialized(r + 1); */
{
@@ -204,7 +205,7 @@ int main(void)
__gen_e_acsl_initialized_20 = __e_acsl_initialized((void *)(r + 1),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_20,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(r + 1)",54);
+ (char *)"main",(char *)"!\\initialized(r + 1)",55);
}
__e_acsl_initialize((void *)(& d[1]),sizeof(long));
d[1] = (long)1;
@@ -214,7 +215,7 @@ int main(void)
__gen_e_acsl_initialized_21 = __e_acsl_initialized((void *)(d),
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_21,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized((long *)d)",57);
+ (char *)"main",(char *)"\\initialized((long *)d)",58);
}
/*@ assert \initialized(&d[1]); */
{
@@ -222,7 +223,7 @@ int main(void)
__gen_e_acsl_initialized_22 = __e_acsl_initialized((void *)(& d[1]),
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_22,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&d[1])",58);
+ (char *)"main",(char *)"\\initialized(&d[1])",59);
}
/*@ assert \initialized(&d); */
{
@@ -230,7 +231,7 @@ int main(void)
__gen_e_acsl_initialized_23 = __e_acsl_initialized((void *)(& d),
sizeof(long [2]));
__e_acsl_assert(__gen_e_acsl_initialized_23,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&d)",59);
+ (char *)"main",(char *)"\\initialized(&d)",60);
}
/*@ assert \initialized(r); */
{
@@ -238,7 +239,7 @@ int main(void)
__gen_e_acsl_initialized_24 = __e_acsl_initialized((void *)r,
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_24,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(r)",60);
+ (char *)"main",(char *)"\\initialized(r)",61);
}
/*@ assert \initialized(r + 1); */
{
@@ -246,7 +247,7 @@ int main(void)
__gen_e_acsl_initialized_25 = __e_acsl_initialized((void *)(r + 1),
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_25,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(r + 1)",61);
+ (char *)"main",(char *)"\\initialized(r + 1)",62);
}
__e_acsl_full_init((void *)(& p));
p = (int *)malloc(sizeof(int *));
@@ -255,7 +256,7 @@ int main(void)
int __gen_e_acsl_initialized_26;
__gen_e_acsl_initialized_26 = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_26,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(p)",65);
+ (char *)"main",(char *)"!\\initialized(p)",66);
}
__e_acsl_full_init((void *)(& q));
q = (int *)calloc((unsigned long)1,sizeof(int));
@@ -264,7 +265,7 @@ int main(void)
int __gen_e_acsl_initialized_27;
__gen_e_acsl_initialized_27 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_27,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(q)",69);
+ (char *)"main",(char *)"\\initialized(q)",70);
}
__e_acsl_full_init((void *)(& q));
q = (int *)realloc((void *)q,(unsigned long)2 * sizeof(int));
@@ -273,7 +274,7 @@ int main(void)
int __gen_e_acsl_initialized_28;
__gen_e_acsl_initialized_28 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_28,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(q)",74);
+ (char *)"main",(char *)"\\initialized(q)",75);
}
__e_acsl_full_init((void *)(& q));
q ++;
@@ -282,7 +283,7 @@ int main(void)
int __gen_e_acsl_initialized_29;
__gen_e_acsl_initialized_29 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_29,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(q)",76);
+ (char *)"main",(char *)"!\\initialized(q)",77);
}
__e_acsl_full_init((void *)(& q));
q --;
@@ -291,16 +292,18 @@ int main(void)
/*@ assert ¬\initialized(p); */
{
int __gen_e_acsl_initialized_30;
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&p); */
__gen_e_acsl_initialized_30 = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_30,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(p)",84);
+ (char *)"main",(char *)"!\\initialized(p)",85);
}
/*@ assert ¬\initialized(q); */
{
int __gen_e_acsl_initialized_31;
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&q); */
__gen_e_acsl_initialized_31 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_31,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(q)",85);
+ (char *)"main",(char *)"!\\initialized(q)",86);
}
__e_acsl_full_init((void *)(& q));
q = (int *)(& q - 1024 * 5);
@@ -311,7 +314,7 @@ int main(void)
int __gen_e_acsl_initialized_32;
__gen_e_acsl_initialized_32 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_32,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(q)",93);
+ (char *)"main",(char *)"!\\initialized(q)",94);
}
__e_acsl_full_init((void *)(& p));
p = (int *)0;
@@ -320,7 +323,7 @@ int main(void)
int __gen_e_acsl_initialized_33;
__gen_e_acsl_initialized_33 = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_33,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(p)",96);
+ (char *)"main",(char *)"!\\initialized(p)",97);
}
int size = 100;
char *partsc = malloc((unsigned long)size * sizeof(char));
@@ -329,10 +332,10 @@ int main(void)
int i = 0;
while (i < size) {
if (i % 2 != 0)
- /*@ assert Value: mem_access: \valid(partsc + i); */
+ /*@ assert Eva: mem_access: \valid(partsc + i); */
*(partsc + i) = (char)'0';
else
- /*@ assert Value: mem_access: \valid(partsi + i); */
+ /*@ assert Eva: mem_access: \valid(partsi + i); */
*(partsi + i) = (char)0;
i ++;
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_invariant.c
index b937dcc050160b7ccbb6f31d54c670b246c29009..e1ac038ae1dfed70bb62129533b15f7fc74269cf 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_invariant.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_invariant.c
@@ -1,12 +1,13 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
int main(void)
{
int __retres;
- int x;
- x = 0;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ int x = 0;
{
- int i;
- i = 0;
+ int i = 0;
while (i < 10) {
/*@ invariant 0 ≤ i < 10; */
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_localvar.c
index d238cea7a4d25f4ffb1d15da64de69e493dbea07..787629e84006dcab2b937755cb866c94ea8c489a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_localvar.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_localvar.c
@@ -1,4 +1,6 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
struct list {
int element ;
struct list *next ;
@@ -6,8 +8,8 @@ struct list {
struct list *add(struct list *l, int i)
{
struct list *new;
- __e_acsl_store_block((void *)(& new),8UL);
- __e_acsl_store_block((void *)(& l),8UL);
+ __e_acsl_store_block((void *)(& new),(size_t)8);
+ __e_acsl_store_block((void *)(& l),(size_t)8);
__e_acsl_full_init((void *)(& new));
new = (struct list *)malloc(sizeof(struct list));
/*@ assert \valid(new); */
@@ -18,7 +20,8 @@ struct list *add(struct list *l, int i)
sizeof(struct list *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)new,sizeof(struct list));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)new,sizeof(struct list),
+ (void *)new,(void *)(& new));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -37,11 +40,10 @@ struct list *add(struct list *l, int i)
int main(void)
{
int __retres;
- struct list *l;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& l),8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ struct list *l = (struct list *)0;
+ __e_acsl_store_block((void *)(& l),(size_t)8);
__e_acsl_full_init((void *)(& l));
- l = (struct list *)0;
__e_acsl_full_init((void *)(& l));
l = add(l,4);
__e_acsl_full_init((void *)(& l));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_loop.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_loop.c
index 46adee7686eb208a41375ff00252f481a9b08930..fec7a5f6f53723bc5e6364c8f304f7763a61d162 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_loop.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_loop.c
@@ -1,16 +1,18 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
void simple_loop(void)
{
- int sum;
- sum = 0;
+ int sum = 0;
{
- int i;
- i = 0;
+ int i = 0;
{
- int __gen_e_acsl_and;
- if (0 <= i) __gen_e_acsl_and = i <= 10; else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,(char *)"Invariant",
- (char *)"simple_loop",(char *)"0 <= i <= 10",8);
+ {
+ int __gen_e_acsl_and;
+ if (0 <= i) __gen_e_acsl_and = i <= 10; else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Invariant",
+ (char *)"simple_loop",(char *)"0 <= i <= 10",8);
+ }
/*@ loop invariant 0 ≤ i ≤ 10; */
while (i < 10) {
sum += i;
@@ -31,61 +33,71 @@ void simple_loop(void)
void nested_loops(void)
{
int t[10][15];
- int i;
- i = 0;
+ int i = 0;
{
- int __gen_e_acsl_and;
- if (0 <= i) __gen_e_acsl_and = i <= 10; else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,(char *)"Invariant",
- (char *)"nested_loops",(char *)"0 <= i <= 10",15);
+ {
+ int __gen_e_acsl_and;
+ if (0 <= i) __gen_e_acsl_and = i <= 10; else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Invariant",
+ (char *)"nested_loops",(char *)"0 <= i <= 10",15);
+ }
/*@ loop invariant 0 ≤ i ≤ 10; */
while (i < 10) {
{
- int j;
- j = 0;
+ int j = 0;
{
- int __gen_e_acsl_forall;
- int __gen_e_acsl_k;
- int __gen_e_acsl_l;
- int __gen_e_acsl_and_2;
- __gen_e_acsl_forall = 1;
- __gen_e_acsl_k = 0;
- while (1) {
- if (__gen_e_acsl_k < i) ; else break;
- __gen_e_acsl_l = 0;
+ {
+ int __gen_e_acsl_forall;
+ int __gen_e_acsl_k;
+ int __gen_e_acsl_l;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_forall = 1;
+ __gen_e_acsl_k = 0;
while (1) {
- if (__gen_e_acsl_l < j) ; else break;
- __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_l) < 15U,
- (char *)"RTE",(char *)"nested_loops",
- (char *)"index_bound: (unsigned long)__gen_e_acsl_l < 15",
- 19);
- __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_k) < 10U,
- (char *)"RTE",(char *)"nested_loops",
- (char *)"index_bound: (unsigned long)__gen_e_acsl_k < 10",
- 19);
- if (t[(unsigned long)__gen_e_acsl_k][(unsigned long)__gen_e_acsl_l] ==
- __gen_e_acsl_k * __gen_e_acsl_l) ;
- else {
- __gen_e_acsl_forall = 0;
- goto e_acsl_end_loop1;
+ if (__gen_e_acsl_k < i) ; else break;
+ __gen_e_acsl_l = 0;
+ while (1) {
+ if (__gen_e_acsl_l < j) ; else break;
+ __e_acsl_assert(__gen_e_acsl_l < 15,(char *)"RTE",
+ (char *)"nested_loops",
+ (char *)"index_bound: __gen_e_acsl_l < 15",
+ 19);
+ __e_acsl_assert(0 <= __gen_e_acsl_l,(char *)"RTE",
+ (char *)"nested_loops",
+ (char *)"index_bound: 0 <= __gen_e_acsl_l",
+ 19);
+ __e_acsl_assert(__gen_e_acsl_k < 10,(char *)"RTE",
+ (char *)"nested_loops",
+ (char *)"index_bound: __gen_e_acsl_k < 10",
+ 19);
+ __e_acsl_assert(0 <= __gen_e_acsl_k,(char *)"RTE",
+ (char *)"nested_loops",
+ (char *)"index_bound: 0 <= __gen_e_acsl_k",
+ 19);
+ if ((long)t[__gen_e_acsl_k][__gen_e_acsl_l] == __gen_e_acsl_k * (long)__gen_e_acsl_l)
+ ;
+ else {
+ __gen_e_acsl_forall = 0;
+ goto e_acsl_end_loop1;
+ }
+ __gen_e_acsl_l ++;
}
- __gen_e_acsl_l = (int)(__gen_e_acsl_l + 1L);
+ __gen_e_acsl_k ++;
}
- __gen_e_acsl_k = (int)(__gen_e_acsl_k + 1L);
+ e_acsl_end_loop1: ;
+ __e_acsl_assert(__gen_e_acsl_forall,(char *)"Invariant",
+ (char *)"nested_loops",
+ (char *)"\\forall integer k, integer l; 0 <= k < i && 0 <= l < j ==> t[k][l] == k * l",
+ 19);
+ if (0 <= j) __gen_e_acsl_and_2 = j <= 15;
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_2,(char *)"Invariant",
+ (char *)"nested_loops",(char *)"0 <= j <= 15",17);
}
- e_acsl_end_loop1: ;
- __e_acsl_assert(__gen_e_acsl_forall,(char *)"Invariant",
- (char *)"nested_loops",
- (char *)"\\forall integer k, integer l; 0 <= k < i && 0 <= l < j ==> t[k][l] == k*l",
- 19);
- if (0 <= j) __gen_e_acsl_and_2 = j <= 15;
- else __gen_e_acsl_and_2 = 0;
- __e_acsl_assert(__gen_e_acsl_and_2,(char *)"Invariant",
- (char *)"nested_loops",(char *)"0 <= j <= 15",17);
/*@ loop invariant 0 ≤ j ≤ 15;
loop invariant
∀ ℤ k, ℤ l;
- 0 ≤ k < i ∧ 0 ≤ l < j ⇒ t[k][l] ≡ k*l;
+ 0 ≤ k < i ∧ 0 ≤ l < j ⇒ t[k][l] ≡ k * l;
*/
while (j < 15) {
t[i][j] = i * j;
@@ -107,32 +119,40 @@ void nested_loops(void)
__gen_e_acsl_l_2 = 0;
while (1) {
if (__gen_e_acsl_l_2 < j) ; else break;
- __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_l_2) < 15U,
- (char *)"RTE",(char *)"nested_loops",
- (char *)"index_bound: (unsigned long)__gen_e_acsl_l_2 < 15",
+ __e_acsl_assert(__gen_e_acsl_l_2 < 15,(char *)"RTE",
+ (char *)"nested_loops",
+ (char *)"index_bound: __gen_e_acsl_l_2 < 15",
+ 19);
+ __e_acsl_assert(0 <= __gen_e_acsl_l_2,(char *)"RTE",
+ (char *)"nested_loops",
+ (char *)"index_bound: 0 <= __gen_e_acsl_l_2",
19);
- __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_k_2) < 10U,
- (char *)"RTE",(char *)"nested_loops",
- (char *)"index_bound: (unsigned long)__gen_e_acsl_k_2 < 10",
+ __e_acsl_assert(__gen_e_acsl_k_2 < 10,(char *)"RTE",
+ (char *)"nested_loops",
+ (char *)"index_bound: __gen_e_acsl_k_2 < 10",
+ 19);
+ __e_acsl_assert(0 <= __gen_e_acsl_k_2,(char *)"RTE",
+ (char *)"nested_loops",
+ (char *)"index_bound: 0 <= __gen_e_acsl_k_2",
19);
/*@ assert
- Value: initialisation:
- \initialized(&t[(unsigned long)__gen_e_acsl_k_2][(unsigned long)__gen_e_acsl_l_2]);
+ Eva: initialization:
+ \initialized(&t[__gen_e_acsl_k_2][__gen_e_acsl_l_2]);
*/
- if (t[(unsigned long)__gen_e_acsl_k_2][(unsigned long)__gen_e_acsl_l_2] ==
- __gen_e_acsl_k_2 * __gen_e_acsl_l_2) ;
+ if ((long)t[__gen_e_acsl_k_2][__gen_e_acsl_l_2] ==
+ __gen_e_acsl_k_2 * (long)__gen_e_acsl_l_2) ;
else {
__gen_e_acsl_forall_2 = 0;
goto e_acsl_end_loop2;
}
- __gen_e_acsl_l_2 = (int)(__gen_e_acsl_l_2 + 1L);
+ __gen_e_acsl_l_2 ++;
}
- __gen_e_acsl_k_2 = (int)(__gen_e_acsl_k_2 + 1L);
+ __gen_e_acsl_k_2 ++;
}
e_acsl_end_loop2: ;
__e_acsl_assert(__gen_e_acsl_forall_2,(char *)"Invariant",
(char *)"nested_loops",
- (char *)"\\forall integer k, integer l; 0 <= k < i && 0 <= l < j ==> t[k][l] == k*l",
+ (char *)"\\forall integer k, integer l; 0 <= k < i && 0 <= l < j ==> t[k][l] == k * l",
19);
}
}
@@ -153,16 +173,16 @@ void nested_loops(void)
void unnatural_loop(void)
{
- int x;
- x = 0;
+ int x = 0;
{
- int i;
- i = 0;
+ int i = 0;
{
- int __gen_e_acsl_and;
- if (0 <= i) __gen_e_acsl_and = i <= 6; else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,(char *)"Invariant",
- (char *)"unnatural_loop",(char *)"0 <= i <= 6",26);
+ {
+ int __gen_e_acsl_and;
+ if (0 <= i) __gen_e_acsl_and = i <= 6; else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Invariant",
+ (char *)"unnatural_loop",(char *)"0 <= i <= 6",26);
+ }
/*@ loop invariant 0 ≤ i ≤ 6; */
while (i < 10) {
if (x == 5) break;
@@ -184,6 +204,7 @@ void unnatural_loop(void)
int main(void)
{
int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
simple_loop();
nested_loops();
unnatural_loop();
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_valid.c
index d6e48e6949ca30dee52516e466ecd8b5cd3815dc..fc8127008e9303c2a32b0e45c891238869e494ef 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_valid.c
@@ -1,26 +1,27 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
int *X;
int Z;
/*@ requires \valid(x);
ensures \valid(\result); */
int *__gen_e_acsl_f(int *x);
-/*@ requires \valid(x);
- ensures \valid(\result); */
int *f(int *x)
{
int *y;
- __e_acsl_store_block((void *)(& y),8UL);
+ __e_acsl_store_block((void *)(& y),(size_t)8);
/*@ assert ¬\valid(y); */
{
int __gen_e_acsl_initialized;
int __gen_e_acsl_and;
- __e_acsl_store_block((void *)(& x),8UL);
+ __e_acsl_store_block((void *)(& x),(size_t)8);
__gen_e_acsl_initialized = __e_acsl_initialized((void *)(& y),
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),(void *)y,
+ (void *)(& y));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -32,7 +33,8 @@ int *f(int *x)
/*@ assert \valid(x); */
{
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)x,sizeof(int));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)x,sizeof(int),(void *)x,
+ (void *)(& x));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",(char *)"f",
(char *)"\\valid(x)",19);
}
@@ -46,9 +48,9 @@ void g(void)
int m;
int *u;
int **p;
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& u),8UL);
- __e_acsl_store_block((void *)(& m),4UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& u),(size_t)8);
+ __e_acsl_store_block((void *)(& m),(size_t)4);
__e_acsl_full_init((void *)(& p));
p = & u;
__e_acsl_full_init((void *)(& u));
@@ -69,13 +71,16 @@ void g(void)
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)p,
- sizeof(int *));
+ sizeof(int *),
+ (void *)p,
+ (void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid_read;
}
else __gen_e_acsl_and = 0;
__e_acsl_assert(__gen_e_acsl_and,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(p)",28);
- __gen_e_acsl_valid = __e_acsl_valid((void *)*p,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)*p,sizeof(int),(void *)*p,
+ (void *)p);
__gen_e_acsl_and_2 = __gen_e_acsl_valid;
}
else __gen_e_acsl_and_2 = 0;
@@ -93,18 +98,21 @@ void g(void)
int *__gen_e_acsl_f(int *x)
{
int *__retres;
- __e_acsl_store_block((void *)(& __retres),8UL);
+ __e_acsl_store_block((void *)(& __retres),(size_t)8);
{
int __gen_e_acsl_valid;
- __e_acsl_store_block((void *)(& x),8UL);
- __gen_e_acsl_valid = __e_acsl_valid((void *)x,sizeof(int));
+ __e_acsl_store_block((void *)(& x),(size_t)8);
+ __gen_e_acsl_valid = __e_acsl_valid((void *)x,sizeof(int),(void *)x,
+ (void *)(& x));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"f",
(char *)"\\valid(x)",13);
- __retres = f(x);
}
+ __retres = f(x);
{
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)__retres,sizeof(int));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)__retres,sizeof(int),
+ (void *)__retres,
+ (void *)(& __retres));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Postcondition",(char *)"f",
(char *)"\\valid(\\result)",14);
__e_acsl_delete_block((void *)(& x));
@@ -115,9 +123,9 @@ int *__gen_e_acsl_f(int *x)
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& Z),4UL);
+ __e_acsl_store_block((void *)(& Z),(size_t)4);
__e_acsl_full_init((void *)(& Z));
- __e_acsl_store_block((void *)(& X),8UL);
+ __e_acsl_store_block((void *)(& X),(size_t)8);
__e_acsl_full_init((void *)(& X));
return;
}
@@ -129,16 +137,15 @@ int main(void)
int *b;
int **c;
int ***d;
- int n;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& n),4UL);
- __e_acsl_store_block((void *)(& d),8UL);
- __e_acsl_store_block((void *)(& c),8UL);
- __e_acsl_store_block((void *)(& b),8UL);
- __e_acsl_store_block((void *)(& a),8UL);
+ __e_acsl_store_block((void *)(& d),(size_t)8);
+ __e_acsl_store_block((void *)(& c),(size_t)8);
+ __e_acsl_store_block((void *)(& b),(size_t)8);
+ __e_acsl_store_block((void *)(& a),(size_t)8);
+ int n = 0;
+ __e_acsl_store_block((void *)(& n),(size_t)4);
__e_acsl_full_init((void *)(& n));
- n = 0;
/*@ assert ¬\valid(a) ∧ ¬\valid(b) ∧ ¬\valid(X); */
{
int __gen_e_acsl_initialized;
@@ -149,7 +156,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)a,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)a,sizeof(int),(void *)a,
+ (void *)(& a));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -160,7 +168,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)b,sizeof(int));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)b,sizeof(int),
+ (void *)b,(void *)(& b));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -169,7 +178,8 @@ int main(void)
else __gen_e_acsl_and_3 = 0;
if (__gen_e_acsl_and_3) {
int __gen_e_acsl_valid_3;
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)X,sizeof(int));
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)X,sizeof(int),(void *)X,
+ (void *)(& X));
__gen_e_acsl_and_4 = ! __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_4 = 0;
@@ -188,7 +198,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_3) {
int __gen_e_acsl_valid_4;
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)a,sizeof(int));
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)a,sizeof(int),(void *)a,
+ (void *)(& a));
__gen_e_acsl_and_5 = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and_5 = 0;
@@ -199,7 +210,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_4) {
int __gen_e_acsl_valid_5;
- __gen_e_acsl_valid_5 = __e_acsl_valid((void *)b,sizeof(int));
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)b,sizeof(int),
+ (void *)b,(void *)(& b));
__gen_e_acsl_and_6 = __gen_e_acsl_valid_5;
}
else __gen_e_acsl_and_6 = 0;
@@ -208,7 +220,8 @@ int main(void)
else __gen_e_acsl_and_7 = 0;
if (__gen_e_acsl_and_7) {
int __gen_e_acsl_valid_6;
- __gen_e_acsl_valid_6 = __e_acsl_valid((void *)X,sizeof(int));
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)X,sizeof(int),(void *)X,
+ (void *)(& X));
__gen_e_acsl_and_8 = ! __gen_e_acsl_valid_6;
}
else __gen_e_acsl_and_8 = 0;
@@ -226,7 +239,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_5) {
int __gen_e_acsl_valid_7;
- __gen_e_acsl_valid_7 = __e_acsl_valid((void *)a,sizeof(int));
+ __gen_e_acsl_valid_7 = __e_acsl_valid((void *)a,sizeof(int),(void *)a,
+ (void *)(& a));
__gen_e_acsl_and_9 = __gen_e_acsl_valid_7;
}
else __gen_e_acsl_and_9 = 0;
@@ -237,7 +251,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_6) {
int __gen_e_acsl_valid_8;
- __gen_e_acsl_valid_8 = __e_acsl_valid((void *)b,sizeof(int));
+ __gen_e_acsl_valid_8 = __e_acsl_valid((void *)b,sizeof(int),
+ (void *)b,(void *)(& b));
__gen_e_acsl_and_10 = __gen_e_acsl_valid_8;
}
else __gen_e_acsl_and_10 = 0;
@@ -246,7 +261,8 @@ int main(void)
else __gen_e_acsl_and_11 = 0;
if (__gen_e_acsl_and_11) {
int __gen_e_acsl_valid_9;
- __gen_e_acsl_valid_9 = __e_acsl_valid((void *)X,sizeof(int));
+ __gen_e_acsl_valid_9 = __e_acsl_valid((void *)X,sizeof(int),(void *)X,
+ (void *)(& X));
__gen_e_acsl_and_12 = __gen_e_acsl_valid_9;
}
else __gen_e_acsl_and_12 = 0;
@@ -265,7 +281,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_7) {
int __gen_e_acsl_valid_10;
- __gen_e_acsl_valid_10 = __e_acsl_valid((void *)a,sizeof(int));
+ __gen_e_acsl_valid_10 = __e_acsl_valid((void *)a,sizeof(int),(void *)a,
+ (void *)(& a));
__gen_e_acsl_and_13 = __gen_e_acsl_valid_10;
}
else __gen_e_acsl_and_13 = 0;
@@ -276,7 +293,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_8) {
int __gen_e_acsl_valid_11;
- __gen_e_acsl_valid_11 = __e_acsl_valid((void *)b,sizeof(int));
+ __gen_e_acsl_valid_11 = __e_acsl_valid((void *)b,sizeof(int),
+ (void *)b,(void *)(& b));
__gen_e_acsl_and_14 = __gen_e_acsl_valid_11;
}
else __gen_e_acsl_and_14 = 0;
@@ -285,7 +303,8 @@ int main(void)
else __gen_e_acsl_and_15 = 0;
if (__gen_e_acsl_and_15) {
int __gen_e_acsl_valid_12;
- __gen_e_acsl_valid_12 = __e_acsl_valid((void *)X,sizeof(int));
+ __gen_e_acsl_valid_12 = __e_acsl_valid((void *)X,sizeof(int),(void *)X,
+ (void *)(& X));
__gen_e_acsl_and_16 = __gen_e_acsl_valid_12;
}
else __gen_e_acsl_and_16 = 0;
@@ -303,7 +322,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_9) {
int __gen_e_acsl_valid_13;
- __gen_e_acsl_valid_13 = __e_acsl_valid((void *)a,sizeof(int));
+ __gen_e_acsl_valid_13 = __e_acsl_valid((void *)a,sizeof(int),(void *)a,
+ (void *)(& a));
__gen_e_acsl_and_17 = __gen_e_acsl_valid_13;
}
else __gen_e_acsl_and_17 = 0;
@@ -314,7 +334,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_10) {
int __gen_e_acsl_valid_14;
- __gen_e_acsl_valid_14 = __e_acsl_valid((void *)b,sizeof(int));
+ __gen_e_acsl_valid_14 = __e_acsl_valid((void *)b,sizeof(int),
+ (void *)b,(void *)(& b));
__gen_e_acsl_and_18 = __gen_e_acsl_valid_14;
}
else __gen_e_acsl_and_18 = 0;
@@ -323,7 +344,8 @@ int main(void)
else __gen_e_acsl_and_19 = 0;
if (__gen_e_acsl_and_19) {
int __gen_e_acsl_valid_15;
- __gen_e_acsl_valid_15 = __e_acsl_valid((void *)X,sizeof(int));
+ __gen_e_acsl_valid_15 = __e_acsl_valid((void *)X,sizeof(int),(void *)X,
+ (void *)(& X));
__gen_e_acsl_and_20 = __gen_e_acsl_valid_15;
}
else __gen_e_acsl_and_20 = 0;
@@ -349,13 +371,16 @@ int main(void)
if (__gen_e_acsl_initialized_12) {
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)c,
- sizeof(int *));
+ sizeof(int *),
+ (void *)c,
+ (void *)(& c));
__gen_e_acsl_and_21 = __gen_e_acsl_valid_read;
}
else __gen_e_acsl_and_21 = 0;
__e_acsl_assert(__gen_e_acsl_and_21,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(c)",44);
- __gen_e_acsl_valid_16 = __e_acsl_valid((void *)*c,sizeof(int));
+ __gen_e_acsl_valid_16 = __e_acsl_valid((void *)*c,sizeof(int),
+ (void *)*c,(void *)c);
__gen_e_acsl_and_22 = __gen_e_acsl_valid_16;
}
else __gen_e_acsl_and_22 = 0;
@@ -367,7 +392,8 @@ int main(void)
int __gen_e_acsl_valid_read_2;
int __gen_e_acsl_initialized_13;
int __gen_e_acsl_and_26;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)d,sizeof(int **));
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)d,sizeof(int **),
+ (void *)d,(void *)(& d));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(d)",45);
__gen_e_acsl_initialized_13 = __e_acsl_initialized((void *)*d,
@@ -389,14 +415,17 @@ int main(void)
if (__gen_e_acsl_initialized_15) {
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)d,
- sizeof(int **));
+ sizeof(int **),
+ (void *)d,
+ (void *)(& d));
__gen_e_acsl_and_23 = __gen_e_acsl_valid_read_3;
}
else __gen_e_acsl_and_23 = 0;
__e_acsl_assert(__gen_e_acsl_and_23,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(d)",45);
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)*d,
- sizeof(int *));
+ sizeof(int *),
+ (void *)*d,(void *)d);
__gen_e_acsl_and_24 = __gen_e_acsl_valid_read_4;
}
else __gen_e_acsl_and_24 = 0;
@@ -407,13 +436,16 @@ int main(void)
if (__gen_e_acsl_initialized_16) {
int __gen_e_acsl_valid_read_5;
__gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)d,
- sizeof(int **));
+ sizeof(int **),
+ (void *)d,
+ (void *)(& d));
__gen_e_acsl_and_25 = __gen_e_acsl_valid_read_5;
}
else __gen_e_acsl_and_25 = 0;
__e_acsl_assert(__gen_e_acsl_and_25,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(d)",45);
- __gen_e_acsl_valid_17 = __e_acsl_valid((void *)*(*d),sizeof(int));
+ __gen_e_acsl_valid_17 = __e_acsl_valid((void *)*(*d),sizeof(int),
+ (void *)*(*d),(void *)*d);
__gen_e_acsl_and_26 = __gen_e_acsl_valid_17;
}
else __gen_e_acsl_and_26 = 0;
@@ -431,8 +463,9 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_17) {
int __gen_e_acsl_valid_18;
- /*@ assert Value: dangling_pointer: ¬\dangling(&a); */
- __gen_e_acsl_valid_18 = __e_acsl_valid((void *)a,sizeof(int));
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&a); */
+ __gen_e_acsl_valid_18 = __e_acsl_valid((void *)a,sizeof(int),(void *)a,
+ (void *)(& a));
__gen_e_acsl_and_27 = __gen_e_acsl_valid_18;
}
else __gen_e_acsl_and_27 = 0;
@@ -443,7 +476,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_18) {
int __gen_e_acsl_valid_19;
- __gen_e_acsl_valid_19 = __e_acsl_valid((void *)b,sizeof(int));
+ __gen_e_acsl_valid_19 = __e_acsl_valid((void *)b,sizeof(int),
+ (void *)b,(void *)(& b));
__gen_e_acsl_and_28 = __gen_e_acsl_valid_19;
}
else __gen_e_acsl_and_28 = 0;
@@ -452,7 +486,8 @@ int main(void)
else __gen_e_acsl_and_29 = 0;
if (__gen_e_acsl_and_29) {
int __gen_e_acsl_valid_20;
- __gen_e_acsl_valid_20 = __e_acsl_valid((void *)X,sizeof(int));
+ __gen_e_acsl_valid_20 = __e_acsl_valid((void *)X,sizeof(int),(void *)X,
+ (void *)(& X));
__gen_e_acsl_and_30 = __gen_e_acsl_valid_20;
}
else __gen_e_acsl_and_30 = 0;
@@ -462,7 +497,8 @@ int main(void)
/*@ assert \valid(&Z); */
{
int __gen_e_acsl_valid_21;
- __gen_e_acsl_valid_21 = __e_acsl_valid((void *)(& Z),sizeof(int));
+ __gen_e_acsl_valid_21 = __e_acsl_valid((void *)(& Z),sizeof(int),
+ (void *)(& Z),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_21,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&Z)",48);
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_valid_alias.c
index 1fbd54747adf1f32ee2e053012ec64de62214e94..240cfaf9d6fe6d0536c732bbf541b554ebb7c22c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_valid_alias.c
@@ -1,14 +1,15 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
int main(void)
{
int __retres;
int *a;
int *b;
- int n;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& b),8UL);
- __e_acsl_store_block((void *)(& a),8UL);
- n = 0;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& b),(size_t)8);
+ __e_acsl_store_block((void *)(& a),(size_t)8);
+ int n = 0;
/*@ assert ¬\valid(a) ∧ ¬\valid(b); */
{
int __gen_e_acsl_initialized;
@@ -18,7 +19,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)a,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)a,sizeof(int),(void *)a,
+ (void *)(& a));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -29,7 +31,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)b,sizeof(int));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)b,sizeof(int),
+ (void *)b,(void *)(& b));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -54,7 +57,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_3) {
int __gen_e_acsl_valid_3;
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)a,sizeof(int));
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)a,sizeof(int),(void *)a,
+ (void *)(& a));
__gen_e_acsl_and_4 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_4 = 0;
@@ -65,7 +69,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_4) {
int __gen_e_acsl_valid_4;
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)b,sizeof(int));
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)b,sizeof(int),
+ (void *)b,(void *)(& b));
__gen_e_acsl_and_5 = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and_5 = 0;
@@ -83,7 +88,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_5) {
int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)b,sizeof(int));
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)b,sizeof(int),
+ (void *)b,(void *)(& b));
__gen_e_acsl_and_7 = __gen_e_acsl_valid_read;
}
else __gen_e_acsl_and_7 = 0;
@@ -102,8 +108,9 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_6) {
int __gen_e_acsl_valid_5;
- /*@ assert Value: dangling_pointer: ¬\dangling(&a); */
- __gen_e_acsl_valid_5 = __e_acsl_valid((void *)a,sizeof(int));
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&a); */
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)a,sizeof(int),(void *)a,
+ (void *)(& a));
__gen_e_acsl_and_8 = __gen_e_acsl_valid_5;
}
else __gen_e_acsl_and_8 = 0;
@@ -114,8 +121,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_7) {
int __gen_e_acsl_valid_6;
- /*@ assert Value: dangling_pointer: ¬\dangling(&b); */
- __gen_e_acsl_valid_6 = __e_acsl_valid((void *)b,sizeof(int));
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)b,sizeof(int),
+ (void *)b,(void *)(& b));
__gen_e_acsl_and_9 = __gen_e_acsl_valid_6;
}
else __gen_e_acsl_and_9 = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_valid_in_contract.c
index d6d8a05b17e38aab26d9bc3e4ed2828f30d90161..06099dcf046460bfae680882c849d663262faf31 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_valid_in_contract.c
@@ -1,4 +1,6 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
struct list {
int element ;
struct list *next ;
@@ -8,26 +10,16 @@ struct list {
ensures \result ≡ \old(l);
behavior B2:
- assumes ¬\valid(l);
- assumes ¬\valid(l->next);
+ assumes ¬\valid(l) ∨ ¬\valid(l->next);
ensures \result ≡ \old(l);
*/
struct list *__gen_e_acsl_f(struct list *l);
-/*@ behavior B1:
- assumes l ≡ \null;
- ensures \result ≡ \old(l);
-
- behavior B2:
- assumes ¬\valid(l);
- assumes ¬\valid(l->next);
- ensures \result ≡ \old(l);
- */
struct list *f(struct list *l)
{
struct list *__retres;
- __e_acsl_store_block((void *)(& __retres),8UL);
- __e_acsl_store_block((void *)(& l),8UL);
+ __e_acsl_store_block((void *)(& __retres),(size_t)8);
+ __e_acsl_store_block((void *)(& l),(size_t)8);
if (l == (struct list *)0) {
__e_acsl_full_init((void *)(& __retres));
__retres = l;
@@ -41,15 +33,17 @@ struct list *f(struct list *l)
__e_acsl_full_init((void *)(& __retres));
__retres = (struct list *)0;
return_label:
+ {
__e_acsl_delete_block((void *)(& l));
__e_acsl_delete_block((void *)(& __retres));
return __retres;
+ }
}
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__gen_e_acsl_f((struct list *)0);
__retres = 0;
__e_acsl_memory_clean();
@@ -61,8 +55,7 @@ int main(void)
ensures \result ≡ \old(l);
behavior B2:
- assumes ¬\valid(l);
- assumes ¬\valid(l->next);
+ assumes ¬\valid(l) ∨ ¬\valid(l->next);
ensures \result ≡ \old(l);
*/
struct list *__gen_e_acsl_f(struct list *l)
@@ -72,15 +65,15 @@ struct list *__gen_e_acsl_f(struct list *l)
struct list *__gen_e_acsl_at_2;
int __gen_e_acsl_at;
struct list *__retres;
- __e_acsl_store_block((void *)(& __retres),8UL);
- __e_acsl_store_block((void *)(& l),8UL);
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_4),8UL);
+ __e_acsl_store_block((void *)(& __retres),(size_t)8);
__gen_e_acsl_at_4 = l;
{
int __gen_e_acsl_valid;
- int __gen_e_acsl_and_2;
- __gen_e_acsl_valid = __e_acsl_valid((void *)l,sizeof(struct list));
- if (! __gen_e_acsl_valid) {
+ int __gen_e_acsl_or;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)l,sizeof(struct list),
+ (void *)l,(void *)(& l));
+ if (! __gen_e_acsl_valid) __gen_e_acsl_or = 1;
+ else {
int __gen_e_acsl_initialized;
int __gen_e_acsl_and;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)(& l->next),
@@ -89,24 +82,25 @@ struct list *__gen_e_acsl_f(struct list *l)
int __gen_e_acsl_valid_read;
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& l->next),
- sizeof(struct list *));
+ sizeof(struct list *),
+ (void *)(& l->next),
+ (void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
- (char *)"mem_access: \\valid_read(&l->next)",19);
- /*@ assert Value: mem_access: \valid_read(&l->next); */
+ (char *)"mem_access: \\valid_read(&l->next)",18);
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)l->next,
- sizeof(struct list));
+ sizeof(struct list),
+ (void *)l->next,
+ (void *)(& l->next));
__gen_e_acsl_and = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and = 0;
- __gen_e_acsl_and_2 = ! __gen_e_acsl_and;
+ __gen_e_acsl_or = ! __gen_e_acsl_and;
}
- else __gen_e_acsl_and_2 = 0;
- __gen_e_acsl_at_3 = __gen_e_acsl_and_2;
+ __gen_e_acsl_at_3 = __gen_e_acsl_or;
}
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_2),8UL);
__gen_e_acsl_at_2 = l;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at),4UL);
- __gen_e_acsl_at = l == (void *)0;
+ __gen_e_acsl_at = l == (struct list *)0;
+ __e_acsl_store_block((void *)(& l),(size_t)8);
__retres = f(l);
{
int __gen_e_acsl_implies;
@@ -119,8 +113,8 @@ struct list *__gen_e_acsl_f(struct list *l)
else __gen_e_acsl_implies_2 = __retres == __gen_e_acsl_at_4;
__e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Postcondition",
(char *)"f",
- (char *)"\\old(!\\valid{Here}(l) && !\\valid{Here}(l->next)) ==> \\result == \\old(l)",
- 20);
+ (char *)"\\old(!\\valid{Here}(l) || !\\valid{Here}(l->next)) ==> \\result == \\old(l)",
+ 19);
__e_acsl_delete_block((void *)(& l));
__e_acsl_delete_block((void *)(& __retres));
return __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_vector.c
index a956c2f63b3ff4ac66124a9822480ef5e3bd2291..ed998b8cb0fa6a35045fd43761a59fb9b93375f7 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_vector.c
@@ -1,10 +1,12 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
int LAST;
int *new_inversed(int len, int *v)
{
int i;
int *p;
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
p = (int *)malloc(sizeof(int) * (unsigned long)len);
i = 0;
@@ -20,41 +22,35 @@ int *new_inversed(int len, int *v)
int main(void)
{
int __retres;
- int x;
- int v1[3];
int *v2;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& v2),8UL);
- __e_acsl_store_block((void *)(v1),12UL);
- x = 3;
- __e_acsl_initialize((void *)(v1),sizeof(int));
- v1[0] = 1;
- __e_acsl_initialize((void *)(& v1[1]),sizeof(int));
- v1[1] = 2;
- __e_acsl_initialize((void *)(& v1[2]),sizeof(int));
- v1[2] = x;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& v2),(size_t)8);
+ int x = 3;
+ int v1[3] = {1, 2, x};
+ __e_acsl_store_block((void *)(v1),(size_t)12);
+ __e_acsl_full_init((void *)(& v1));
LAST = v1[2];
/*@ assert \initialized(&v1[2]); */
{
int __gen_e_acsl_initialized;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& v1[2UL]),
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& v1[2]),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
(char *)"main",(char *)"\\initialized(&v1[2])",24);
}
__e_acsl_full_init((void *)(& v2));
v2 = new_inversed(3,v1);
+ /*@ assert Eva: initialization: \initialized(v2 + 2); */
LAST = *(v2 + 2);
- /*@ assert \initialized(v2+2); */
+ /*@ assert \initialized(v2 + 2); */
{
int __gen_e_acsl_initialized_2;
- __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(v2 + 2UL),
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(v2 + 2),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_2,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(v2+2)",27);
+ (char *)"main",(char *)"\\initialized(v2 + 2)",27);
}
/*@ assert LAST ≡ 1; */
- /*@ assert Value: initialisation: \initialized(&LAST); */
__e_acsl_assert(LAST == 1,(char *)"Assertion",(char *)"main",
(char *)"LAST == 1",28);
free((void *)v2);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
index 3408a9d5cd5b3182d88c007e7ac4a0151d87f882..2ae6332f88fc911b73f5d0ed1321e089bf186ff4 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
@@ -40,7 +40,7 @@ int main(int argc, char const **argv)
{
int __gen_e_acsl_or;
/*@ assert
- Value: ptr_comparison: \pointer_comparable((void *)g1, (void *)0);
+ Eva: ptr_comparison: \pointer_comparable((void *)g1, (void *)0);
*/
if (g1 == (char *)0) __gen_e_acsl_or = 1;
else {
@@ -64,7 +64,7 @@ int main(int argc, char const **argv)
{
int __gen_e_acsl_or_2;
/*@ assert
- Value: ptr_comparison: \pointer_comparable((void *)g2, (void *)0);
+ Eva: ptr_comparison: \pointer_comparable((void *)g2, (void *)0);
*/
if (g2 == (char *)0) __gen_e_acsl_or_2 = 1;
else {