From f3500fa5e041fad514c3fc58317c63be24e76f92 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 7 Feb 2018 10:37:51 +0100
Subject: [PATCH] fix typing in presence of comparison operators (gitlab issue
49)
---
src/plugins/e-acsl/doc/Changelog | 4 +
.../e-acsl/tests/bts/oracle/gen_bts1307.c | 10 +-
src/plugins/e-acsl/tests/gmp/cast.i | 2 +-
.../e-acsl/tests/gmp/oracle/gen_arith.c | 29 +++--
.../e-acsl/tests/gmp/oracle/gen_comparison.c | 37 +++---
.../tests/gmp/oracle/gen_integer_constant.c | 9 +-
.../tests/runtime/oracle/gen_block_length.c | 18 +--
.../runtime/oracle/gen_function_contract.c | 6 +-
.../e-acsl/tests/runtime/oracle/gen_lazy.c | 6 +-
.../tests/runtime/oracle/gen_literal_string.c | 4 +-
.../tests/runtime/oracle/gen_mainargs.c | 4 +-
.../tests/runtime/oracle/gen_memalign.c | 8 +-
.../e-acsl/tests/runtime/oracle/gen_offset.c | 107 +++++++++++-------
.../runtime/oracle/gen_other_constants.c | 4 +-
.../e-acsl/tests/runtime/oracle/gen_ptr.c | 10 +-
.../e-acsl/tests/runtime/oracle/gen_sizeof.c | 2 +-
.../tests/runtime/oracle/gen_stmt_contract.c | 4 +-
.../e-acsl/tests/runtime/oracle/gen_typedef.c | 4 +-
.../tests/special/oracle/gen_e-acsl-valid.c | 10 +-
.../tests/special/oracle/gen_e-acsl-valid2.c | 4 +-
.../tests/temporal/oracle/gen_t_getenv.c | 4 +-
src/plugins/e-acsl/translate.ml | 2 +-
22 files changed, 150 insertions(+), 138 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 300ebb5fd7d..6708ab84cec 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,6 +19,10 @@
# configure configure
###############################################################################
+-* E-ACSL [2018/02/07] Fix incorrect typing in presence of
+ comparison operators (may only be visible when directly
+ analyzing the E-ACSL's generated code with Frama-C without
+ pretty-printing it).
-* runtime [2018/01/30] E-ACSL aborted when run on a machine with a
low hard limit on the stack size.
-* E-ACSL [2018/01/08] Fix a crash when translating a postcondition
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index bf5e66ec057..0f4ad92032f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -156,7 +156,7 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_3)",
23);
- __gen_e_acsl_and = *__gen_e_acsl_at_3 < 0.85 * *__gen_e_acsl_at_4;
+ __gen_e_acsl_and = (long double)*__gen_e_acsl_at_3 < 0.85 * *__gen_e_acsl_at_4;
}
else __gen_e_acsl_and = 0;
if (__gen_e_acsl_and) {
@@ -168,7 +168,7 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_5)",
23);
- __gen_e_acsl_if = *__gen_e_acsl_at_5 != 0.;
+ __gen_e_acsl_if = (long double)*__gen_e_acsl_at_5 != 0.;
}
else {
int __gen_e_acsl_valid_read_6;
@@ -254,9 +254,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
(void *)(& __gen_e_acsl_at));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"foo",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at)",11);
- __e_acsl_assert(*__gen_e_acsl_at == *__gen_e_acsl_at_2 + ((long double)5 -
- ((long double)(
- 5 / 80) * *__gen_e_acsl_at_3) * 0.4),
+ __e_acsl_assert((long double)*__gen_e_acsl_at == *__gen_e_acsl_at_2 + (
+ (long double)5 -
+ ((long double)0 * *__gen_e_acsl_at_3) * 0.4),
(char *)"Postcondition",(char *)"foo",
(char *)"*\\old(Mtmax_out) == *\\old(Mtmax_in) + (5 - ((5 / 80) * *\\old(Mwmax)) * 0.4)",
11);
diff --git a/src/plugins/e-acsl/tests/gmp/cast.i b/src/plugins/e-acsl/tests/gmp/cast.i
index 3b014c861ad..700d338841e 100644
--- a/src/plugins/e-acsl/tests/gmp/cast.i
+++ b/src/plugins/e-acsl/tests/gmp/cast.i
@@ -20,7 +20,7 @@ int main(void) {
/* heterogeneous casts from/to integers */
int t[2] = { 0, 1 };
- /*@ assert (float)x == (float)t[(int)0.1]; */
+ /*@ assert (float)x == t[(int)0.1]; */
return 0;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
index a3079f4d26d..1ba870b526f 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
@@ -14,16 +14,15 @@ int main(void)
__e_acsl_assert(x == -3,(char *)"Assertion",(char *)"main",
(char *)"x == -3",11);
/*@ assert 0 ≢ ~0; */
- __e_acsl_assert(0 != ~ 0,(char *)"Assertion",(char *)"main",
- (char *)"0 != ~0",12);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"0 != ~0",12);
/*@ assert x + 1 ≡ -2; */
- __e_acsl_assert(x + 1L == -2,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(x + 1L == -2L,(char *)"Assertion",(char *)"main",
(char *)"x + 1 == -2",14);
/*@ assert x - 1 ≡ -4; */
- __e_acsl_assert(x - 1L == -4,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(x - 1L == -4L,(char *)"Assertion",(char *)"main",
(char *)"x - 1 == -4",15);
/*@ assert x * 3 ≡ -9; */
- __e_acsl_assert(x * 3L == -9,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(x * 3L == -9L,(char *)"Assertion",(char *)"main",
(char *)"x * 3 == -9",16);
/*@ assert x / 3 ≡ -1; */
__e_acsl_assert(x / 3 == -1,(char *)"Assertion",(char *)"main",
@@ -48,7 +47,7 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
__gen_e_acsl__3 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_div));
- __e_acsl_assert(__gen_e_acsl__3 == 1,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(__gen_e_acsl__3 == 1L,(char *)"Assertion",(char *)"main",
(char *)"0xffffffffffffffffffffff / 0xffffffffffffffffffffff == 1",
18);
__gmpz_clear(__gen_e_acsl_);
@@ -59,29 +58,29 @@ int main(void)
__e_acsl_assert(x % 2 == -1,(char *)"Assertion",(char *)"main",
(char *)"x % 2 == -1",19);
/*@ assert -3 % -2 ≡ -1; */
- __e_acsl_assert(-3 % -2 == -1,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"-3 % -2 == -1",20);
/*@ assert 3 % -2 ≡ 1; */
- __e_acsl_assert(3 % -2 == 1,(char *)"Assertion",(char *)"main",
- (char *)"3 % -2 == 1",21);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"3 % -2 == 1",
+ 21);
/*@ assert ((x * 2 + (3 + y)) - 4) + (x - y) ≡ -10; */
- __e_acsl_assert(((x * 2L + (3L + y)) - 4L) + (x - (long)y) == -10,
+ __e_acsl_assert(((x * 2L + (3L + y)) - 4L) + (x - (long)y) == -10L,
(char *)"Assertion",(char *)"main",
(char *)"((x * 2 + (3 + y)) - 4) + (x - y) == -10",23);
/*@ assert (0 ≡ 1) ≡ !(0 ≡ 0); */
- __e_acsl_assert((0 == 1) == ! (0 == 0),(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 == 1) == !(0 == 0)",25);
/*@ assert (0 ≤ -1) ≡ (0 > 0); */
- __e_acsl_assert((0 <= -1) == (0 > 0),(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 <= -1) == (0 > 0)",26);
/*@ assert (0 ≥ -1) ≡ (0 ≤ 0); */
- __e_acsl_assert((0 >= -1) == (0 <= 0),(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 >= -1) == (0 <= 0)",27);
/*@ assert (0 ≢ 1) ≡ !(0 ≢ 0); */
- __e_acsl_assert((0 != 1) == ! (0 != 0),(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 != 1) == !(0 != 0)",28);
/*@ assert (0 ≢ 0) ≡ !(1 ≢ 0); */
- __e_acsl_assert((0 != 0) == ! (1 != 0),(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 != 0) == !(1 != 0)",30);
/*@ assert 4 / y ≡ 2; */
{
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
index 595ba4cc19b..edf356731d4 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
@@ -21,41 +21,34 @@ int main(void)
__e_acsl_assert(s == s,(char *)"Assertion",(char *)"main",(char *)"s == s",
12);
/*@ assert 5 < 18; */
- __e_acsl_assert(5 < 18,(char *)"Assertion",(char *)"main",(char *)"5 < 18",
- 15);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"5 < 18",15);
/*@ assert 32 > 3; */
- __e_acsl_assert(32 > 3,(char *)"Assertion",(char *)"main",(char *)"32 > 3",
- 16);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"32 > 3",16);
/*@ assert 12 ≤ 13; */
- __e_acsl_assert(12 <= 13,(char *)"Assertion",(char *)"main",
- (char *)"12 <= 13",17);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"12 <= 13",17);
/*@ assert 123 ≥ 12; */
- __e_acsl_assert(123 >= 12,(char *)"Assertion",(char *)"main",
- (char *)"123 >= 12",18);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"123 >= 12",
+ 18);
/*@ assert 0xff ≡ 0xff; */
- __e_acsl_assert(255 == 255,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"0xff == 0xff",19);
/*@ assert 1 ≢ 2; */
- __e_acsl_assert(1 != 2,(char *)"Assertion",(char *)"main",(char *)"1 != 2",
- 20);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"1 != 2",20);
/*@ assert -5 < 18; */
- __e_acsl_assert(-5 < 18,(char *)"Assertion",(char *)"main",
- (char *)"-5 < 18",22);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"-5 < 18",22);
/*@ assert 32 > -3; */
- __e_acsl_assert(32 > -3,(char *)"Assertion",(char *)"main",
- (char *)"32 > -3",23);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"32 > -3",23);
/*@ assert -12 ≤ 13; */
- __e_acsl_assert(-12 <= 13,(char *)"Assertion",(char *)"main",
- (char *)"-12 <= 13",24);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"-12 <= 13",
+ 24);
/*@ assert 123 ≥ -12; */
- __e_acsl_assert(123 >= -12,(char *)"Assertion",(char *)"main",
- (char *)"123 >= -12",25);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"123 >= -12",
+ 25);
/*@ assert -0xff ≡ -0xff; */
- __e_acsl_assert(-255 == -255,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"-0xff == -0xff",26);
/*@ assert 1 ≢ -2; */
- __e_acsl_assert(1 != -2,(char *)"Assertion",(char *)"main",
- (char *)"1 != -2",27);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"1 != -2",27);
__retres = 0;
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
index e8121408525..82bfb1661fa 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
@@ -6,16 +6,13 @@ int main(void)
int x;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
/*@ assert 0 ≡ 0; */
- __e_acsl_assert(0 == 0,(char *)"Assertion",(char *)"main",(char *)"0 == 0",
- 6);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"0 == 0",6);
x = 0;
x ++;
/*@ assert 0 ≢ 1; */
- __e_acsl_assert(0 != 1,(char *)"Assertion",(char *)"main",(char *)"0 != 1",
- 8);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"0 != 1",8);
/*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */
- __e_acsl_assert(1152921504606846975UL == 1152921504606846975UL,
- (char *)"Assertion",(char *)"main",
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"1152921504606846975 == 0xfffffffffffffff",9);
/*@ assert
0xffffffffffffffffffffffffffffffff ≡
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
index ff65273e6fd..1917ddc0bc4 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
@@ -43,7 +43,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_3;
__gen_e_acsl_block_length_3 = __e_acsl_block_length((void *)(A));
- __e_acsl_assert(__gen_e_acsl_block_length_3 == 16,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_block_length_3 == 16UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length((int *)A) == sizeof(A)",20);
}
@@ -51,7 +51,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_4;
__gen_e_acsl_block_length_4 = __e_acsl_block_length((void *)(& A[3]));
- __e_acsl_assert(__gen_e_acsl_block_length_4 == 16,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_block_length_4 == 16UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(&A[3]) == sizeof(A)",21);
}
@@ -59,7 +59,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_5;
__gen_e_acsl_block_length_5 = __e_acsl_block_length((void *)PA);
- __e_acsl_assert(__gen_e_acsl_block_length_5 == 16,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_block_length_5 == 16UL,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(PA) == sizeof(A)",
22);
}
@@ -85,7 +85,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_8;
__gen_e_acsl_block_length_8 = __e_acsl_block_length((void *)(a));
- __e_acsl_assert(__gen_e_acsl_block_length_8 == 16,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_block_length_8 == 16UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length((int *)a) == sizeof(a)",29);
}
@@ -93,7 +93,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_9;
__gen_e_acsl_block_length_9 = __e_acsl_block_length((void *)(& a[3]));
- __e_acsl_assert(__gen_e_acsl_block_length_9 == 16,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_block_length_9 == 16UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(&a[3]) == sizeof(a)",30);
}
@@ -101,7 +101,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_10;
__gen_e_acsl_block_length_10 = __e_acsl_block_length((void *)pa);
- __e_acsl_assert(__gen_e_acsl_block_length_10 == 16,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_block_length_10 == 16UL,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(pa) == sizeof(a)",
31);
}
@@ -128,7 +128,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_13;
__gen_e_acsl_block_length_13 = __e_acsl_block_length((void *)(& l));
- __e_acsl_assert(__gen_e_acsl_block_length_13 == 8,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_block_length_13 == 8UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(&l) == sizeof(long)",39);
}
@@ -136,7 +136,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_14;
__gen_e_acsl_block_length_14 = __e_acsl_block_length((void *)pl);
- __e_acsl_assert(__gen_e_acsl_block_length_14 == 8,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_block_length_14 == 8UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(pl) == sizeof(long)",40);
}
@@ -144,7 +144,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_15;
__gen_e_acsl_block_length_15 = __e_acsl_block_length((void *)(pl + 7));
- __e_acsl_assert(__gen_e_acsl_block_length_15 == 8,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_block_length_15 == 8UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(pl + 7) == sizeof(long)",41);
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
index b8b425b657a..4004a193720 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
@@ -219,7 +219,7 @@ void __gen_e_acsl_m(void)
(char *)"m",(char *)"\\old(X == 5 && Y == 2) ==> X == 7",
60);
if (! __gen_e_acsl_at_3) __gen_e_acsl_implies_3 = 1;
- else __gen_e_acsl_implies_3 = X == __gen_e_acsl_at_4 + Y;
+ else __gen_e_acsl_implies_3 = (long)X == __gen_e_acsl_at_4 + Y;
__e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Postcondition",
(char *)"m",
(char *)"\\old(X == 5 && Y == 2) ==> X == \\old(X) + Y",
@@ -288,14 +288,14 @@ void __gen_e_acsl_j(void)
{
__e_acsl_assert(X == 5,(char *)"Precondition",(char *)"j",(char *)"X == 5",
27);
- __e_acsl_assert(X == 3L + Y,(char *)"Precondition",(char *)"j",
+ __e_acsl_assert((long)X == 3L + Y,(char *)"Precondition",(char *)"j",
(char *)"X == 3 + Y",30);
__e_acsl_assert(Y == 2,(char *)"Precondition",(char *)"j",(char *)"Y == 2",
31);
j();
__e_acsl_assert(X == 3,(char *)"Postcondition",(char *)"j",
(char *)"X == 3",28);
- __e_acsl_assert(X == Y + 1L,(char *)"Postcondition",(char *)"j",
+ __e_acsl_assert((long)X == Y + 1L,(char *)"Postcondition",(char *)"j",
(char *)"X == Y + 1",32);
return;
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c
index 74f7527423e..3af362c97eb 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c
@@ -17,7 +17,7 @@ int main(void)
{
int __gen_e_acsl_and_2;
if (x != 0) {
- __e_acsl_assert(0 != 0,(char *)"RTE",(char *)"main",
+ __e_acsl_assert(0,(char *)"RTE",(char *)"main",
(char *)"division_by_zero: 0 != 0",10);
__gen_e_acsl_and_2 = y == 1 / 0;
}
@@ -37,7 +37,7 @@ int main(void)
int __gen_e_acsl_or_2;
if (x == 0) __gen_e_acsl_or_2 = 1;
else {
- __e_acsl_assert(0 != 0,(char *)"RTE",(char *)"main",
+ __e_acsl_assert(0,(char *)"RTE",(char *)"main",
(char *)"division_by_zero: 0 != 0",12);
__gen_e_acsl_or_2 = y == 1 / 0;
}
@@ -57,7 +57,7 @@ int main(void)
int __gen_e_acsl_implies_2;
if (! (x == 1)) __gen_e_acsl_implies_2 = 1;
else {
- __e_acsl_assert(0 != 0,(char *)"RTE",(char *)"main",
+ __e_acsl_assert(0,(char *)"RTE",(char *)"main",
(char *)"division_by_zero: 0 != 0",14);
__gen_e_acsl_implies_2 = y == 1 / 0;
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
index 54dc8baee65..38d06675846 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
@@ -20,7 +20,7 @@ void f(void)
(void *)(& T));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
(char *)"mem_access: \\valid_read(T + G)",11);
- __e_acsl_assert(*(T + G) == 'b',(char *)"Assertion",(char *)"f",
+ __e_acsl_assert((int)*(T + G) == 98,(char *)"Assertion",(char *)"f",
(char *)"*(T + G) == \'b\'",11);
}
G ++;
@@ -91,7 +91,7 @@ int main(void)
(void *)(& S));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(S + G2)",25);
- __e_acsl_assert(*(S + G2) == 'o',(char *)"Assertion",(char *)"main",
+ __e_acsl_assert((int)*(S + G2) == 111,(char *)"Assertion",(char *)"main",
(char *)"*(S + G2) == \'o\'",25);
}
/*@ assert \initialized(S); */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
index d86edf694ff..1da969d8f52 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
@@ -63,7 +63,7 @@ int __gen_e_acsl_main(int argc, char **argv)
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(argv + argc)",15);
/*@ assert Value: mem_access: \valid_read(argv + argc); */
- __e_acsl_assert(*(argv + argc) == (void *)0,(char *)"Assertion",
+ __e_acsl_assert(*(argv + argc) == (char *)0,(char *)"Assertion",
(char *)"main",(char *)"*(argv + argc) == \\null",15);
}
/*@ assert ¬\valid(*(argv + argc)); */
@@ -131,7 +131,7 @@ int __gen_e_acsl_main(int argc, char **argv)
__gen_e_acsl_forall_2 = 1;
__gen_e_acsl_k_2 = 0;
while (1) {
- if (__gen_e_acsl_k_2 <= len) ; else break;
+ if (__gen_e_acsl_k_2 <= (long)len) ; else break;
{
int __gen_e_acsl_valid_read_4;
int __gen_e_acsl_valid_4;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
index f1b95b483bb..7e1ad93c3b7 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
@@ -66,22 +66,22 @@ int main(int argc, char const **argv)
__e_acsl_full_init((void *)(& a));
a = (char *)aligned_alloc((unsigned long)256,(unsigned long)12);
/*@ assert a ≡ \null; */
- __e_acsl_assert(a == (void *)0,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(a == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"a == \\null",23);
__e_acsl_full_init((void *)(& a));
a = (char *)aligned_alloc((unsigned long)255,(unsigned long)512);
/*@ assert a ≡ \null; */
- __e_acsl_assert(a == (void *)0,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(a == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"a == \\null",26);
__e_acsl_full_init((void *)(& a));
a = (char *)aligned_alloc((unsigned long)0,(unsigned long)512);
/*@ assert a ≡ \null; */
- __e_acsl_assert(a == (void *)0,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(a == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"a == \\null",29);
__e_acsl_full_init((void *)(& a));
a = (char *)aligned_alloc((unsigned long)256,(unsigned long)512);
/*@ assert a ≢ \null; */
- __e_acsl_assert(a != (void *)0,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(a != (char *)0,(char *)"Assertion",(char *)"main",
(char *)"a != \\null",32);
/*@ assert \valid(a); */
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
index 617b202e126..e85e0a89dfa 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
@@ -21,30 +21,34 @@ int main(void)
{
int __gen_e_acsl_offset;
__gen_e_acsl_offset = __e_acsl_offset((void *)(A));
- __e_acsl_assert(__gen_e_acsl_offset == 0UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset((int *)A) == 0",13);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset == 0UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset((int *)A) == 0",13);
}
/*@ assert \offset(&A[3]) ≡ 12; */
{
int __gen_e_acsl_offset_2;
__gen_e_acsl_offset_2 = __e_acsl_offset((void *)(& A[3]));
- __e_acsl_assert(__gen_e_acsl_offset_2 == 12UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(&A[3]) == 12",14);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_2 == 12UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(&A[3]) == 12",14);
}
/*@ assert \offset(PA) ≡ 0; */
{
int __gen_e_acsl_offset_3;
__gen_e_acsl_offset_3 = __e_acsl_offset((void *)PA);
- __e_acsl_assert(__gen_e_acsl_offset_3 == 0UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(PA) == 0",15);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_3 == 0UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(PA) == 0",15);
}
PA ++;
/*@ assert \offset(PA + 1) ≡ 8; */
{
int __gen_e_acsl_offset_4;
__gen_e_acsl_offset_4 = __e_acsl_offset((void *)(PA + 1));
- __e_acsl_assert(__gen_e_acsl_offset_4 == 8UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(PA + 1) == 8",17);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_4 == 8UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(PA + 1) == 8",17);
}
int a[4] = {1, 2, 3, 4};
__e_acsl_store_block((void *)(a),(size_t)16);
@@ -53,22 +57,25 @@ int main(void)
{
int __gen_e_acsl_offset_5;
__gen_e_acsl_offset_5 = __e_acsl_offset((void *)(a));
- __e_acsl_assert(__gen_e_acsl_offset_5 == 0UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset((int *)a) == 0",21);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_5 == 0UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset((int *)a) == 0",21);
}
/*@ assert \offset(&a[1]) ≡ 4; */
{
int __gen_e_acsl_offset_6;
__gen_e_acsl_offset_6 = __e_acsl_offset((void *)(& a[1]));
- __e_acsl_assert(__gen_e_acsl_offset_6 == 4UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(&a[1]) == 4",22);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_6 == 4UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(&a[1]) == 4",22);
}
/*@ assert \offset(&a[3]) ≡ 12; */
{
int __gen_e_acsl_offset_7;
__gen_e_acsl_offset_7 = __e_acsl_offset((void *)(& a[3]));
- __e_acsl_assert(__gen_e_acsl_offset_7 == 12UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(&a[3]) == 12",23);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_7 == 12UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(&a[3]) == 12",23);
}
long l = (long)4;
__e_acsl_store_block((void *)(& l),(size_t)8);
@@ -80,29 +87,33 @@ int main(void)
{
int __gen_e_acsl_offset_8;
__gen_e_acsl_offset_8 = __e_acsl_offset((void *)(& l));
- __e_acsl_assert(__gen_e_acsl_offset_8 == 0UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(&l) == 0",28);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_8 == 0UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(&l) == 0",28);
}
/*@ assert \offset(pl) ≡ 0; */
{
int __gen_e_acsl_offset_9;
__gen_e_acsl_offset_9 = __e_acsl_offset((void *)pl);
- __e_acsl_assert(__gen_e_acsl_offset_9 == 0UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(pl) == 0",29);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_9 == 0UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(pl) == 0",29);
}
/*@ assert \offset(pl + 1) ≡ 1; */
{
int __gen_e_acsl_offset_10;
__gen_e_acsl_offset_10 = __e_acsl_offset((void *)(pl + 1));
- __e_acsl_assert(__gen_e_acsl_offset_10 == 1UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(pl + 1) == 1",30);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_10 == 1UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(pl + 1) == 1",30);
}
/*@ assert \offset(pl + 7) ≡ 7; */
{
int __gen_e_acsl_offset_11;
__gen_e_acsl_offset_11 = __e_acsl_offset((void *)(pl + 7));
- __e_acsl_assert(__gen_e_acsl_offset_11 == 7UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(pl + 7) == 7",31);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_11 == 7UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(pl + 7) == 7",31);
}
int *pi = (int *)(& l);
__e_acsl_store_block((void *)(& pi),(size_t)8);
@@ -111,8 +122,9 @@ int main(void)
{
int __gen_e_acsl_offset_12;
__gen_e_acsl_offset_12 = __e_acsl_offset((void *)pi);
- __e_acsl_assert(__gen_e_acsl_offset_12 == 0UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(pi) == 0",33);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_12 == 0UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(pi) == 0",33);
}
__e_acsl_full_init((void *)(& pi));
pi ++;
@@ -120,8 +132,9 @@ int main(void)
{
int __gen_e_acsl_offset_13;
__gen_e_acsl_offset_13 = __e_acsl_offset((void *)pi);
- __e_acsl_assert(__gen_e_acsl_offset_13 == 4UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(pi) == 4",35);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_13 == 4UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(pi) == 4",35);
}
char *p = malloc((unsigned long)12);
__e_acsl_store_block((void *)(& p),(size_t)8);
@@ -130,22 +143,25 @@ int main(void)
{
int __gen_e_acsl_offset_14;
__gen_e_acsl_offset_14 = __e_acsl_offset((void *)p);
- __e_acsl_assert(__gen_e_acsl_offset_14 == 0UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(p) == 0",39);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_14 == 0UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(p) == 0",39);
}
/*@ assert \offset(p + 1) ≡ 1; */
{
int __gen_e_acsl_offset_15;
__gen_e_acsl_offset_15 = __e_acsl_offset((void *)(p + 1));
- __e_acsl_assert(__gen_e_acsl_offset_15 == 1UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(p + 1) == 1",40);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_15 == 1UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(p + 1) == 1",40);
}
/*@ assert \offset(p + 11) ≡ 11; */
{
int __gen_e_acsl_offset_16;
__gen_e_acsl_offset_16 = __e_acsl_offset((void *)(p + 11));
- __e_acsl_assert(__gen_e_acsl_offset_16 == 11UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(p + 11) == 11",41);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_16 == 11UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(p + 11) == 11",41);
}
__e_acsl_full_init((void *)(& p));
p += 5;
@@ -153,15 +169,17 @@ int main(void)
{
int __gen_e_acsl_offset_17;
__gen_e_acsl_offset_17 = __e_acsl_offset((void *)(p + 5));
- __e_acsl_assert(__gen_e_acsl_offset_17 == 10UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(p + 5) == 10",43);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_17 == 10UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(p + 5) == 10",43);
}
/*@ assert \offset(p - 5) ≡ 0; */
{
int __gen_e_acsl_offset_18;
__gen_e_acsl_offset_18 = __e_acsl_offset((void *)(p - 5));
- __e_acsl_assert(__gen_e_acsl_offset_18 == 0UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(p - 5) == 0",44);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_18 == 0UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(p - 5) == 0",44);
}
long *q = malloc((unsigned long)30 * sizeof(long));
__e_acsl_store_block((void *)(& q),(size_t)8);
@@ -170,8 +188,9 @@ int main(void)
{
int __gen_e_acsl_offset_19;
__gen_e_acsl_offset_19 = __e_acsl_offset((void *)q);
- __e_acsl_assert(__gen_e_acsl_offset_19 == 0UL,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(q) == 0",49);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_19 == 0UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(q) == 0",49);
}
__e_acsl_full_init((void *)(& q));
q ++;
@@ -188,9 +207,9 @@ int main(void)
{
int __gen_e_acsl_offset_21;
__gen_e_acsl_offset_21 = __e_acsl_offset((void *)q);
- __e_acsl_assert(__gen_e_acsl_offset_21 == 8 * 3,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(q) == sizeof(long) * 3",
- 53);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_21 == 24UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(q) == sizeof(long) * 3",53);
}
__e_acsl_full_init((void *)(& q));
q += 4;
@@ -198,9 +217,9 @@ int main(void)
{
int __gen_e_acsl_offset_22;
__gen_e_acsl_offset_22 = __e_acsl_offset((void *)q);
- __e_acsl_assert(__gen_e_acsl_offset_22 == 8 * 7,(char *)"Assertion",
- (char *)"main",(char *)"\\offset(q) == sizeof(long) * 7",
- 55);
+ __e_acsl_assert((unsigned long)__gen_e_acsl_offset_22 == 56UL,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(q) == sizeof(long) * 7",55);
}
__retres = 0;
__e_acsl_delete_block((void *)(& PA));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c
index dc9943a1413..d5b4bfb8f0c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c
@@ -9,10 +9,10 @@ int main(void)
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
/*@ assert 'c' ≡ 'c'; */
- __e_acsl_assert('c' == 'c',(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"\'c\' == \'c\'",10);
/*@ assert false ≢ true; */
- __e_acsl_assert(false != true,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"false != true",11);
__retres = 0;
return __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
index e4608da3ba1..e7c194eb446 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
@@ -38,7 +38,7 @@ int main(void)
__e_acsl_assert(t[2] == 4,(char *)"Assertion",(char *)"main",
(char *)"t[2] == 4",13);
/*@ assert t[(2 * sizeof(int)) / sizeof((int)0x0)] ≡ 4; */
- __e_acsl_assert(t[(2 * 4) / 4] == 4,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(t[2] == 4,(char *)"Assertion",(char *)"main",
(char *)"t[(2 * sizeof(int)) / sizeof((int)0x0)] == 4",14);
{
int i = 0;
@@ -49,8 +49,8 @@ int main(void)
(char *)"index_bound: i < 3",17);
__e_acsl_assert(0 <= i,(char *)"RTE",(char *)"main",
(char *)"index_bound: 0 <= i",17);
- __e_acsl_assert(t[i] == i + 2L,(char *)"Assertion",(char *)"main",
- (char *)"t[i] == i + 2",17);
+ __e_acsl_assert((long)t[i] == i + 2L,(char *)"Assertion",
+ (char *)"main",(char *)"t[i] == i + 2",17);
}
/*@ assert t[2 - i] ≡ 4 - i; */
{
@@ -58,7 +58,7 @@ int main(void)
(char *)"index_bound: (long)(2 - i) < 3",18);
__e_acsl_assert(0L <= 2L - i,(char *)"RTE",(char *)"main",
(char *)"index_bound: 0 <= (long)(2 - i)",18);
- __e_acsl_assert(t[2L - i] == 4L - i,(char *)"Assertion",
+ __e_acsl_assert((long)t[2L - i] == 4L - i,(char *)"Assertion",
(char *)"main",(char *)"t[2 - i] == 4 - i",18);
}
/*@ assert *(&t[2] - i) ≡ 4 - i; */
@@ -71,7 +71,7 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(&t[2] - i)",19);
- __e_acsl_assert(*(& t[2] - i) == 4L - i,(char *)"Assertion",
+ __e_acsl_assert((long)*(& t[2] - i) == 4L - i,(char *)"Assertion",
(char *)"main",(char *)"*(&t[2] - i) == 4 - i",19);
}
i ++;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c
index 370901be596..0d4621a3787 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c
@@ -7,7 +7,7 @@ int main(void)
int x = 0;
x ++;
/*@ assert sizeof(int) ≡ sizeof(x); */
- __e_acsl_assert(4 == 4,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"sizeof(int) == sizeof(x)",8);
__retres = 0;
return __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
index f93322eba9c..9be411f816a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
@@ -53,14 +53,14 @@ int main(void)
{
__e_acsl_assert(x == 5,(char *)"Precondition",(char *)"main",
(char *)"x == 5",25);
- __e_acsl_assert(x == 3L + y,(char *)"Precondition",(char *)"main",
+ __e_acsl_assert((long)x == 3L + y,(char *)"Precondition",(char *)"main",
(char *)"x == 3 + y",28);
__e_acsl_assert(y == 2,(char *)"Precondition",(char *)"main",
(char *)"y == 2",29);
x = 3;
__e_acsl_assert(x == 3,(char *)"Postcondition",(char *)"main",
(char *)"x == 3",26);
- __e_acsl_assert(x == y + 1L,(char *)"Postcondition",(char *)"main",
+ __e_acsl_assert((long)x == y + 1L,(char *)"Postcondition",(char *)"main",
(char *)"x == y + 1",30);
}
/*@ behavior b1:
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c
index 50b033f93b4..00c3d99c4eb 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c
@@ -7,8 +7,8 @@ int main(void)
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
uint8 x = (unsigned char)0;
/*@ assert x ≡ 0; */
- __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",
- 9);
+ __e_acsl_assert((int)x == 0,(char *)"Assertion",(char *)"main",
+ (char *)"x == 0",9);
__retres = 0;
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
index 9ec0221d8cc..de7456a80e8 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
@@ -39,8 +39,8 @@ void f(int *x, int *y)
}
__e_acsl_initialize((void *)x,sizeof(int));
(*x) ++;
- __e_acsl_assert(2 >= 1,(char *)"Postcondition",(char *)"f",
- (char *)"2 >= 1",28);
+ __e_acsl_assert(1,(char *)"Postcondition",(char *)"f",(char *)"2 >= 1",
+ 28);
}
{
int i = 0;
@@ -55,8 +55,8 @@ void f(int *x, int *y)
/*@ loop invariant 0 ≤ i ≤ 1; */
while (i < 1) {
/*@ assert 1 ≡ 1; */
- __e_acsl_assert(1 == 1,(char *)"Assertion",(char *)"f",
- (char *)"1 == 1",33);
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"f",(char *)"1 == 1",
+ 33);
/*@ assert \valid(y); */
{
int __gen_e_acsl_valid;
@@ -196,7 +196,7 @@ void __gen_e_acsl_f(int *x, int *y)
__e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Postcondition",
(char *)"f",(char *)"\\old(*x == 0) ==> *\\old(x) == 1",
22);
- __e_acsl_assert(*__gen_e_acsl_at_5 == __gen_e_acsl_at_6 + 1L,
+ __e_acsl_assert((long)*__gen_e_acsl_at_5 == __gen_e_acsl_at_6 + 1L,
(char *)"Postcondition",(char *)"f",
(char *)"*\\old(x) == \\old(*x) + 1",14);
__e_acsl_delete_block((void *)(& y));
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c
index dd54c01842d..47fab5a664b 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c
@@ -39,8 +39,8 @@ void f(int *x, int *y)
}
__e_acsl_initialize((void *)x,sizeof(int));
(*x) ++;
- __e_acsl_assert(2 >= 1,(char *)"Postcondition",(char *)"f",
- (char *)"2 >= 1",28);
+ __e_acsl_assert(1,(char *)"Postcondition",(char *)"f",(char *)"2 >= 1",
+ 28);
}
{
int i = 0;
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 b5c44029845..bf5eca3ea03 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
@@ -38,7 +38,7 @@ int main(int argc, char const **argv)
/*@ assert g1 ≡ \null ∨ \valid(g1); */
{
int __gen_e_acsl_or;
- if (g1 == (void *)0) __gen_e_acsl_or = 1;
+ if (g1 == (char *)0) __gen_e_acsl_or = 1;
else {
int __gen_e_acsl_initialized;
int __gen_e_acsl_and;
@@ -59,7 +59,7 @@ int main(int argc, char const **argv)
/*@ assert g2 ≡ \null ∨ \valid(g2); */
{
int __gen_e_acsl_or_2;
- if (g2 == (void *)0) __gen_e_acsl_or_2 = 1;
+ if (g2 == (char *)0) __gen_e_acsl_or_2 = 1;
else {
int __gen_e_acsl_initialized_2;
int __gen_e_acsl_and_2;
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index f2eb5dab38c..6782dc740c9 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -545,7 +545,7 @@ and comparison_to_exp
in
Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
| Typing.C_type _ | Typing.Other ->
- Cil.new_exp ~loc (BinOp(bop, e1, e2, Cil.intType)), env
+ Cil.mkBinOp ~loc bop e1 e2, env
(* \base_addr, \block_length and \freeable annotations *)
and mmodel_call ~loc kf name ctx env t =
--
GitLab