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 6b7354a356dbad21526e2603c23c3dbc97711008..d6f5642b29065594aba77fcb0f93eb2cdb6cd9fd 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
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -147,7 +147,7 @@ extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),8U);
+ __store_block((void *)(& __retres),8UL);
__retres = __malloc(size);
__delete_block((void *)(& __retres));
return __retres;
@@ -175,8 +175,8 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __store_block((void *)(& p),8U);
- __store_block((void *)(& __e_acsl_at),4U);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(& __e_acsl_at),4UL);
__e_acsl_at = p != (void *)0;
__free(p);
__delete_block((void *)(& p));
@@ -195,16 +195,16 @@ int Z;
int *f(int *x)
{
int *y;
- __store_block((void *)(& y),8U);
+ __store_block((void *)(& y),8UL);
/*@ assert ¬\valid(y); */
{
int __e_acsl_initialized;
int __e_acsl_and;
- __store_block((void *)(& x),8U);
- __e_acsl_initialized = __initialized((void *)(& y),(size_t)sizeof(int *));
+ __store_block((void *)(& x),8UL);
+ __e_acsl_initialized = __initialized((void *)(& y),sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = __valid((void *)y,(size_t)sizeof(int));
+ __e_acsl_valid = __valid((void *)y,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else __e_acsl_and = 0;
@@ -216,7 +216,7 @@ int *f(int *x)
/*@ assert \valid(x); */
{
int __e_acsl_valid_2;
- __e_acsl_valid_2 = __valid((void *)x,(size_t)sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)x,sizeof(int));
e_acsl_assert(__e_acsl_valid_2,(char *)"Assertion",(char *)"f",
(char *)"\\valid(x)",21);
}
@@ -230,18 +230,18 @@ int *f(int *x)
int *__e_acsl_f(int *x)
{
int *__retres;
- __store_block((void *)(& __retres),8U);
+ __store_block((void *)(& __retres),8UL);
{
int __e_acsl_valid;
- __store_block((void *)(& x),8U);
- __e_acsl_valid = __valid((void *)x,(size_t)sizeof(int));
+ __store_block((void *)(& x),8UL);
+ __e_acsl_valid = __valid((void *)x,sizeof(int));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"f",
(char *)"\\valid(x)",15);
__retres = f(x);
}
{
int __e_acsl_valid_2;
- __e_acsl_valid_2 = __valid((void *)__retres,(size_t)sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)__retres,sizeof(int));
e_acsl_assert(__e_acsl_valid_2,(char *)"Postcondition",(char *)"f",
(char *)"\\valid(\\result)",16);
__delete_block((void *)(& x));
@@ -255,9 +255,9 @@ void g(void)
int m;
int *u;
int **p;
- __store_block((void *)(& p),8U);
- __store_block((void *)(& u),8U);
- __store_block((void *)(& m),4U);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(& u),8UL);
+ __store_block((void *)(& m),4UL);
__full_init((void *)(& p));
p = & u;
__full_init((void *)(& u));
@@ -268,22 +268,21 @@ void g(void)
{
int __e_acsl_initialized;
int __e_acsl_and_2;
- __e_acsl_initialized = __initialized((void *)p,(size_t)sizeof(int *));
+ __e_acsl_initialized = __initialized((void *)p,sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_initialized_2;
int __e_acsl_and;
int __e_acsl_valid;
- __e_acsl_initialized_2 = __initialized((void *)(& p),
- (size_t)sizeof(int **));
+ __e_acsl_initialized_2 = __initialized((void *)(& p),sizeof(int **));
if (__e_acsl_initialized_2) {
int __e_acsl_valid_read;
- __e_acsl_valid_read = __valid_read((void *)p,(size_t)sizeof(int *));
+ __e_acsl_valid_read = __valid_read((void *)p,sizeof(int *));
__e_acsl_and = __e_acsl_valid_read;
}
else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(p)",30);
- __e_acsl_valid = __valid((void *)*p,(size_t)sizeof(int));
+ __e_acsl_valid = __valid((void *)*p,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid;
}
else __e_acsl_and_2 = 0;
@@ -298,8 +297,8 @@ void g(void)
void __e_acsl_memory_init(void)
{
- __store_block((void *)(& Z),4U);
- __store_block((void *)(& X),8U);
+ __store_block((void *)(& Z),4UL);
+ __store_block((void *)(& X),8UL);
return;
}
@@ -312,11 +311,11 @@ int main(void)
int ***d;
int n;
__e_acsl_memory_init();
- __store_block((void *)(& n),4U);
- __store_block((void *)(& d),8U);
- __store_block((void *)(& c),8U);
- __store_block((void *)(& b),8U);
- __store_block((void *)(& a),8U);
+ __store_block((void *)(& n),4UL);
+ __store_block((void *)(& d),8UL);
+ __store_block((void *)(& c),8UL);
+ __store_block((void *)(& b),8UL);
+ __store_block((void *)(& a),8UL);
__full_init((void *)(& n));
n = 0;
/*@ assert (¬\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
@@ -325,21 +324,20 @@ int main(void)
int __e_acsl_and;
int __e_acsl_and_3;
int __e_acsl_and_4;
- __e_acsl_initialized = __initialized((void *)(& a),(size_t)sizeof(int *));
+ __e_acsl_initialized = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_valid = __valid((void *)a,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else __e_acsl_and = 0;
if (! __e_acsl_and) {
int __e_acsl_initialized_2;
int __e_acsl_and_2;
- __e_acsl_initialized_2 = __initialized((void *)(& b),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_2 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_2) {
int __e_acsl_valid_2;
- __e_acsl_valid_2 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)b,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_2;
}
else __e_acsl_and_2 = 0;
@@ -348,7 +346,7 @@ int main(void)
else __e_acsl_and_3 = 0;
if (__e_acsl_and_3) {
int __e_acsl_valid_3;
- __e_acsl_valid_3 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_valid_3 = __valid((void *)X,sizeof(int));
__e_acsl_and_4 = ! __e_acsl_valid_3;
}
else __e_acsl_and_4 = 0;
@@ -356,29 +354,27 @@ int main(void)
(char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",35);
}
__full_init((void *)(& a));
- a = (int *)__e_acsl_malloc((unsigned int)sizeof(int));
+ a = (int *)__e_acsl_malloc(sizeof(int));
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
{
int __e_acsl_initialized_3;
int __e_acsl_and_5;
int __e_acsl_and_7;
int __e_acsl_and_8;
- __e_acsl_initialized_3 = __initialized((void *)(& a),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_3 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_3) {
int __e_acsl_valid_4;
- __e_acsl_valid_4 = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_valid_4 = __valid((void *)a,sizeof(int));
__e_acsl_and_5 = __e_acsl_valid_4;
}
else __e_acsl_and_5 = 0;
if (__e_acsl_and_5) {
int __e_acsl_initialized_4;
int __e_acsl_and_6;
- __e_acsl_initialized_4 = __initialized((void *)(& b),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_4 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_4) {
int __e_acsl_valid_5;
- __e_acsl_valid_5 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_valid_5 = __valid((void *)b,sizeof(int));
__e_acsl_and_6 = __e_acsl_valid_5;
}
else __e_acsl_and_6 = 0;
@@ -387,7 +383,7 @@ int main(void)
else __e_acsl_and_7 = 0;
if (__e_acsl_and_7) {
int __e_acsl_valid_6;
- __e_acsl_valid_6 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_valid_6 = __valid((void *)X,sizeof(int));
__e_acsl_and_8 = ! __e_acsl_valid_6;
}
else __e_acsl_and_8 = 0;
@@ -401,22 +397,20 @@ int main(void)
int __e_acsl_and_9;
int __e_acsl_and_11;
int __e_acsl_and_12;
- __e_acsl_initialized_5 = __initialized((void *)(& a),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_5 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_5) {
int __e_acsl_valid_7;
- __e_acsl_valid_7 = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_valid_7 = __valid((void *)a,sizeof(int));
__e_acsl_and_9 = __e_acsl_valid_7;
}
else __e_acsl_and_9 = 0;
if (__e_acsl_and_9) {
int __e_acsl_initialized_6;
int __e_acsl_and_10;
- __e_acsl_initialized_6 = __initialized((void *)(& b),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_6 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_6) {
int __e_acsl_valid_8;
- __e_acsl_valid_8 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_valid_8 = __valid((void *)b,sizeof(int));
__e_acsl_and_10 = __e_acsl_valid_8;
}
else __e_acsl_and_10 = 0;
@@ -425,7 +419,7 @@ int main(void)
else __e_acsl_and_11 = 0;
if (__e_acsl_and_11) {
int __e_acsl_valid_9;
- __e_acsl_valid_9 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_valid_9 = __valid((void *)X,sizeof(int));
__e_acsl_and_12 = __e_acsl_valid_9;
}
else __e_acsl_and_12 = 0;
@@ -440,22 +434,20 @@ int main(void)
int __e_acsl_and_13;
int __e_acsl_and_15;
int __e_acsl_and_16;
- __e_acsl_initialized_7 = __initialized((void *)(& a),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_7 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_7) {
int __e_acsl_valid_10;
- __e_acsl_valid_10 = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_valid_10 = __valid((void *)a,sizeof(int));
__e_acsl_and_13 = __e_acsl_valid_10;
}
else __e_acsl_and_13 = 0;
if (__e_acsl_and_13) {
int __e_acsl_initialized_8;
int __e_acsl_and_14;
- __e_acsl_initialized_8 = __initialized((void *)(& b),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_8 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_8) {
int __e_acsl_valid_11;
- __e_acsl_valid_11 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_valid_11 = __valid((void *)b,sizeof(int));
__e_acsl_and_14 = __e_acsl_valid_11;
}
else __e_acsl_and_14 = 0;
@@ -464,7 +456,7 @@ int main(void)
else __e_acsl_and_15 = 0;
if (__e_acsl_and_15) {
int __e_acsl_valid_12;
- __e_acsl_valid_12 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_valid_12 = __valid((void *)X,sizeof(int));
__e_acsl_and_16 = __e_acsl_valid_12;
}
else __e_acsl_and_16 = 0;
@@ -478,22 +470,20 @@ int main(void)
int __e_acsl_and_17;
int __e_acsl_and_19;
int __e_acsl_and_20;
- __e_acsl_initialized_9 = __initialized((void *)(& a),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_9 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_9) {
int __e_acsl_valid_13;
- __e_acsl_valid_13 = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_valid_13 = __valid((void *)a,sizeof(int));
__e_acsl_and_17 = __e_acsl_valid_13;
}
else __e_acsl_and_17 = 0;
if (__e_acsl_and_17) {
int __e_acsl_initialized_10;
int __e_acsl_and_18;
- __e_acsl_initialized_10 = __initialized((void *)(& b),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_10 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_10) {
int __e_acsl_valid_14;
- __e_acsl_valid_14 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_valid_14 = __valid((void *)b,sizeof(int));
__e_acsl_and_18 = __e_acsl_valid_14;
}
else __e_acsl_and_18 = 0;
@@ -502,7 +492,7 @@ int main(void)
else __e_acsl_and_19 = 0;
if (__e_acsl_and_19) {
int __e_acsl_valid_15;
- __e_acsl_valid_15 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_valid_15 = __valid((void *)X,sizeof(int));
__e_acsl_and_20 = __e_acsl_valid_15;
}
else __e_acsl_and_20 = 0;
@@ -517,22 +507,21 @@ int main(void)
{
int __e_acsl_initialized_11;
int __e_acsl_and_22;
- __e_acsl_initialized_11 = __initialized((void *)c,(size_t)sizeof(int *));
+ __e_acsl_initialized_11 = __initialized((void *)c,sizeof(int *));
if (__e_acsl_initialized_11) {
int __e_acsl_initialized_12;
int __e_acsl_and_21;
int __e_acsl_valid_16;
- __e_acsl_initialized_12 = __initialized((void *)(& c),
- (size_t)sizeof(int **));
+ __e_acsl_initialized_12 = __initialized((void *)(& c),sizeof(int **));
if (__e_acsl_initialized_12) {
int __e_acsl_valid_read;
- __e_acsl_valid_read = __valid_read((void *)c,(size_t)sizeof(int *));
+ __e_acsl_valid_read = __valid_read((void *)c,sizeof(int *));
__e_acsl_and_21 = __e_acsl_valid_read;
}
else __e_acsl_and_21 = 0;
e_acsl_assert(__e_acsl_and_21,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(c)",46);
- __e_acsl_valid_16 = __valid((void *)*c,(size_t)sizeof(int));
+ __e_acsl_valid_16 = __valid((void *)*c,sizeof(int));
__e_acsl_and_22 = __e_acsl_valid_16;
}
else __e_acsl_and_22 = 0;
@@ -544,52 +533,47 @@ int main(void)
int __e_acsl_valid_read_2;
int __e_acsl_initialized_13;
int __e_acsl_and_26;
- __e_acsl_valid_read_2 = __valid_read((void *)d,(size_t)sizeof(int **));
+ __e_acsl_valid_read_2 = __valid_read((void *)d,sizeof(int **));
e_acsl_assert(__e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(d)",47);
- __e_acsl_initialized_13 = __initialized((void *)*d,(size_t)sizeof(int *));
+ __e_acsl_initialized_13 = __initialized((void *)*d,sizeof(int *));
if (__e_acsl_initialized_13) {
int __e_acsl_initialized_14;
int __e_acsl_and_24;
int __e_acsl_initialized_16;
int __e_acsl_and_25;
int __e_acsl_valid_17;
- __e_acsl_initialized_14 = __initialized((void *)d,
- (size_t)sizeof(int **));
+ __e_acsl_initialized_14 = __initialized((void *)d,sizeof(int **));
if (__e_acsl_initialized_14) {
int __e_acsl_initialized_15;
int __e_acsl_and_23;
int __e_acsl_valid_read_4;
__e_acsl_initialized_15 = __initialized((void *)(& d),
- (size_t)sizeof(int ***));
+ sizeof(int ***));
if (__e_acsl_initialized_15) {
int __e_acsl_valid_read_3;
- __e_acsl_valid_read_3 = __valid_read((void *)d,
- (size_t)sizeof(int **));
+ __e_acsl_valid_read_3 = __valid_read((void *)d,sizeof(int **));
__e_acsl_and_23 = __e_acsl_valid_read_3;
}
else __e_acsl_and_23 = 0;
e_acsl_assert(__e_acsl_and_23,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(d)",47);
- __e_acsl_valid_read_4 = __valid_read((void *)*d,
- (size_t)sizeof(int *));
+ __e_acsl_valid_read_4 = __valid_read((void *)*d,sizeof(int *));
__e_acsl_and_24 = __e_acsl_valid_read_4;
}
else __e_acsl_and_24 = 0;
e_acsl_assert(__e_acsl_and_24,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(*d)",47);
- __e_acsl_initialized_16 = __initialized((void *)(& d),
- (size_t)sizeof(int ***));
+ __e_acsl_initialized_16 = __initialized((void *)(& d),sizeof(int ***));
if (__e_acsl_initialized_16) {
int __e_acsl_valid_read_5;
- __e_acsl_valid_read_5 = __valid_read((void *)d,
- (size_t)sizeof(int **));
+ __e_acsl_valid_read_5 = __valid_read((void *)d,sizeof(int **));
__e_acsl_and_25 = __e_acsl_valid_read_5;
}
else __e_acsl_and_25 = 0;
e_acsl_assert(__e_acsl_and_25,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(d)",47);
- __e_acsl_valid_17 = __valid((void *)*(*d),(size_t)sizeof(int));
+ __e_acsl_valid_17 = __valid((void *)*(*d),sizeof(int));
__e_acsl_and_26 = __e_acsl_valid_17;
}
else __e_acsl_and_26 = 0;
@@ -603,22 +587,20 @@ int main(void)
int __e_acsl_and_27;
int __e_acsl_and_29;
int __e_acsl_and_30;
- __e_acsl_initialized_17 = __initialized((void *)(& a),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_17 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_17) {
int __e_acsl_valid_18;
- __e_acsl_valid_18 = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_valid_18 = __valid((void *)a,sizeof(int));
__e_acsl_and_27 = __e_acsl_valid_18;
}
else __e_acsl_and_27 = 0;
if (! __e_acsl_and_27) {
int __e_acsl_initialized_18;
int __e_acsl_and_28;
- __e_acsl_initialized_18 = __initialized((void *)(& b),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_18 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_18) {
int __e_acsl_valid_19;
- __e_acsl_valid_19 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_valid_19 = __valid((void *)b,sizeof(int));
__e_acsl_and_28 = __e_acsl_valid_19;
}
else __e_acsl_and_28 = 0;
@@ -627,7 +609,7 @@ int main(void)
else __e_acsl_and_29 = 0;
if (__e_acsl_and_29) {
int __e_acsl_valid_20;
- __e_acsl_valid_20 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_valid_20 = __valid((void *)X,sizeof(int));
__e_acsl_and_30 = __e_acsl_valid_20;
}
else __e_acsl_and_30 = 0;
@@ -637,7 +619,7 @@ int main(void)
/*@ assert \valid(&Z); */
{
int __e_acsl_valid_21;
- __e_acsl_valid_21 = __valid((void *)(& Z),(size_t)sizeof(int));
+ __e_acsl_valid_21 = __valid((void *)(& Z),sizeof(int));
e_acsl_assert(__e_acsl_valid_21,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&Z)",50);
}
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 6b7354a356dbad21526e2603c23c3dbc97711008..d6f5642b29065594aba77fcb0f93eb2cdb6cd9fd 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
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -147,7 +147,7 @@ extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),8U);
+ __store_block((void *)(& __retres),8UL);
__retres = __malloc(size);
__delete_block((void *)(& __retres));
return __retres;
@@ -175,8 +175,8 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __store_block((void *)(& p),8U);
- __store_block((void *)(& __e_acsl_at),4U);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(& __e_acsl_at),4UL);
__e_acsl_at = p != (void *)0;
__free(p);
__delete_block((void *)(& p));
@@ -195,16 +195,16 @@ int Z;
int *f(int *x)
{
int *y;
- __store_block((void *)(& y),8U);
+ __store_block((void *)(& y),8UL);
/*@ assert ¬\valid(y); */
{
int __e_acsl_initialized;
int __e_acsl_and;
- __store_block((void *)(& x),8U);
- __e_acsl_initialized = __initialized((void *)(& y),(size_t)sizeof(int *));
+ __store_block((void *)(& x),8UL);
+ __e_acsl_initialized = __initialized((void *)(& y),sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = __valid((void *)y,(size_t)sizeof(int));
+ __e_acsl_valid = __valid((void *)y,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else __e_acsl_and = 0;
@@ -216,7 +216,7 @@ int *f(int *x)
/*@ assert \valid(x); */
{
int __e_acsl_valid_2;
- __e_acsl_valid_2 = __valid((void *)x,(size_t)sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)x,sizeof(int));
e_acsl_assert(__e_acsl_valid_2,(char *)"Assertion",(char *)"f",
(char *)"\\valid(x)",21);
}
@@ -230,18 +230,18 @@ int *f(int *x)
int *__e_acsl_f(int *x)
{
int *__retres;
- __store_block((void *)(& __retres),8U);
+ __store_block((void *)(& __retres),8UL);
{
int __e_acsl_valid;
- __store_block((void *)(& x),8U);
- __e_acsl_valid = __valid((void *)x,(size_t)sizeof(int));
+ __store_block((void *)(& x),8UL);
+ __e_acsl_valid = __valid((void *)x,sizeof(int));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"f",
(char *)"\\valid(x)",15);
__retres = f(x);
}
{
int __e_acsl_valid_2;
- __e_acsl_valid_2 = __valid((void *)__retres,(size_t)sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)__retres,sizeof(int));
e_acsl_assert(__e_acsl_valid_2,(char *)"Postcondition",(char *)"f",
(char *)"\\valid(\\result)",16);
__delete_block((void *)(& x));
@@ -255,9 +255,9 @@ void g(void)
int m;
int *u;
int **p;
- __store_block((void *)(& p),8U);
- __store_block((void *)(& u),8U);
- __store_block((void *)(& m),4U);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(& u),8UL);
+ __store_block((void *)(& m),4UL);
__full_init((void *)(& p));
p = & u;
__full_init((void *)(& u));
@@ -268,22 +268,21 @@ void g(void)
{
int __e_acsl_initialized;
int __e_acsl_and_2;
- __e_acsl_initialized = __initialized((void *)p,(size_t)sizeof(int *));
+ __e_acsl_initialized = __initialized((void *)p,sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_initialized_2;
int __e_acsl_and;
int __e_acsl_valid;
- __e_acsl_initialized_2 = __initialized((void *)(& p),
- (size_t)sizeof(int **));
+ __e_acsl_initialized_2 = __initialized((void *)(& p),sizeof(int **));
if (__e_acsl_initialized_2) {
int __e_acsl_valid_read;
- __e_acsl_valid_read = __valid_read((void *)p,(size_t)sizeof(int *));
+ __e_acsl_valid_read = __valid_read((void *)p,sizeof(int *));
__e_acsl_and = __e_acsl_valid_read;
}
else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(p)",30);
- __e_acsl_valid = __valid((void *)*p,(size_t)sizeof(int));
+ __e_acsl_valid = __valid((void *)*p,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid;
}
else __e_acsl_and_2 = 0;
@@ -298,8 +297,8 @@ void g(void)
void __e_acsl_memory_init(void)
{
- __store_block((void *)(& Z),4U);
- __store_block((void *)(& X),8U);
+ __store_block((void *)(& Z),4UL);
+ __store_block((void *)(& X),8UL);
return;
}
@@ -312,11 +311,11 @@ int main(void)
int ***d;
int n;
__e_acsl_memory_init();
- __store_block((void *)(& n),4U);
- __store_block((void *)(& d),8U);
- __store_block((void *)(& c),8U);
- __store_block((void *)(& b),8U);
- __store_block((void *)(& a),8U);
+ __store_block((void *)(& n),4UL);
+ __store_block((void *)(& d),8UL);
+ __store_block((void *)(& c),8UL);
+ __store_block((void *)(& b),8UL);
+ __store_block((void *)(& a),8UL);
__full_init((void *)(& n));
n = 0;
/*@ assert (¬\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
@@ -325,21 +324,20 @@ int main(void)
int __e_acsl_and;
int __e_acsl_and_3;
int __e_acsl_and_4;
- __e_acsl_initialized = __initialized((void *)(& a),(size_t)sizeof(int *));
+ __e_acsl_initialized = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_valid = __valid((void *)a,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else __e_acsl_and = 0;
if (! __e_acsl_and) {
int __e_acsl_initialized_2;
int __e_acsl_and_2;
- __e_acsl_initialized_2 = __initialized((void *)(& b),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_2 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_2) {
int __e_acsl_valid_2;
- __e_acsl_valid_2 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)b,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_2;
}
else __e_acsl_and_2 = 0;
@@ -348,7 +346,7 @@ int main(void)
else __e_acsl_and_3 = 0;
if (__e_acsl_and_3) {
int __e_acsl_valid_3;
- __e_acsl_valid_3 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_valid_3 = __valid((void *)X,sizeof(int));
__e_acsl_and_4 = ! __e_acsl_valid_3;
}
else __e_acsl_and_4 = 0;
@@ -356,29 +354,27 @@ int main(void)
(char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",35);
}
__full_init((void *)(& a));
- a = (int *)__e_acsl_malloc((unsigned int)sizeof(int));
+ a = (int *)__e_acsl_malloc(sizeof(int));
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
{
int __e_acsl_initialized_3;
int __e_acsl_and_5;
int __e_acsl_and_7;
int __e_acsl_and_8;
- __e_acsl_initialized_3 = __initialized((void *)(& a),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_3 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_3) {
int __e_acsl_valid_4;
- __e_acsl_valid_4 = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_valid_4 = __valid((void *)a,sizeof(int));
__e_acsl_and_5 = __e_acsl_valid_4;
}
else __e_acsl_and_5 = 0;
if (__e_acsl_and_5) {
int __e_acsl_initialized_4;
int __e_acsl_and_6;
- __e_acsl_initialized_4 = __initialized((void *)(& b),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_4 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_4) {
int __e_acsl_valid_5;
- __e_acsl_valid_5 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_valid_5 = __valid((void *)b,sizeof(int));
__e_acsl_and_6 = __e_acsl_valid_5;
}
else __e_acsl_and_6 = 0;
@@ -387,7 +383,7 @@ int main(void)
else __e_acsl_and_7 = 0;
if (__e_acsl_and_7) {
int __e_acsl_valid_6;
- __e_acsl_valid_6 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_valid_6 = __valid((void *)X,sizeof(int));
__e_acsl_and_8 = ! __e_acsl_valid_6;
}
else __e_acsl_and_8 = 0;
@@ -401,22 +397,20 @@ int main(void)
int __e_acsl_and_9;
int __e_acsl_and_11;
int __e_acsl_and_12;
- __e_acsl_initialized_5 = __initialized((void *)(& a),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_5 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_5) {
int __e_acsl_valid_7;
- __e_acsl_valid_7 = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_valid_7 = __valid((void *)a,sizeof(int));
__e_acsl_and_9 = __e_acsl_valid_7;
}
else __e_acsl_and_9 = 0;
if (__e_acsl_and_9) {
int __e_acsl_initialized_6;
int __e_acsl_and_10;
- __e_acsl_initialized_6 = __initialized((void *)(& b),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_6 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_6) {
int __e_acsl_valid_8;
- __e_acsl_valid_8 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_valid_8 = __valid((void *)b,sizeof(int));
__e_acsl_and_10 = __e_acsl_valid_8;
}
else __e_acsl_and_10 = 0;
@@ -425,7 +419,7 @@ int main(void)
else __e_acsl_and_11 = 0;
if (__e_acsl_and_11) {
int __e_acsl_valid_9;
- __e_acsl_valid_9 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_valid_9 = __valid((void *)X,sizeof(int));
__e_acsl_and_12 = __e_acsl_valid_9;
}
else __e_acsl_and_12 = 0;
@@ -440,22 +434,20 @@ int main(void)
int __e_acsl_and_13;
int __e_acsl_and_15;
int __e_acsl_and_16;
- __e_acsl_initialized_7 = __initialized((void *)(& a),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_7 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_7) {
int __e_acsl_valid_10;
- __e_acsl_valid_10 = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_valid_10 = __valid((void *)a,sizeof(int));
__e_acsl_and_13 = __e_acsl_valid_10;
}
else __e_acsl_and_13 = 0;
if (__e_acsl_and_13) {
int __e_acsl_initialized_8;
int __e_acsl_and_14;
- __e_acsl_initialized_8 = __initialized((void *)(& b),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_8 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_8) {
int __e_acsl_valid_11;
- __e_acsl_valid_11 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_valid_11 = __valid((void *)b,sizeof(int));
__e_acsl_and_14 = __e_acsl_valid_11;
}
else __e_acsl_and_14 = 0;
@@ -464,7 +456,7 @@ int main(void)
else __e_acsl_and_15 = 0;
if (__e_acsl_and_15) {
int __e_acsl_valid_12;
- __e_acsl_valid_12 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_valid_12 = __valid((void *)X,sizeof(int));
__e_acsl_and_16 = __e_acsl_valid_12;
}
else __e_acsl_and_16 = 0;
@@ -478,22 +470,20 @@ int main(void)
int __e_acsl_and_17;
int __e_acsl_and_19;
int __e_acsl_and_20;
- __e_acsl_initialized_9 = __initialized((void *)(& a),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_9 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_9) {
int __e_acsl_valid_13;
- __e_acsl_valid_13 = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_valid_13 = __valid((void *)a,sizeof(int));
__e_acsl_and_17 = __e_acsl_valid_13;
}
else __e_acsl_and_17 = 0;
if (__e_acsl_and_17) {
int __e_acsl_initialized_10;
int __e_acsl_and_18;
- __e_acsl_initialized_10 = __initialized((void *)(& b),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_10 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_10) {
int __e_acsl_valid_14;
- __e_acsl_valid_14 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_valid_14 = __valid((void *)b,sizeof(int));
__e_acsl_and_18 = __e_acsl_valid_14;
}
else __e_acsl_and_18 = 0;
@@ -502,7 +492,7 @@ int main(void)
else __e_acsl_and_19 = 0;
if (__e_acsl_and_19) {
int __e_acsl_valid_15;
- __e_acsl_valid_15 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_valid_15 = __valid((void *)X,sizeof(int));
__e_acsl_and_20 = __e_acsl_valid_15;
}
else __e_acsl_and_20 = 0;
@@ -517,22 +507,21 @@ int main(void)
{
int __e_acsl_initialized_11;
int __e_acsl_and_22;
- __e_acsl_initialized_11 = __initialized((void *)c,(size_t)sizeof(int *));
+ __e_acsl_initialized_11 = __initialized((void *)c,sizeof(int *));
if (__e_acsl_initialized_11) {
int __e_acsl_initialized_12;
int __e_acsl_and_21;
int __e_acsl_valid_16;
- __e_acsl_initialized_12 = __initialized((void *)(& c),
- (size_t)sizeof(int **));
+ __e_acsl_initialized_12 = __initialized((void *)(& c),sizeof(int **));
if (__e_acsl_initialized_12) {
int __e_acsl_valid_read;
- __e_acsl_valid_read = __valid_read((void *)c,(size_t)sizeof(int *));
+ __e_acsl_valid_read = __valid_read((void *)c,sizeof(int *));
__e_acsl_and_21 = __e_acsl_valid_read;
}
else __e_acsl_and_21 = 0;
e_acsl_assert(__e_acsl_and_21,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(c)",46);
- __e_acsl_valid_16 = __valid((void *)*c,(size_t)sizeof(int));
+ __e_acsl_valid_16 = __valid((void *)*c,sizeof(int));
__e_acsl_and_22 = __e_acsl_valid_16;
}
else __e_acsl_and_22 = 0;
@@ -544,52 +533,47 @@ int main(void)
int __e_acsl_valid_read_2;
int __e_acsl_initialized_13;
int __e_acsl_and_26;
- __e_acsl_valid_read_2 = __valid_read((void *)d,(size_t)sizeof(int **));
+ __e_acsl_valid_read_2 = __valid_read((void *)d,sizeof(int **));
e_acsl_assert(__e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(d)",47);
- __e_acsl_initialized_13 = __initialized((void *)*d,(size_t)sizeof(int *));
+ __e_acsl_initialized_13 = __initialized((void *)*d,sizeof(int *));
if (__e_acsl_initialized_13) {
int __e_acsl_initialized_14;
int __e_acsl_and_24;
int __e_acsl_initialized_16;
int __e_acsl_and_25;
int __e_acsl_valid_17;
- __e_acsl_initialized_14 = __initialized((void *)d,
- (size_t)sizeof(int **));
+ __e_acsl_initialized_14 = __initialized((void *)d,sizeof(int **));
if (__e_acsl_initialized_14) {
int __e_acsl_initialized_15;
int __e_acsl_and_23;
int __e_acsl_valid_read_4;
__e_acsl_initialized_15 = __initialized((void *)(& d),
- (size_t)sizeof(int ***));
+ sizeof(int ***));
if (__e_acsl_initialized_15) {
int __e_acsl_valid_read_3;
- __e_acsl_valid_read_3 = __valid_read((void *)d,
- (size_t)sizeof(int **));
+ __e_acsl_valid_read_3 = __valid_read((void *)d,sizeof(int **));
__e_acsl_and_23 = __e_acsl_valid_read_3;
}
else __e_acsl_and_23 = 0;
e_acsl_assert(__e_acsl_and_23,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(d)",47);
- __e_acsl_valid_read_4 = __valid_read((void *)*d,
- (size_t)sizeof(int *));
+ __e_acsl_valid_read_4 = __valid_read((void *)*d,sizeof(int *));
__e_acsl_and_24 = __e_acsl_valid_read_4;
}
else __e_acsl_and_24 = 0;
e_acsl_assert(__e_acsl_and_24,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(*d)",47);
- __e_acsl_initialized_16 = __initialized((void *)(& d),
- (size_t)sizeof(int ***));
+ __e_acsl_initialized_16 = __initialized((void *)(& d),sizeof(int ***));
if (__e_acsl_initialized_16) {
int __e_acsl_valid_read_5;
- __e_acsl_valid_read_5 = __valid_read((void *)d,
- (size_t)sizeof(int **));
+ __e_acsl_valid_read_5 = __valid_read((void *)d,sizeof(int **));
__e_acsl_and_25 = __e_acsl_valid_read_5;
}
else __e_acsl_and_25 = 0;
e_acsl_assert(__e_acsl_and_25,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(d)",47);
- __e_acsl_valid_17 = __valid((void *)*(*d),(size_t)sizeof(int));
+ __e_acsl_valid_17 = __valid((void *)*(*d),sizeof(int));
__e_acsl_and_26 = __e_acsl_valid_17;
}
else __e_acsl_and_26 = 0;
@@ -603,22 +587,20 @@ int main(void)
int __e_acsl_and_27;
int __e_acsl_and_29;
int __e_acsl_and_30;
- __e_acsl_initialized_17 = __initialized((void *)(& a),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_17 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_17) {
int __e_acsl_valid_18;
- __e_acsl_valid_18 = __valid((void *)a,(size_t)sizeof(int));
+ __e_acsl_valid_18 = __valid((void *)a,sizeof(int));
__e_acsl_and_27 = __e_acsl_valid_18;
}
else __e_acsl_and_27 = 0;
if (! __e_acsl_and_27) {
int __e_acsl_initialized_18;
int __e_acsl_and_28;
- __e_acsl_initialized_18 = __initialized((void *)(& b),
- (size_t)sizeof(int *));
+ __e_acsl_initialized_18 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_18) {
int __e_acsl_valid_19;
- __e_acsl_valid_19 = __valid((void *)b,(size_t)sizeof(int));
+ __e_acsl_valid_19 = __valid((void *)b,sizeof(int));
__e_acsl_and_28 = __e_acsl_valid_19;
}
else __e_acsl_and_28 = 0;
@@ -627,7 +609,7 @@ int main(void)
else __e_acsl_and_29 = 0;
if (__e_acsl_and_29) {
int __e_acsl_valid_20;
- __e_acsl_valid_20 = __valid((void *)X,(size_t)sizeof(int));
+ __e_acsl_valid_20 = __valid((void *)X,sizeof(int));
__e_acsl_and_30 = __e_acsl_valid_20;
}
else __e_acsl_and_30 = 0;
@@ -637,7 +619,7 @@ int main(void)
/*@ assert \valid(&Z); */
{
int __e_acsl_valid_21;
- __e_acsl_valid_21 = __valid((void *)(& Z),(size_t)sizeof(int));
+ __e_acsl_valid_21 = __valid((void *)(& Z),sizeof(int));
e_acsl_assert(__e_acsl_valid_21,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&Z)",50);
}