diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index 370a935bc4793ba14b6cf1f7dbef6dc0727e4a1f..ab4a49034539ca546dd509ffc3d26f7b6609136a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -87,13 +87,13 @@ int __gen_e_acsl_sorted(int *t, int n)
(char *)"mem_access: \\valid_read(t+(unsigned long)__gen_e_acsl_i)",
6);
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + (unsigned long)(
- __gen_e_acsl_i - 1)),
+ __gen_e_acsl_i - 1L)),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"sorted",
(char *)"mem_access: \\valid_read(t+(unsigned long)((long)(__gen_e_acsl_i-1)))",
6);
- if (*(t + (unsigned long)(__gen_e_acsl_i - 1)) <= *(t + (unsigned long)__gen_e_acsl_i))
+ if (*(t + (unsigned long)(__gen_e_acsl_i - 1L)) <= *(t + (unsigned long)__gen_e_acsl_i))
;
else {
__gen_e_acsl_forall = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index 626085b24fc6b5e943b094126cd3b2a16e0672ae..0dc222899d2d73a76c0464882443955ca0791d3f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -95,25 +95,25 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read((int *)*__gen_e_acsl_at_6)",
8);
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_5)[1]),
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_5)[1UL]),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_5)[1])",
8);
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_4)[2]),
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_4)[2UL]),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_4)[2])",
8);
- __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_3)[3]),
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_3)[3UL]),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_3)[3])",
8);
- __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_2)[4]),
+ __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_2)[4UL]),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
@@ -124,7 +124,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__e_acsl_assert(__gen_e_acsl_valid_read_6,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at)",8);
- __e_acsl_assert(*__gen_e_acsl_at == (int)((((((*__gen_e_acsl_at_2)[4] + (*__gen_e_acsl_at_3)[3]) + (*__gen_e_acsl_at_4)[2]) + (*__gen_e_acsl_at_5)[1]) + (*__gen_e_acsl_at_6)[0]) / 5),
+ __e_acsl_assert(*__gen_e_acsl_at == (int)((((((*__gen_e_acsl_at_2)[4UL] + (*__gen_e_acsl_at_3)[3UL]) + (*__gen_e_acsl_at_4)[2UL]) + (*__gen_e_acsl_at_5)[1UL]) + (*__gen_e_acsl_at_6)[0UL]) / 5L),
(char *)"Postcondition",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"*\\old(AverageAccel) ==\n(((((*\\old(Accel))[4]+(*\\old(Accel))[3])+(*\\old(Accel))[2])+(*\\old(Accel))[1])+(*\n \\old(Accel))[0])/5",
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 f2790b2a2d6e506dae914675af757c8ca61d1049..5c194226eec561c2ae4eae73fb98baec27f7a8d4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -79,7 +79,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_forall_2;
unsigned long __gen_e_acsl_k;
__gen_e_acsl_forall_2 = 1;
- __gen_e_acsl_k = 0;
+ __gen_e_acsl_k = 0UL;
while (1) {
if (__gen_e_acsl_k < n) ; else break;
{
@@ -100,7 +100,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
mpz_t __gen_e_acsl__5;
mpz_t __gen_e_acsl_add_3;
unsigned long __gen_e_acsl__6;
- __gmpz_init_set_ui(__gen_e_acsl__5,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__5,1L);
__gmpz_init(__gen_e_acsl_add_3);
__gmpz_add(__gen_e_acsl_add_3,(__mpz_struct const *)__gen_e_acsl_k,
(__mpz_struct const *)(__gen_e_acsl__5));
@@ -120,7 +120,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_exists;
unsigned long __gen_e_acsl_i;
__gen_e_acsl_exists = 0;
- __gen_e_acsl_i = 0;
+ __gen_e_acsl_i = 0UL;
while (1) {
if (__gen_e_acsl_i < n) ; else break;
{
@@ -141,7 +141,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
mpz_t __gen_e_acsl_;
mpz_t __gen_e_acsl_add;
unsigned long __gen_e_acsl__2;
- __gmpz_init_set_ui(__gen_e_acsl_,1UL);
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)__gen_e_acsl_i,
(__mpz_struct const *)(__gen_e_acsl_));
@@ -189,7 +189,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
mpz_t __gen_e_acsl__3;
mpz_t __gen_e_acsl_add_2;
unsigned long __gen_e_acsl__4;
- __gmpz_init_set_ui(__gen_e_acsl__3,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__3,1L);
__gmpz_init(__gen_e_acsl_add_2);
__gmpz_add(__gen_e_acsl_add_2,(__mpz_struct const *)__gen_e_acsl_j,
(__mpz_struct const *)(__gen_e_acsl__3));
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 eec556a814892f9a85a5d4dfa3ea30e86cd4504b..ec7a141eff32162d869883769f09e936bdd96509 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
@@ -25,7 +25,7 @@ int main(void)
(char *)"mem_access: \\valid_read(&state->bitsInQueue)",
22);
__gen_e_acsl_initialized = __e_acsl_initialized((void *)(& state->dataQueue[
- state->bitsInQueue / 8]),
+ state->bitsInQueue / 8UL]),
sizeof(unsigned char __attribute__((
__aligned__(32)))));
__e_acsl_assert(! __gen_e_acsl_initialized,(char *)"Assertion",
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
index c274fbfcf2b7fd9c8eaf8a53ee9b46c0e948cd15..25a3068c5ea0f9f587f8b14c4fdc09d1f72ba492 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
@@ -34,11 +34,11 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_initialized;
int __gen_e_acsl_and;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& _G[0].str),
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& _G[0UL].str),
sizeof(char *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_G[0].str,
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_G[0UL].str,
sizeof(char));
__gen_e_acsl_and = __gen_e_acsl_valid_read;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c
index 8363cb460ba289cab38856923fa012437eb58d0d..661e8a3dd365fe3fc02f9e611e6b6ff2eabe29cb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c
@@ -48,7 +48,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_3;
void *__gen_e_acsl_base_addr_4;
- __gen_e_acsl_base_addr_3 = __e_acsl_base_addr((void *)(& A[3]));
+ __gen_e_acsl_base_addr_3 = __e_acsl_base_addr((void *)(& A[3UL]));
__gen_e_acsl_base_addr_4 = __e_acsl_base_addr((void *)PA);
__e_acsl_assert(__gen_e_acsl_base_addr_3 == __gen_e_acsl_base_addr_4,
(char *)"Assertion",(char *)"main",
@@ -69,8 +69,8 @@ int main(void)
{
void *__gen_e_acsl_base_addr_7;
void *__gen_e_acsl_base_addr_8;
- __gen_e_acsl_base_addr_7 = __e_acsl_base_addr((void *)(PA + 2));
- __gen_e_acsl_base_addr_8 = __e_acsl_base_addr((void *)(& A[3]));
+ __gen_e_acsl_base_addr_7 = __e_acsl_base_addr((void *)(PA + 2UL));
+ __gen_e_acsl_base_addr_8 = __e_acsl_base_addr((void *)(& A[3UL]));
__e_acsl_assert(__gen_e_acsl_base_addr_7 == __gen_e_acsl_base_addr_8,
(char *)"Assertion",(char *)"main",
(char *)"\\base_addr(PA+2) == \\base_addr(&A[3])",17);
@@ -99,7 +99,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_11;
void *__gen_e_acsl_base_addr_12;
- __gen_e_acsl_base_addr_11 = __e_acsl_base_addr((void *)(& a[3]));
+ __gen_e_acsl_base_addr_11 = __e_acsl_base_addr((void *)(& a[3UL]));
__gen_e_acsl_base_addr_12 = __e_acsl_base_addr((void *)pa);
__e_acsl_assert(__gen_e_acsl_base_addr_11 == __gen_e_acsl_base_addr_12,
(char *)"Assertion",(char *)"main",
@@ -121,7 +121,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_15;
void *__gen_e_acsl_base_addr_16;
- __gen_e_acsl_base_addr_15 = __e_acsl_base_addr((void *)(pa + 2));
+ __gen_e_acsl_base_addr_15 = __e_acsl_base_addr((void *)(pa + 2UL));
__gen_e_acsl_base_addr_16 = __e_acsl_base_addr((void *)(a));
__e_acsl_assert(__gen_e_acsl_base_addr_15 == __gen_e_acsl_base_addr_16,
(char *)"Assertion",(char *)"main",
@@ -145,7 +145,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_19;
void *__gen_e_acsl_base_addr_20;
- __gen_e_acsl_base_addr_19 = __e_acsl_base_addr((void *)(pl + 2));
+ __gen_e_acsl_base_addr_19 = __e_acsl_base_addr((void *)(pl + 2UL));
__gen_e_acsl_base_addr_20 = __e_acsl_base_addr((void *)(& l));
__e_acsl_assert(__gen_e_acsl_base_addr_19 == __gen_e_acsl_base_addr_20,
(char *)"Assertion",(char *)"main",
@@ -195,8 +195,8 @@ int main(void)
{
void *__gen_e_acsl_base_addr_27;
void *__gen_e_acsl_base_addr_28;
- __gen_e_acsl_base_addr_27 = __e_acsl_base_addr((void *)(p + 1));
- __gen_e_acsl_base_addr_28 = __e_acsl_base_addr((void *)(pd + 5));
+ __gen_e_acsl_base_addr_27 = __e_acsl_base_addr((void *)(p + 1UL));
+ __gen_e_acsl_base_addr_28 = __e_acsl_base_addr((void *)(pd + 5UL));
__e_acsl_assert(__gen_e_acsl_base_addr_27 == __gen_e_acsl_base_addr_28,
(char *)"Assertion",(char *)"main",
(char *)"\\base_addr(p+1) == \\base_addr(pd+5)",45);
@@ -205,8 +205,8 @@ int main(void)
{
void *__gen_e_acsl_base_addr_29;
void *__gen_e_acsl_base_addr_30;
- __gen_e_acsl_base_addr_29 = __e_acsl_base_addr((void *)(p + 11));
- __gen_e_acsl_base_addr_30 = __e_acsl_base_addr((void *)(pd + 1));
+ __gen_e_acsl_base_addr_29 = __e_acsl_base_addr((void *)(p + 11UL));
+ __gen_e_acsl_base_addr_30 = __e_acsl_base_addr((void *)(pd + 1UL));
__e_acsl_assert(__gen_e_acsl_base_addr_29 == __gen_e_acsl_base_addr_30,
(char *)"Assertion",(char *)"main",
(char *)"\\base_addr(p+11) == \\base_addr(pd+1)",46);
@@ -217,7 +217,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_31;
void *__gen_e_acsl_base_addr_32;
- __gen_e_acsl_base_addr_31 = __e_acsl_base_addr((void *)(p + 5));
+ __gen_e_acsl_base_addr_31 = __e_acsl_base_addr((void *)(p + 5UL));
__gen_e_acsl_base_addr_32 = __e_acsl_base_addr((void *)pd);
__e_acsl_assert(__gen_e_acsl_base_addr_31 == __gen_e_acsl_base_addr_32,
(char *)"Assertion",(char *)"main",
@@ -227,7 +227,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_33;
void *__gen_e_acsl_base_addr_34;
- __gen_e_acsl_base_addr_33 = __e_acsl_base_addr((void *)(p - 5));
+ __gen_e_acsl_base_addr_33 = __e_acsl_base_addr((void *)(p - 5UL));
__gen_e_acsl_base_addr_34 = __e_acsl_base_addr((void *)pd);
__e_acsl_assert(__gen_e_acsl_base_addr_33 == __gen_e_acsl_base_addr_34,
(char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_block_length.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_block_length.c
index 7de3d4ff48c116c0c73d89597089f99ac5d6f0ac..c38da21532d9940823b647cf88ed55c54dae1d3f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_block_length.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_block_length.c
@@ -50,7 +50,7 @@ int main(void)
/*@ assert \block_length(&A[3]) ≡ sizeof(A); */
{
unsigned long __gen_e_acsl_block_length_2;
- __gen_e_acsl_block_length_2 = __e_acsl_block_length((void *)(& A[3]));
+ __gen_e_acsl_block_length_2 = __e_acsl_block_length((void *)(& A[3UL]));
__e_acsl_assert(__gen_e_acsl_block_length_2 == 16,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(&A[3]) == sizeof(A)",16);
@@ -68,8 +68,8 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_4;
unsigned long __gen_e_acsl_block_length_5;
- __gen_e_acsl_block_length_4 = __e_acsl_block_length((void *)(PA + 1));
- __gen_e_acsl_block_length_5 = __e_acsl_block_length((void *)(& A[1]));
+ __gen_e_acsl_block_length_4 = __e_acsl_block_length((void *)(PA + 1UL));
+ __gen_e_acsl_block_length_5 = __e_acsl_block_length((void *)(& A[1UL]));
__e_acsl_assert(__gen_e_acsl_block_length_4 == __gen_e_acsl_block_length_5,
(char *)"Assertion",(char *)"main",
(char *)"\\block_length(PA+1) == \\block_length(&A[1])",
@@ -96,7 +96,7 @@ int main(void)
/*@ assert \block_length(&a[3]) ≡ sizeof(a); */
{
unsigned long __gen_e_acsl_block_length_7;
- __gen_e_acsl_block_length_7 = __e_acsl_block_length((void *)(& a[3]));
+ __gen_e_acsl_block_length_7 = __e_acsl_block_length((void *)(& a[3UL]));
__e_acsl_assert(__gen_e_acsl_block_length_7 == 16,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(&a[3]) == sizeof(a)",25);
@@ -115,8 +115,8 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_9;
unsigned long __gen_e_acsl_block_length_10;
- __gen_e_acsl_block_length_9 = __e_acsl_block_length((void *)(pa + 1));
- __gen_e_acsl_block_length_10 = __e_acsl_block_length((void *)(& a[1]));
+ __gen_e_acsl_block_length_9 = __e_acsl_block_length((void *)(pa + 1UL));
+ __gen_e_acsl_block_length_10 = __e_acsl_block_length((void *)(& a[1UL]));
__e_acsl_assert(__gen_e_acsl_block_length_9 == __gen_e_acsl_block_length_10,
(char *)"Assertion",(char *)"main",
(char *)"\\block_length(pa+1) == \\block_length(&a[1])",
@@ -145,7 +145,7 @@ int main(void)
/*@ assert \block_length(pl+7) ≡ sizeof(long); */
{
unsigned long __gen_e_acsl_block_length_13;
- __gen_e_acsl_block_length_13 = __e_acsl_block_length((void *)(pl + 7));
+ __gen_e_acsl_block_length_13 = __e_acsl_block_length((void *)(pl + 7UL));
__e_acsl_assert(__gen_e_acsl_block_length_13 == 8,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(pl+7) == sizeof(long)",36);
@@ -187,7 +187,7 @@ int main(void)
/*@ assert \block_length(p+11) ≡ size; */
{
unsigned long __gen_e_acsl_block_length_19;
- __gen_e_acsl_block_length_19 = __e_acsl_block_length((void *)(p + 11));
+ __gen_e_acsl_block_length_19 = __e_acsl_block_length((void *)(p + 11UL));
__e_acsl_assert(__gen_e_acsl_block_length_19 == size,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(p+11) == size",46);
}
@@ -197,8 +197,8 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_20;
unsigned long __gen_e_acsl_block_length_21;
- __gen_e_acsl_block_length_20 = __e_acsl_block_length((void *)(p + 5));
- __gen_e_acsl_block_length_21 = __e_acsl_block_length((void *)(p - 5));
+ __gen_e_acsl_block_length_20 = __e_acsl_block_length((void *)(p + 5UL));
+ __gen_e_acsl_block_length_21 = __e_acsl_block_length((void *)(p - 5UL));
__e_acsl_assert(__gen_e_acsl_block_length_20 == __gen_e_acsl_block_length_21,
(char *)"Assertion",(char *)"main",
(char *)"\\block_length(p+5) == \\block_length(p-5)",48);
@@ -226,14 +226,14 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_24;
__gen_e_acsl_block_length_24 = __e_acsl_block_length((void *)(& ZERO));
- __e_acsl_assert(__gen_e_acsl_block_length_24 == 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_block_length_24 == 0UL,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(&ZERO) == 0",60);
}
/*@ assert \block_length(&zero) ≡ 0; */
{
unsigned long __gen_e_acsl_block_length_25;
__gen_e_acsl_block_length_25 = __e_acsl_block_length((void *)(& zero));
- __e_acsl_assert(__gen_e_acsl_block_length_25 == 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_block_length_25 == 0UL,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(&zero) == 0",61);
}
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers.c
index 41873f0f48f0e3c981556b96a3b6184398da43f4..e91689cdab0429d2ef3188051a005c608b738e3e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers.c
@@ -78,7 +78,7 @@ int main(int argc, char **argv)
sizeof(char *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_A[0],
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_A[0UL],
sizeof(char));
__gen_e_acsl_and = __gen_e_acsl_valid_read;
}
@@ -90,11 +90,11 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_initialized_2;
int __gen_e_acsl_and_2;
- __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& _A[1]),
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& _A[1UL]),
sizeof(char *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_read_2;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)_A[1],
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)_A[1UL],
sizeof(char));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_read_2;
}
@@ -149,7 +149,7 @@ int main(int argc, char **argv)
(char *)"\\valid(&_G)",42);
}
/*@ assert _G[0].num ≡ 99; */
- __e_acsl_assert(_G[0].num == 99,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(_G[0UL].num == 99,(char *)"Assertion",(char *)"main",
(char *)"_G[0].num == 99",43);
__retres = 0;
__e_acsl_delete_block((void *)(_G));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
index 9292547138fd27eaacddded42dcf3c67f3ee1755..35982c77d6f71a2507958535f5f7215f62bae471 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
@@ -34,7 +34,7 @@ int main(void)
/*@ assert ¬\freeable(p+1); */
{
int __gen_e_acsl_freeable_3;
- __gen_e_acsl_freeable_3 = __e_acsl_freeable((void *)(p + 1));
+ __gen_e_acsl_freeable_3 = __e_acsl_freeable((void *)(p + 1UL));
__e_acsl_assert(! __gen_e_acsl_freeable_3,(char *)"Assertion",
(char *)"main",(char *)"!\\freeable(p+1)",18);
}
@@ -63,7 +63,7 @@ int main(void)
/*@ assert ¬\freeable(&array[5]); */
{
int __gen_e_acsl_freeable_7;
- __gen_e_acsl_freeable_7 = __e_acsl_freeable((void *)(& array[5]));
+ __gen_e_acsl_freeable_7 = __e_acsl_freeable((void *)(& array[5UL]));
__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/e-acsl-runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
index 52a4f185b624b05d123fa9f804d7e338ea7f5d3c..7865409aa55f26a4bd637c96c71b349beca39444 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
@@ -311,7 +311,7 @@ void __gen_e_acsl_k(void)
(char *)"k",(char *)"X == 3 && Y == 2 ==> X == 3",42);
if (X == 3) __gen_e_acsl_and_2 = Y == 2; else __gen_e_acsl_and_2 = 0;
if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1;
- else __gen_e_acsl_implies_3 = X + Y == 5;
+ else __gen_e_acsl_implies_3 = X + Y == 5L;
__e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
(char *)"k",(char *)"X == 3 && Y == 2 ==> X+Y == 5",43);
k();
@@ -332,14 +332,14 @@ void __gen_e_acsl_j(void)
{
__e_acsl_assert(X == 5,(char *)"Precondition",(char *)"j",(char *)"X == 5",
27);
- __e_acsl_assert(X == 3 + Y,(char *)"Precondition",(char *)"j",
+ __e_acsl_assert(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 + 1,(char *)"Postcondition",(char *)"j",
+ __e_acsl_assert(X == Y + 1L,(char *)"Postcondition",(char *)"j",
(char *)"X == Y+1",32);
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c
index a59138963615961ea62b70f52e42df4439a69922..6e0e311130ead0c50445101faba7844df0285120 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c
@@ -143,7 +143,7 @@ int main(void)
/*@ assert ¬\initialized(&d[1]); */
{
int __gen_e_acsl_initialized_12;
- __gen_e_acsl_initialized_12 = __e_acsl_initialized((void *)(& d[1]),
+ __gen_e_acsl_initialized_12 = __e_acsl_initialized((void *)(& d[1UL]),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_12,(char *)"Assertion",
(char *)"main",(char *)"!\\initialized(&d[1])",44);
@@ -167,7 +167,7 @@ int main(void)
/*@ assert ¬\initialized(r+1); */
{
int __gen_e_acsl_initialized_15;
- __gen_e_acsl_initialized_15 = __e_acsl_initialized((void *)(r + 1),
+ __gen_e_acsl_initialized_15 = __e_acsl_initialized((void *)(r + 1UL),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_15,(char *)"Assertion",
(char *)"main",(char *)"!\\initialized(r+1)",47);
@@ -185,7 +185,7 @@ int main(void)
/*@ assert ¬\initialized(&d[1]); */
{
int __gen_e_acsl_initialized_17;
- __gen_e_acsl_initialized_17 = __e_acsl_initialized((void *)(& d[1]),
+ __gen_e_acsl_initialized_17 = __e_acsl_initialized((void *)(& d[1UL]),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_17,(char *)"Assertion",
(char *)"main",(char *)"!\\initialized(&d[1])",51);
@@ -209,7 +209,7 @@ int main(void)
/*@ assert ¬\initialized(r+1); */
{
int __gen_e_acsl_initialized_20;
- __gen_e_acsl_initialized_20 = __e_acsl_initialized((void *)(r + 1),
+ __gen_e_acsl_initialized_20 = __e_acsl_initialized((void *)(r + 1UL),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_20,(char *)"Assertion",
(char *)"main",(char *)"!\\initialized(r+1)",54);
@@ -227,7 +227,7 @@ int main(void)
/*@ assert \initialized(&d[1]); */
{
int __gen_e_acsl_initialized_22;
- __gen_e_acsl_initialized_22 = __e_acsl_initialized((void *)(& d[1]),
+ __gen_e_acsl_initialized_22 = __e_acsl_initialized((void *)(& d[1UL]),
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_22,(char *)"Assertion",
(char *)"main",(char *)"\\initialized(&d[1])",58);
@@ -251,7 +251,7 @@ int main(void)
/*@ assert \initialized(r+1); */
{
int __gen_e_acsl_initialized_25;
- __gen_e_acsl_initialized_25 = __e_acsl_initialized((void *)(r + 1),
+ __gen_e_acsl_initialized_25 = __e_acsl_initialized((void *)(r + 1UL),
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_25,(char *)"Assertion",
(char *)"main",(char *)"\\initialized(r+1)",61);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index 22b41d67d4e8b1225ca414f3c66146a652b4faf7..706a1e4335d58a3912aa374551f8794ac9f583d3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -35,7 +35,7 @@ int search(int elt)
__gen_e_acsl_i = 0;
while (1) {
if (__gen_e_acsl_i < k) ; else break;
- __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_i) < 10,
+ __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_i) < 10U,
(char *)"RTE",(char *)"search",
(char *)"index_bound: (unsigned long)__gen_e_acsl_i < 10",
18);
@@ -79,7 +79,7 @@ int search(int elt)
__gen_e_acsl_i_2 = 0;
while (1) {
if (__gen_e_acsl_i_2 < k) ; else break;
- __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_i_2) < 10,
+ __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_i_2) < 10U,
(char *)"RTE",(char *)"search",
(char *)"index_bound: (unsigned long)__gen_e_acsl_i_2 < 10",
18);
@@ -148,7 +148,7 @@ int __gen_e_acsl_search(int elt)
__gen_e_acsl_i = 0;
while (1) {
if (__gen_e_acsl_i < 9) ; else break;
- __e_acsl_assert((unsigned int)((unsigned long)(__gen_e_acsl_i + 1)) < 10,
+ __e_acsl_assert((unsigned int)((unsigned long)(__gen_e_acsl_i + 1L)) < 10U,
(char *)"RTE",(char *)"search",
(char *)"index_bound: (unsigned long)(__gen_e_acsl_i+1) < 10",
7);
@@ -156,7 +156,7 @@ int __gen_e_acsl_search(int elt)
(char *)"index_bound: __gen_e_acsl_i < 10",7);
__e_acsl_assert(0 <= __gen_e_acsl_i,(char *)"RTE",(char *)"search",
(char *)"index_bound: 0 <= __gen_e_acsl_i",7);
- if (A[__gen_e_acsl_i] <= A[__gen_e_acsl_i + 1]) ;
+ if (A[__gen_e_acsl_i] <= A[__gen_e_acsl_i + 1UL]) ;
else {
__gen_e_acsl_forall = 0;
goto e_acsl_end_loop3;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
index 03edc7ec0616664ce30624598ff456f1018404c0..46adee7686eb208a41375ff00252f481a9b08930 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
@@ -55,11 +55,11 @@ void nested_loops(void)
__gen_e_acsl_l = 0;
while (1) {
if (__gen_e_acsl_l < j) ; else break;
- __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_l) < 15,
+ __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) < 10,
+ __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);
@@ -107,11 +107,11 @@ 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) < 15,
+ __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",
19);
- __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_k_2) < 10,
+ __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",
19);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
index fb58b0114e392a4dce59b5348fd2c46c3890f5a7..c82c2fe2c03e3ef2d999c6aac2fc3d65bef1c0e9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
@@ -53,7 +53,7 @@ int main(int argc, char **argv)
int __gen_e_acsl_eq;
__gen_e_acsl_block_length = __e_acsl_block_length((void *)argv);
__gmpz_init_set_ui(__gen_e_acsl_block_length_2,__gen_e_acsl_block_length);
- __gmpz_init_set_si(__gen_e_acsl_,(argc + 1) * 8);
+ __gmpz_init_set_si(__gen_e_acsl_,(argc + 1L) * 8);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_2),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
index 84d0d914344d829243acff3b468adfe64fc362e9..baef4ede1cde093a82b74134800a584150812260 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
@@ -10,54 +10,54 @@ int main(int argc, char **argv)
__e_acsl_full_init((void *)(& a));
a = (char *)__gen_e_acsl_malloc((unsigned long)7);
/*@ assert __e_acsl_heap_size ≡ 7; */
- __e_acsl_assert(__e_acsl_heap_size == 7,(char *)"Assertion",(char *)"main",
- (char *)"__e_acsl_heap_size == 7",22);
+ __e_acsl_assert(__e_acsl_heap_size == 7UL,(char *)"Assertion",
+ (char *)"main",(char *)"__e_acsl_heap_size == 7",22);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_malloc((unsigned long)14);
/*@ assert __e_acsl_heap_size ≡ 21; */
- __e_acsl_assert(__e_acsl_heap_size == 21,(char *)"Assertion",
+ __e_acsl_assert(__e_acsl_heap_size == 21UL,(char *)"Assertion",
(char *)"main",(char *)"__e_acsl_heap_size == 21",24);
__gen_e_acsl_free((void *)a);
/*@ assert __e_acsl_heap_size ≡ 14; */
- __e_acsl_assert(__e_acsl_heap_size == 14,(char *)"Assertion",
+ __e_acsl_assert(__e_acsl_heap_size == 14UL,(char *)"Assertion",
(char *)"main",(char *)"__e_acsl_heap_size == 14",28);
__e_acsl_full_init((void *)(& a));
a = (char *)0;
__gen_e_acsl_free((void *)a);
/*@ assert __e_acsl_heap_size ≡ 14; */
- __e_acsl_assert(__e_acsl_heap_size == 14,(char *)"Assertion",
+ __e_acsl_assert(__e_acsl_heap_size == 14UL,(char *)"Assertion",
(char *)"main",(char *)"__e_acsl_heap_size == 14",33);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_realloc((void *)b,(unsigned long)9);
/*@ assert __e_acsl_heap_size ≡ 9; */
- __e_acsl_assert(__e_acsl_heap_size == 9,(char *)"Assertion",(char *)"main",
- (char *)"__e_acsl_heap_size == 9",37);
+ __e_acsl_assert(__e_acsl_heap_size == 9UL,(char *)"Assertion",
+ (char *)"main",(char *)"__e_acsl_heap_size == 9",37);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_realloc((void *)b,(unsigned long)18);
/*@ assert __e_acsl_heap_size ≡ 18; */
- __e_acsl_assert(__e_acsl_heap_size == 18,(char *)"Assertion",
+ __e_acsl_assert(__e_acsl_heap_size == 18UL,(char *)"Assertion",
(char *)"main",(char *)"__e_acsl_heap_size == 18",41);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_realloc((void *)b,(unsigned long)0);
__e_acsl_full_init((void *)(& b));
b = (char *)0;
/*@ assert __e_acsl_heap_size ≡ 0; */
- __e_acsl_assert(__e_acsl_heap_size == 0,(char *)"Assertion",(char *)"main",
- (char *)"__e_acsl_heap_size == 0",46);
+ __e_acsl_assert(__e_acsl_heap_size == 0UL,(char *)"Assertion",
+ (char *)"main",(char *)"__e_acsl_heap_size == 0",46);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_realloc((void *)b,(unsigned long)8);
/*@ assert __e_acsl_heap_size ≡ 8; */
- __e_acsl_assert(__e_acsl_heap_size == 8,(char *)"Assertion",(char *)"main",
- (char *)"__e_acsl_heap_size == 8",50);
+ __e_acsl_assert(__e_acsl_heap_size == 8UL,(char *)"Assertion",
+ (char *)"main",(char *)"__e_acsl_heap_size == 8",50);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_realloc((void *)0,(unsigned long)8);
/*@ assert __e_acsl_heap_size ≡ 16; */
- __e_acsl_assert(__e_acsl_heap_size == 16,(char *)"Assertion",
+ __e_acsl_assert(__e_acsl_heap_size == 16UL,(char *)"Assertion",
(char *)"main",(char *)"__e_acsl_heap_size == 16",54);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_realloc((void *)0,18446744073709551615UL);
/*@ assert __e_acsl_heap_size ≡ 16; */
- __e_acsl_assert(__e_acsl_heap_size == 16,(char *)"Assertion",
+ __e_acsl_assert(__e_acsl_heap_size == 16UL,(char *)"Assertion",
(char *)"main",(char *)"__e_acsl_heap_size == 16",58);
/*@ assert b ≡ (char *)((void *)0); */
__e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
@@ -66,7 +66,7 @@ int main(int argc, char **argv)
b = (char *)__gen_e_acsl_calloc(18446744073709551615UL,
18446744073709551615UL);
/*@ assert __e_acsl_heap_size ≡ 16; */
- __e_acsl_assert(__e_acsl_heap_size == 16,(char *)"Assertion",
+ __e_acsl_assert(__e_acsl_heap_size == 16UL,(char *)"Assertion",
(char *)"main",(char *)"__e_acsl_heap_size == 16",63);
/*@ assert b ≡ (char *)((void *)0); */
__e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
@@ -74,7 +74,7 @@ int main(int argc, char **argv)
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_malloc(18446744073709551615UL);
/*@ assert __e_acsl_heap_size ≡ 16; */
- __e_acsl_assert(__e_acsl_heap_size == 16,(char *)"Assertion",
+ __e_acsl_assert(__e_acsl_heap_size == 16UL,(char *)"Assertion",
(char *)"main",(char *)"__e_acsl_heap_size == 16",68);
/*@ assert b ≡ (char *)((void *)0); */
__e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_offset.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_offset.c
index a2bb9d8d67fd848186d8a7f9722d0605cb257f9e..971da0271548c3b6807a581e3fbad604406dade7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_offset.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_offset.c
@@ -32,29 +32,29 @@ int main(void)
{
int __gen_e_acsl_offset;
__gen_e_acsl_offset = __e_acsl_offset((void *)(A));
- __e_acsl_assert(__gen_e_acsl_offset == 0,(char *)"Assertion",
+ __e_acsl_assert(__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 == 12,(char *)"Assertion",
+ __gen_e_acsl_offset_2 = __e_acsl_offset((void *)(& A[3UL]));
+ __e_acsl_assert(__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 == 0,(char *)"Assertion",
+ __e_acsl_assert(__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 == 8,(char *)"Assertion",
+ __gen_e_acsl_offset_4 = __e_acsl_offset((void *)(PA + 1UL));
+ __e_acsl_assert(__gen_e_acsl_offset_4 == 8UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(PA+1) == 8",17);
}
__e_acsl_initialize((void *)(a),sizeof(int));
@@ -69,21 +69,21 @@ 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 == 0,(char *)"Assertion",
+ __e_acsl_assert(__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 == 4,(char *)"Assertion",
+ __gen_e_acsl_offset_6 = __e_acsl_offset((void *)(& a[1UL]));
+ __e_acsl_assert(__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 == 12,(char *)"Assertion",
+ __gen_e_acsl_offset_7 = __e_acsl_offset((void *)(& a[3UL]));
+ __e_acsl_assert(__gen_e_acsl_offset_7 == 12UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(&a[3]) == 12",23);
}
__e_acsl_full_init((void *)(& l));
@@ -94,28 +94,28 @@ 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 == 0,(char *)"Assertion",
+ __e_acsl_assert(__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 == 0,(char *)"Assertion",
+ __e_acsl_assert(__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 == 1,(char *)"Assertion",
+ __gen_e_acsl_offset_10 = __e_acsl_offset((void *)(pl + 1UL));
+ __e_acsl_assert(__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 == 7,(char *)"Assertion",
+ __gen_e_acsl_offset_11 = __e_acsl_offset((void *)(pl + 7UL));
+ __e_acsl_assert(__gen_e_acsl_offset_11 == 7UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(pl+7) == 7",31);
}
__e_acsl_full_init((void *)(& pi));
@@ -124,7 +124,7 @@ 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 == 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_offset_12 == 0UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(pi) == 0",33);
}
__e_acsl_full_init((void *)(& pi));
@@ -133,7 +133,7 @@ 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 == 4,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_offset_13 == 4UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(pi) == 4",35);
}
__e_acsl_full_init((void *)(& p));
@@ -142,21 +142,21 @@ 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 == 0,(char *)"Assertion",
+ __e_acsl_assert(__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 == 1,(char *)"Assertion",
+ __gen_e_acsl_offset_15 = __e_acsl_offset((void *)(p + 1UL));
+ __e_acsl_assert(__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 == 11,(char *)"Assertion",
+ __gen_e_acsl_offset_16 = __e_acsl_offset((void *)(p + 11UL));
+ __e_acsl_assert(__gen_e_acsl_offset_16 == 11UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(p+11) == 11",41);
}
__e_acsl_full_init((void *)(& p));
@@ -164,15 +164,15 @@ int main(void)
/*@ assert \offset(p+5) ≡ 10; */
{
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 == 10,(char *)"Assertion",
+ __gen_e_acsl_offset_17 = __e_acsl_offset((void *)(p + 5UL));
+ __e_acsl_assert(__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 == 0,(char *)"Assertion",
+ __gen_e_acsl_offset_18 = __e_acsl_offset((void *)(p - 5UL));
+ __e_acsl_assert(__gen_e_acsl_offset_18 == 0UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(p-5) == 0",44);
}
__e_acsl_full_init((void *)(& q));
@@ -181,7 +181,7 @@ 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 == 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_offset_19 == 0UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(q) == 0",49);
}
__e_acsl_full_init((void *)(& q));
@@ -199,7 +199,7 @@ 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",
+ __e_acsl_assert(__gen_e_acsl_offset_21 == 8 * 3UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(q) == sizeof(long)*3",
53);
}
@@ -209,7 +209,7 @@ 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",
+ __e_acsl_assert(__gen_e_acsl_offset_22 == 8 * 7UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(q) == sizeof(long)*7",
55);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
index 138fec283e4f154d6d5288d47e998384b6840d45..05ebfe2e433308df264cb866d57785b3d0e222d1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
@@ -40,42 +40,43 @@ int main(void)
__e_acsl_assert(t[0UL] == 2,(char *)"Assertion",(char *)"main",
(char *)"t[0] == 2",12);
/*@ assert t[2] ≡ 4; */
- __e_acsl_assert(t[2] == 4,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(t[2UL] == 4,(char *)"Assertion",(char *)"main",
(char *)"t[2] == 4",13);
/*@ assert t[(2*sizeof(int))/sizeof((int)0x0)] ≡ 4; */
__e_acsl_assert((unsigned long)((unsigned long)(2 * 4) / 4) < 3,
(char *)"RTE",(char *)"main",
(char *)"index_bound: (unsigned long)((unsigned long)(2*4)/4) < 3",
14);
- __e_acsl_assert(t[(2 * 4) / 4] == 4,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(t[(2UL * 4) / 4] == 4,(char *)"Assertion",(char *)"main",
(char *)"t[(2*sizeof(int))/sizeof((int)0x0)] == 4",14);
{
int i;
i = 0;
while (i < 2) {
/*@ assert t[i] ≡ i+2; */
- __e_acsl_assert((unsigned int)((unsigned long)i) < 3,(char *)"RTE",
+ __e_acsl_assert((unsigned int)((unsigned long)i) < 3U,(char *)"RTE",
(char *)"main",
(char *)"index_bound: (unsigned long)i < 3",17);
- __e_acsl_assert(t[(unsigned long)i] == i + 2,(char *)"Assertion",
+ __e_acsl_assert(t[(unsigned long)i] == i + 2L,(char *)"Assertion",
(char *)"main",(char *)"t[i] == i+2",17);
/*@ assert t[2-i] ≡ 4-i; */
- __e_acsl_assert((unsigned int)((unsigned long)(2 - i)) < 3,
+ __e_acsl_assert((unsigned int)((unsigned long)(2L - i)) < 3U,
(char *)"RTE",(char *)"main",
(char *)"index_bound: (unsigned long)((long)(2-i)) < 3",
18);
- __e_acsl_assert(t[(unsigned long)(2 - i)] == 4 - i,(char *)"Assertion",
- (char *)"main",(char *)"t[2-i] == 4-i",18);
+ __e_acsl_assert(t[(unsigned long)(2L - i)] == 4L - i,
+ (char *)"Assertion",(char *)"main",
+ (char *)"t[2-i] == 4-i",18);
/*@ assert *(&t[2]-i) ≡ 4-i; */
{
int __gen_e_acsl_valid_read_2;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& t[2] - (unsigned long)i),
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& t[2UL] - (unsigned long)i),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(&t[2]-(unsigned long)i)",
19);
- __e_acsl_assert(*(& t[2] - (unsigned long)i) == 4 - i,
+ __e_acsl_assert(*(& t[2UL] - (unsigned long)i) == 4L - i,
(char *)"Assertion",(char *)"main",
(char *)"*(&t[2]-i) == 4-i",19);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
index bca2199e10f4409bef6b21c336d0201d1b5a8538..c1471f8ec1d993bbf69770f1f184e10d364b545a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
@@ -44,14 +44,14 @@ int main(void)
{
__e_acsl_assert(x == 5,(char *)"Precondition",(char *)"main",
(char *)"x == 5",23);
- __e_acsl_assert(x == 3 + y,(char *)"Precondition",(char *)"main",
+ __e_acsl_assert(x == 3L + y,(char *)"Precondition",(char *)"main",
(char *)"x == 3+y",26);
__e_acsl_assert(y == 2,(char *)"Precondition",(char *)"main",
(char *)"y == 2",27);
x = 3;
__e_acsl_assert(x == 3,(char *)"Postcondition",(char *)"main",
(char *)"x == 3",24);
- __e_acsl_assert(x == y + 1,(char *)"Postcondition",(char *)"main",
+ __e_acsl_assert(x == y + 1L,(char *)"Postcondition",(char *)"main",
(char *)"x == y+1",28);
}
/*@ behavior b1:
@@ -81,7 +81,7 @@ int main(void)
(char *)"main",(char *)"x == 3 && y == 2 ==> x == 3",37);
if (x == 3) __gen_e_acsl_and_2 = y == 2; else __gen_e_acsl_and_2 = 0;
if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1;
- else __gen_e_acsl_implies_3 = x + y == 5;
+ else __gen_e_acsl_implies_3 = x + y == 5L;
__e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
(char *)"main",(char *)"x == 3 && y == 2 ==> x+y == 5",
38);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
index 3b4d57b36a2de87480e5b15c0fd94f4db22f401d..86fb3e2706bfcd82f0412d3754badd1d88b5e987 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
@@ -37,7 +37,7 @@ int main(void)
/*@ assert \initialized(&v1[2]); */
{
int __gen_e_acsl_initialized;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& v1[2]),
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& v1[2UL]),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
(char *)"main",(char *)"\\initialized(&v1[2])",24);
@@ -48,7 +48,7 @@ int main(void)
/*@ assert \initialized(v2+2); */
{
int __gen_e_acsl_initialized_2;
- __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(v2 + 2),
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(v2 + 2UL),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_2,(char *)"Assertion",
(char *)"main",(char *)"\\initialized(v2+2)",27);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
index 7b95350061a0f82fffe3c84436db40f5dd168fc5..3fad77f57e37c1a8987b1c97a90f503b2a70c109 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
@@ -12,14 +12,13 @@
__e_acsl_heap_size ∈ [--..--]
[value] using specification for function __e_acsl_assert
[value] using specification for function __gmpz_init_set_str
-[value] using specification for function __gmpz_init_set_ui
+[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_cmp
[value] using specification for function __gmpz_init
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_q
[value] using specification for function __gmpz_get_ui
[value] using specification for function __gmpz_clear
-[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_add
tests/gmp/arith.i:34:[value] warning: signed overflow. assert 1+__gen_e_acsl__7 ≤ 2147483647;
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
index 7bfeea1647e7239805cf4422273cd765247f13c4..fcbbbadd1109eb0dcbfdcfceecd9dc7929e0f4f6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
@@ -10,10 +10,9 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_size ∈ [--..--]
-[value] using specification for function __gmpz_init_set_ui
+[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_neg
-[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
@@ -25,4 +24,5 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: preco
[value] using specification for function __gmpz_tdiv_q
[value] using specification for function __gmpz_init_set_str
[value] using specification for function __gmpz_tdiv_r
+[value] using specification for function __gmpz_init_set_ui
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
index 57166c474fd15aaa224462af9dde64f7aef7a41c..58d0a4552754f585698881064f2a9b755ea189d9 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
@@ -21,7 +21,6 @@
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_add
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:53:[value] warning: function __gmpz_init_set: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
index 5b573d17ea2deb3890abba2e07add5ef55474785..bbd8afb45e9bffb7591bc8f7933b07b04c0f931d 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
@@ -15,7 +15,6 @@
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_neg
[value] done for function main
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 edfa526c381617674a5c0cb5f1cd8f657af28dc6..9ccdc0c34c585bf8a8bb94b6cffe0557c979b407 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
@@ -18,13 +18,13 @@ int main(void)
__e_acsl_assert(0 != ~ 0,(char *)"Assertion",(char *)"main",
(char *)"0 != ~0",12);
/*@ assert x+1 ≡ -2; */
- __e_acsl_assert(x + 1 == -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 - 1 == -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 * 3 == -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",
@@ -37,7 +37,7 @@ int main(void)
mpz_t __gen_e_acsl_div;
unsigned long __gen_e_acsl__3;
__gmpz_init_set_str(__gen_e_acsl_,"309485009821345068724781055",10);
- __gmpz_init_set_ui(__gen_e_acsl__2,0UL);
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
__gen_e_acsl_div_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl__2));
__gmpz_init(__gen_e_acsl_div);
@@ -65,7 +65,7 @@ int main(void)
__e_acsl_assert(3 % -2 == 1,(char *)"Assertion",(char *)"main",
(char *)"3%-2 == 1",21);
/*@ assert ((x*2+(3+y))-4)+(x-y) ≡ -10; */
- __e_acsl_assert(((x * 2 + (3 + y)) - 4) + (x - y) == -10,
+ __e_acsl_assert(((x * 2L + (3L + y)) - 4L) + (x - y) == -10L,
(char *)"Assertion",(char *)"main",
(char *)"((x*2+(3+y))-4)+(x-y) == -10",23);
/*@ assert (0≡1) ≡ !(0≡0); */
@@ -99,12 +99,12 @@ int main(void)
mpz_t __gen_e_acsl_div_2;
unsigned long __gen_e_acsl__7;
__gmpz_init_set_si(__gen_e_acsl_z,z);
- __gmpz_init_set_ui(__gen_e_acsl__4,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__4,1L);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)(__gen_e_acsl_z),
(__mpz_struct const *)(__gen_e_acsl__4));
- __gmpz_init_set_si(__gen_e_acsl__5,y - (long)123456789123456789);
- __gmpz_init_set_ui(__gen_e_acsl__6,0UL);
+ __gmpz_init_set_si(__gen_e_acsl__5,y - 123456789123456789L);
+ __gmpz_init_set_si(__gen_e_acsl__6,0L);
__gen_e_acsl_div_guard_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__5),
(__mpz_struct const *)(__gen_e_acsl__6));
__gmpz_init(__gen_e_acsl_div_2);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
index 877cce249c7dbead6b917302bb4bb11b8b4003ff..9ceb2760f14caf855b432548659426a2f6acf317 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
@@ -14,7 +14,7 @@ int main(void)
mpz_t __gen_e_acsl_neg;
mpz_t __gen_e_acsl_x;
int __gen_e_acsl_eq;
- __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)3);
+ __gmpz_init_set_si(__gen_e_acsl_,3L);
__gmpz_init(__gen_e_acsl_neg);
__gmpz_neg(__gen_e_acsl_neg,(__mpz_struct const *)(__gen_e_acsl_));
__gmpz_init_set_si(__gen_e_acsl_x,(long)x);
@@ -33,7 +33,7 @@ int main(void)
mpz_t __gen_e_acsl_neg_2;
int __gen_e_acsl_eq_2;
__gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
- __gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)3);
+ __gmpz_init_set_si(__gen_e_acsl__2,3L);
__gmpz_init(__gen_e_acsl_neg_2);
__gmpz_neg(__gen_e_acsl_neg_2,(__mpz_struct const *)(__gen_e_acsl__2));
__gen_e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_2),
@@ -49,7 +49,7 @@ int main(void)
mpz_t __gen_e_acsl__3;
mpz_t __gen_e_acsl_bnot;
int __gen_e_acsl_ne;
- __gmpz_init_set_ui(__gen_e_acsl__3,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl__3,0L);
__gmpz_init(__gen_e_acsl_bnot);
__gmpz_com(__gen_e_acsl_bnot,(__mpz_struct const *)(__gen_e_acsl__3));
__gen_e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__3),
@@ -68,11 +68,11 @@ int main(void)
mpz_t __gen_e_acsl_neg_3;
int __gen_e_acsl_eq_3;
__gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
- __gmpz_init_set_ui(__gen_e_acsl__4,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__4,1L);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)(__gen_e_acsl_x_3),
(__mpz_struct const *)(__gen_e_acsl__4));
- __gmpz_init_set_ui(__gen_e_acsl__5,(unsigned long)2);
+ __gmpz_init_set_si(__gen_e_acsl__5,2L);
__gmpz_init(__gen_e_acsl_neg_3);
__gmpz_neg(__gen_e_acsl_neg_3,(__mpz_struct const *)(__gen_e_acsl__5));
__gen_e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_add),
@@ -94,11 +94,11 @@ int main(void)
mpz_t __gen_e_acsl_neg_4;
int __gen_e_acsl_eq_4;
__gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
- __gmpz_init_set_ui(__gen_e_acsl__6,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__6,1L);
__gmpz_init(__gen_e_acsl_sub);
__gmpz_sub(__gen_e_acsl_sub,(__mpz_struct const *)(__gen_e_acsl_x_4),
(__mpz_struct const *)(__gen_e_acsl__6));
- __gmpz_init_set_ui(__gen_e_acsl__7,(unsigned long)4);
+ __gmpz_init_set_si(__gen_e_acsl__7,4L);
__gmpz_init(__gen_e_acsl_neg_4);
__gmpz_neg(__gen_e_acsl_neg_4,(__mpz_struct const *)(__gen_e_acsl__7));
__gen_e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_sub),
@@ -120,11 +120,11 @@ int main(void)
mpz_t __gen_e_acsl_neg_5;
int __gen_e_acsl_eq_5;
__gmpz_init_set_si(__gen_e_acsl_x_5,(long)x);
- __gmpz_init_set_ui(__gen_e_acsl__8,(unsigned long)3);
+ __gmpz_init_set_si(__gen_e_acsl__8,3L);
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,(__mpz_struct const *)(__gen_e_acsl_x_5),
(__mpz_struct const *)(__gen_e_acsl__8));
- __gmpz_init_set_ui(__gen_e_acsl__9,(unsigned long)9);
+ __gmpz_init_set_si(__gen_e_acsl__9,9L);
__gmpz_init(__gen_e_acsl_neg_5);
__gmpz_neg(__gen_e_acsl_neg_5,(__mpz_struct const *)(__gen_e_acsl__9));
__gen_e_acsl_eq_5 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_mul),
@@ -148,8 +148,8 @@ int main(void)
mpz_t __gen_e_acsl_neg_6;
int __gen_e_acsl_eq_6;
__gmpz_init_set_si(__gen_e_acsl_x_6,(long)x);
- __gmpz_init_set_ui(__gen_e_acsl__10,(unsigned long)3);
- __gmpz_init_set_ui(__gen_e_acsl__11,0UL);
+ __gmpz_init_set_si(__gen_e_acsl__10,3L);
+ __gmpz_init_set_si(__gen_e_acsl__11,0L);
__gen_e_acsl_div_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__10),
(__mpz_struct const *)(__gen_e_acsl__11));
__gmpz_init(__gen_e_acsl_div);
@@ -158,7 +158,7 @@ int main(void)
(char *)"main",(char *)"3 == 0",17);
__gmpz_tdiv_q(__gen_e_acsl_div,(__mpz_struct const *)(__gen_e_acsl_x_6),
(__mpz_struct const *)(__gen_e_acsl__10));
- __gmpz_init_set_ui(__gen_e_acsl__12,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__12,1L);
__gmpz_init(__gen_e_acsl_neg_6);
__gmpz_neg(__gen_e_acsl_neg_6,(__mpz_struct const *)(__gen_e_acsl__12));
__gen_e_acsl_eq_6 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_div),
@@ -181,7 +181,7 @@ int main(void)
mpz_t __gen_e_acsl__15;
int __gen_e_acsl_eq_7;
__gmpz_init_set_str(__gen_e_acsl__13,"309485009821345068724781055",10);
- __gmpz_init_set_ui(__gen_e_acsl__14,0UL);
+ __gmpz_init_set_si(__gen_e_acsl__14,0L);
__gen_e_acsl_div_guard_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__13),
(__mpz_struct const *)(__gen_e_acsl__14));
__gmpz_init(__gen_e_acsl_div_2);
@@ -192,7 +192,7 @@ int main(void)
__gmpz_tdiv_q(__gen_e_acsl_div_2,
(__mpz_struct const *)(__gen_e_acsl__13),
(__mpz_struct const *)(__gen_e_acsl__13));
- __gmpz_init_set_ui(__gen_e_acsl__15,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__15,1L);
__gen_e_acsl_eq_7 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_div_2),
(__mpz_struct const *)(__gen_e_acsl__15));
__e_acsl_assert(__gen_e_acsl_eq_7 == 0,(char *)"Assertion",
@@ -215,8 +215,8 @@ int main(void)
mpz_t __gen_e_acsl_neg_7;
int __gen_e_acsl_eq_8;
__gmpz_init_set_si(__gen_e_acsl_x_7,(long)x);
- __gmpz_init_set_ui(__gen_e_acsl__16,(unsigned long)2);
- __gmpz_init_set_ui(__gen_e_acsl__17,0UL);
+ __gmpz_init_set_si(__gen_e_acsl__16,2L);
+ __gmpz_init_set_si(__gen_e_acsl__17,0L);
__gen_e_acsl_mod_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__16),
(__mpz_struct const *)(__gen_e_acsl__17));
__gmpz_init(__gen_e_acsl_mod);
@@ -225,7 +225,7 @@ int main(void)
(char *)"main",(char *)"2 == 0",19);
__gmpz_tdiv_r(__gen_e_acsl_mod,(__mpz_struct const *)(__gen_e_acsl_x_7),
(__mpz_struct const *)(__gen_e_acsl__16));
- __gmpz_init_set_ui(__gen_e_acsl__18,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__18,1L);
__gmpz_init(__gen_e_acsl_neg_7);
__gmpz_neg(__gen_e_acsl_neg_7,(__mpz_struct const *)(__gen_e_acsl__18));
__gen_e_acsl_eq_8 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_mod),
@@ -251,13 +251,13 @@ int main(void)
mpz_t __gen_e_acsl__22;
mpz_t __gen_e_acsl_neg_10;
int __gen_e_acsl_eq_9;
- __gmpz_init_set_ui(__gen_e_acsl__19,(unsigned long)3);
+ __gmpz_init_set_si(__gen_e_acsl__19,3L);
__gmpz_init(__gen_e_acsl_neg_8);
__gmpz_neg(__gen_e_acsl_neg_8,(__mpz_struct const *)(__gen_e_acsl__19));
- __gmpz_init_set_ui(__gen_e_acsl__20,(unsigned long)2);
+ __gmpz_init_set_si(__gen_e_acsl__20,2L);
__gmpz_init(__gen_e_acsl_neg_9);
__gmpz_neg(__gen_e_acsl_neg_9,(__mpz_struct const *)(__gen_e_acsl__20));
- __gmpz_init_set_ui(__gen_e_acsl__21,0UL);
+ __gmpz_init_set_si(__gen_e_acsl__21,0L);
__gen_e_acsl_mod_guard_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_neg_9),
(__mpz_struct const *)(__gen_e_acsl__21));
__gmpz_init(__gen_e_acsl_mod_2);
@@ -267,7 +267,7 @@ int main(void)
__gmpz_tdiv_r(__gen_e_acsl_mod_2,
(__mpz_struct const *)(__gen_e_acsl_neg_8),
(__mpz_struct const *)(__gen_e_acsl_neg_9));
- __gmpz_init_set_ui(__gen_e_acsl__22,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__22,1L);
__gmpz_init(__gen_e_acsl_neg_10);
__gmpz_neg(__gen_e_acsl_neg_10,(__mpz_struct const *)(__gen_e_acsl__22));
__gen_e_acsl_eq_9 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_mod_2),
@@ -293,11 +293,11 @@ int main(void)
mpz_t __gen_e_acsl_mod_3;
mpz_t __gen_e_acsl__26;
int __gen_e_acsl_eq_10;
- __gmpz_init_set_ui(__gen_e_acsl__23,(unsigned long)3);
- __gmpz_init_set_ui(__gen_e_acsl__24,(unsigned long)2);
+ __gmpz_init_set_si(__gen_e_acsl__23,3L);
+ __gmpz_init_set_si(__gen_e_acsl__24,2L);
__gmpz_init(__gen_e_acsl_neg_11);
__gmpz_neg(__gen_e_acsl_neg_11,(__mpz_struct const *)(__gen_e_acsl__24));
- __gmpz_init_set_ui(__gen_e_acsl__25,0UL);
+ __gmpz_init_set_si(__gen_e_acsl__25,0L);
__gen_e_acsl_mod_guard_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_neg_11),
(__mpz_struct const *)(__gen_e_acsl__25));
__gmpz_init(__gen_e_acsl_mod_3);
@@ -307,7 +307,7 @@ int main(void)
__gmpz_tdiv_r(__gen_e_acsl_mod_3,
(__mpz_struct const *)(__gen_e_acsl__23),
(__mpz_struct const *)(__gen_e_acsl_neg_11));
- __gmpz_init_set_ui(__gen_e_acsl__26,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__26,1L);
__gen_e_acsl_eq_10 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_mod_3),
(__mpz_struct const *)(__gen_e_acsl__26));
__e_acsl_assert(__gen_e_acsl_eq_10 == 0,(char *)"Assertion",
@@ -336,11 +336,11 @@ int main(void)
mpz_t __gen_e_acsl_neg_12;
int __gen_e_acsl_eq_11;
__gmpz_init_set_si(__gen_e_acsl_x_8,(long)x);
- __gmpz_init_set_ui(__gen_e_acsl__27,(unsigned long)2);
+ __gmpz_init_set_si(__gen_e_acsl__27,2L);
__gmpz_init(__gen_e_acsl_mul_2);
__gmpz_mul(__gen_e_acsl_mul_2,(__mpz_struct const *)(__gen_e_acsl_x_8),
(__mpz_struct const *)(__gen_e_acsl__27));
- __gmpz_init_set_ui(__gen_e_acsl__28,(unsigned long)3);
+ __gmpz_init_set_si(__gen_e_acsl__28,3L);
__gmpz_init_set_si(__gen_e_acsl_y,(long)y);
__gmpz_init(__gen_e_acsl_add_2);
__gmpz_add(__gen_e_acsl_add_2,(__mpz_struct const *)(__gen_e_acsl__28),
@@ -348,7 +348,7 @@ int main(void)
__gmpz_init(__gen_e_acsl_add_3);
__gmpz_add(__gen_e_acsl_add_3,(__mpz_struct const *)(__gen_e_acsl_mul_2),
(__mpz_struct const *)(__gen_e_acsl_add_2));
- __gmpz_init_set_ui(__gen_e_acsl__29,(unsigned long)4);
+ __gmpz_init_set_si(__gen_e_acsl__29,4L);
__gmpz_init(__gen_e_acsl_sub_2);
__gmpz_sub(__gen_e_acsl_sub_2,(__mpz_struct const *)(__gen_e_acsl_add_3),
(__mpz_struct const *)(__gen_e_acsl__29));
@@ -358,7 +358,7 @@ int main(void)
__gmpz_init(__gen_e_acsl_add_4);
__gmpz_add(__gen_e_acsl_add_4,(__mpz_struct const *)(__gen_e_acsl_sub_2),
(__mpz_struct const *)(__gen_e_acsl_sub_3));
- __gmpz_init_set_ui(__gen_e_acsl__30,(unsigned long)10);
+ __gmpz_init_set_si(__gen_e_acsl__30,10L);
__gmpz_init(__gen_e_acsl_neg_12);
__gmpz_neg(__gen_e_acsl_neg_12,(__mpz_struct const *)(__gen_e_acsl__30));
__gen_e_acsl_eq_11 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_add_4),
@@ -390,8 +390,8 @@ int main(void)
int __gen_e_acsl_not;
mpz_t __gen_e_acsl__35;
int __gen_e_acsl_eq_14;
- __gmpz_init_set_ui(__gen_e_acsl__31,(unsigned long)0);
- __gmpz_init_set_ui(__gen_e_acsl__32,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__31,0L);
+ __gmpz_init_set_si(__gen_e_acsl__32,1L);
__gen_e_acsl_eq_12 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__31),
(__mpz_struct const *)(__gen_e_acsl__32));
__gmpz_init_set_si(__gen_e_acsl__33,(long)(__gen_e_acsl_eq_12 == 0));
@@ -421,8 +421,8 @@ int main(void)
int __gen_e_acsl_gt;
mpz_t __gen_e_acsl__39;
int __gen_e_acsl_eq_15;
- __gmpz_init_set_ui(__gen_e_acsl__36,(unsigned long)0);
- __gmpz_init_set_ui(__gen_e_acsl__37,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__36,0L);
+ __gmpz_init_set_si(__gen_e_acsl__37,1L);
__gmpz_init(__gen_e_acsl_neg_13);
__gmpz_neg(__gen_e_acsl_neg_13,(__mpz_struct const *)(__gen_e_acsl__37));
__gen_e_acsl_le = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__36),
@@ -451,8 +451,8 @@ int main(void)
int __gen_e_acsl_le_2;
mpz_t __gen_e_acsl__43;
int __gen_e_acsl_eq_16;
- __gmpz_init_set_ui(__gen_e_acsl__40,(unsigned long)0);
- __gmpz_init_set_ui(__gen_e_acsl__41,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__40,0L);
+ __gmpz_init_set_si(__gen_e_acsl__41,1L);
__gmpz_init(__gen_e_acsl_neg_14);
__gmpz_neg(__gen_e_acsl_neg_14,(__mpz_struct const *)(__gen_e_acsl__41));
__gen_e_acsl_ge = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__40),
@@ -482,8 +482,8 @@ int main(void)
int __gen_e_acsl_not_2;
mpz_t __gen_e_acsl__48;
int __gen_e_acsl_eq_17;
- __gmpz_init_set_ui(__gen_e_acsl__44,(unsigned long)0);
- __gmpz_init_set_ui(__gen_e_acsl__45,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__44,0L);
+ __gmpz_init_set_si(__gen_e_acsl__45,1L);
__gen_e_acsl_ne_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__44),
(__mpz_struct const *)(__gen_e_acsl__45));
__gmpz_init_set_si(__gen_e_acsl__46,(long)(__gen_e_acsl_ne_2 != 0));
@@ -514,11 +514,11 @@ int main(void)
int __gen_e_acsl_not_3;
mpz_t __gen_e_acsl__53;
int __gen_e_acsl_eq_18;
- __gmpz_init_set_ui(__gen_e_acsl__49,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl__49,0L);
__gen_e_acsl_ne_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__49),
(__mpz_struct const *)(__gen_e_acsl__49));
__gmpz_init_set_si(__gen_e_acsl__50,(long)(__gen_e_acsl_ne_4 != 0));
- __gmpz_init_set_ui(__gen_e_acsl__51,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__51,1L);
__gen_e_acsl_ne_5 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__51),
(__mpz_struct const *)(__gen_e_acsl__49));
__gmpz_init_set_si(__gen_e_acsl__52,(long)(__gen_e_acsl_ne_5 != 0));
@@ -544,9 +544,9 @@ int main(void)
mpz_t __gen_e_acsl_div_3;
mpz_t __gen_e_acsl__56;
int __gen_e_acsl_eq_19;
- __gmpz_init_set_ui(__gen_e_acsl__54,(unsigned long)4);
+ __gmpz_init_set_si(__gen_e_acsl__54,4L);
__gmpz_init_set_si(__gen_e_acsl_y_2,(long)y);
- __gmpz_init_set_ui(__gen_e_acsl__55,0UL);
+ __gmpz_init_set_si(__gen_e_acsl__55,0L);
__gen_e_acsl_div_guard_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_y_2),
(__mpz_struct const *)(__gen_e_acsl__55));
__gmpz_init(__gen_e_acsl_div_3);
@@ -556,7 +556,7 @@ int main(void)
__gmpz_tdiv_q(__gen_e_acsl_div_3,
(__mpz_struct const *)(__gen_e_acsl__54),
(__mpz_struct const *)(__gen_e_acsl_y_2));
- __gmpz_init_set_ui(__gen_e_acsl__56,(unsigned long)2);
+ __gmpz_init_set_si(__gen_e_acsl__56,2L);
__gen_e_acsl_eq_19 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_div_3),
(__mpz_struct const *)(__gen_e_acsl__56));
__e_acsl_assert(__gen_e_acsl_eq_19 == 0,(char *)"Assertion",
@@ -580,17 +580,17 @@ int main(void)
mpz_t __gen_e_acsl_div_4;
mpz_t __gen_e_acsl_add_6;
int __gen_e_acsl_eq_20;
- __gmpz_init_set_ui(__gen_e_acsl__57,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__57,1L);
__gmpz_init_set_si(__gen_e_acsl_z,z);
__gmpz_init(__gen_e_acsl_add_5);
__gmpz_add(__gen_e_acsl_add_5,(__mpz_struct const *)(__gen_e_acsl_z),
(__mpz_struct const *)(__gen_e_acsl__57));
__gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
- __gmpz_init_set_ui(__gen_e_acsl__58,123456789123456789);
+ __gmpz_init_set_ui(__gen_e_acsl__58,123456789123456789UL);
__gmpz_init(__gen_e_acsl_sub_4);
__gmpz_sub(__gen_e_acsl_sub_4,(__mpz_struct const *)(__gen_e_acsl_y_3),
(__mpz_struct const *)(__gen_e_acsl__58));
- __gmpz_init_set_ui(__gen_e_acsl__59,0UL);
+ __gmpz_init_set_si(__gen_e_acsl__59,0L);
__gen_e_acsl_div_guard_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_sub_4),
(__mpz_struct const *)(__gen_e_acsl__59));
__gmpz_init(__gen_e_acsl_div_4);
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 4e8e4913f1bb8b1323ed3a7f07257ea15977f849..a3e45b4666eae33e8c90343149e96681333c9ca2 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_array.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_array.c
@@ -21,10 +21,10 @@ int main(void)
}
}
/*@ assert T1[0] ≡ T2[0]; */
- __e_acsl_assert(T1[0] == T2[0],(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(T1[0UL] == T2[0UL],(char *)"Assertion",(char *)"main",
(char *)"T1[0] == T2[0]",13);
/*@ assert T1[1] ≢ T2[1]; */
- __e_acsl_assert(T1[1] != T2[1],(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(T1[1UL] != T2[1UL],(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 04b89745d9373be092a0147bbf47e337c976fa37..8b57d232ff6f7e266949eb4ff2c34cf98f97c0db 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_array2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_array2.c
@@ -25,8 +25,8 @@ int main(void)
mpz_t __gen_e_acsl_;
mpz_t __gen_e_acsl__2;
int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_,(long)T1[0]);
- __gmpz_init_set_si(__gen_e_acsl__2,(long)T2[0]);
+ __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));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
@@ -39,8 +39,8 @@ int main(void)
mpz_t __gen_e_acsl__3;
mpz_t __gen_e_acsl__4;
int __gen_e_acsl_ne;
- __gmpz_init_set_si(__gen_e_acsl__3,(long)T1[1]);
- __gmpz_init_set_si(__gen_e_acsl__4,(long)T2[1]);
+ __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));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
index f264d7d235cf80e9d1702904d67278f13a5ed2a6..a59759c3885b81a338b3313783d76852c40890e5 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -129,7 +129,7 @@ int main(void)
__e_acsl_store_block((void *)(& __gen_e_acsl_at_3),4UL);
__gen_e_acsl_at_3 = x;
__e_acsl_store_block((void *)(& __gen_e_acsl_at_2),8UL);
- __gen_e_acsl_at_2 = x + 1;
+ __gen_e_acsl_at_2 = x + 1L;
__e_acsl_store_block((void *)(& __gen_e_acsl_at),4UL);
__gen_e_acsl_at = x;
/*@ assert x ≡ 0; */
@@ -144,10 +144,10 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_at == 0,(char *)"Assertion",(char *)"main",
(char *)"\\at(x,L) == 0",48);
/*@ assert \at(x+1,L) ≡ 1; */
- __e_acsl_assert(__gen_e_acsl_at_2 == 1,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(__gen_e_acsl_at_2 == 1L,(char *)"Assertion",(char *)"main",
(char *)"\\at(x+1,L) == 1",49);
/*@ assert \at(x,L)+1 ≡ 1; */
- __e_acsl_assert(__gen_e_acsl_at_3 + 1 == 1,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_at_3 + 1L == 1L,(char *)"Assertion",
(char *)"main",(char *)"\\at(x,L)+1 == 1",50);
g(t,& x);
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
index efe0a01ae117a0a7010fd4f69d0b64c2786abc5b..5c2f9f5687e1eb9ade14568536f9b763ec593005 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
@@ -37,7 +37,7 @@ void f(void)
{
mpz_t __gen_e_acsl_;
int __gen_e_acsl_eq;
- __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_at),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"f",
@@ -48,7 +48,7 @@ void f(void)
{
mpz_t __gen_e_acsl__2;
int __gen_e_acsl_eq_2;
- __gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__2,1L);
__gen_e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_at_2),
(__mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"f",
@@ -61,7 +61,7 @@ void f(void)
mpz_t __gen_e_acsl__3;
int __gen_e_acsl_eq_3;
__gmpz_init_set_si(__gen_e_acsl_A_3,(long)A);
- __gmpz_init_set_ui(__gen_e_acsl__3,(unsigned long)2);
+ __gmpz_init_set_si(__gen_e_acsl__3,2L);
__gen_e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_A_3),
(__mpz_struct const *)(__gen_e_acsl__3));
__e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",(char *)"f",
@@ -73,7 +73,7 @@ void f(void)
{
mpz_t __gen_e_acsl__4;
int __gen_e_acsl_eq_4;
- __gmpz_init_set_ui(__gen_e_acsl__4,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl__4,0L);
__gen_e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_at_3),
(__mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",(char *)"f",
@@ -142,7 +142,7 @@ void g(int *p, int *q)
{
mpz_t __gen_e_acsl__2;
int __gen_e_acsl_eq;
- __gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)2);
+ __gmpz_init_set_si(__gen_e_acsl__2,2L);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_at_2),
(__mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"g",
@@ -156,7 +156,7 @@ void g(int *p, int *q)
mpz_t __gen_e_acsl__4;
int __gen_e_acsl_eq_2;
__gmpz_init_set_si(__gen_e_acsl__3,(long)*(p + __gen_e_acsl_at_3));
- __gmpz_init_set_ui(__gen_e_acsl__4,(unsigned long)2);
+ __gmpz_init_set_si(__gen_e_acsl__4,2L);
__gen_e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__3),
(__mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"g",
@@ -206,7 +206,7 @@ int main(void)
mpz_t __gen_e_acsl__3;
mpz_t __gen_e_acsl_add;
__gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
- __gmpz_init_set_ui(__gen_e_acsl__3,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__3,1L);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)(__gen_e_acsl_x_3),
(__mpz_struct const *)(__gen_e_acsl__3));
@@ -229,7 +229,7 @@ int main(void)
mpz_t __gen_e_acsl_;
int __gen_e_acsl_eq;
__gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",
@@ -246,7 +246,7 @@ int main(void)
{
mpz_t __gen_e_acsl__2;
int __gen_e_acsl_eq_2;
- __gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
__gen_e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_at),
(__mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
@@ -257,7 +257,7 @@ int main(void)
{
mpz_t __gen_e_acsl__4;
int __gen_e_acsl_eq_3;
- __gmpz_init_set_ui(__gen_e_acsl__4,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__4,1L);
__gen_e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_at_2),
(__mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
@@ -269,7 +269,7 @@ int main(void)
mpz_t __gen_e_acsl__5;
mpz_t __gen_e_acsl_add_2;
int __gen_e_acsl_eq_4;
- __gmpz_init_set_ui(__gen_e_acsl__5,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__5,1L);
__gmpz_init(__gen_e_acsl_add_2);
__gmpz_add(__gen_e_acsl_add_2,(__mpz_struct const *)(__gen_e_acsl_at),
(__mpz_struct const *)(__gen_e_acsl__5));
@@ -334,7 +334,7 @@ void __gen_e_acsl_f(void)
__gmpz_init_set(__gen_e_acsl_at,(__mpz_struct const *)(__gen_e_acsl_A));
__gmpz_clear(__gen_e_acsl_A);
}
- __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)3);
+ __gmpz_init_set_si(__gen_e_acsl_,3L);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_at),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Postcondition",(char *)"f",
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 afa708400e806a414bf3eb1884ba615b09f56e15..f3859df710c5ee042defc15cf8f8d46d6767486e 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_cast.c
@@ -16,14 +16,14 @@ int main(void)
__e_acsl_assert(y == 0,(char *)"Assertion",(char *)"main",
(char *)"y == (int)0",13);
/*@ assert (unsigned int)y ≡ (unsigned int)0; */
- __e_acsl_assert((unsigned int)y == 0,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert((unsigned int)y == 0U,(char *)"Assertion",(char *)"main",
(char *)"(unsigned int)y == (unsigned int)0",14);
/*@ assert y ≢ (int)0xfffffffffffffff; */
- __e_acsl_assert(y != (int)0xfffffffffffffff,(char *)"Assertion",
- (char *)"main",(char *)"y != (int)0xfffffffffffffff",17);
+ __e_acsl_assert(y != -1,(char *)"Assertion",(char *)"main",
+ (char *)"y != (int)0xfffffffffffffff",17);
/*@ assert (unsigned int)y ≢ (unsigned int)0xfffffffffffffff; */
- __e_acsl_assert((unsigned int)y != (unsigned int)0xfffffffffffffff,
- (char *)"Assertion",(char *)"main",
+ __e_acsl_assert((unsigned int)y != 4294967295U,(char *)"Assertion",
+ (char *)"main",
(char *)"(unsigned int)y != (unsigned int)0xfffffffffffffff",
18);
__retres = 0;
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 67a87635204c186bb1a91d24dd4f17faf5bbcf7d..f29b5dd326373504c968abef22018576826eaf99 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_cast2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_cast2.c
@@ -52,7 +52,7 @@ int main(void)
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_ui(__gen_e_acsl__3,(unsigned long)0);
+ __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),
@@ -75,7 +75,7 @@ int main(void)
__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));
__gmpz_init_set_ui(__gen_e_acsl__5,__gen_e_acsl_cast_4);
- __gmpz_init_set_ui(__gen_e_acsl__6,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl__6,0L);
__gen_e_acsl_cast_5 = __gmpz_get_ui((__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),
@@ -96,7 +96,7 @@ int main(void)
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,0xfffffffffffffff);
+ __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),
@@ -119,7 +119,7 @@ int main(void)
__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));
__gmpz_init_set_ui(__gen_e_acsl__10,__gen_e_acsl_cast_7);
- __gmpz_init_set_ui(__gen_e_acsl__11,0xfffffffffffffff);
+ __gmpz_init_set_ui(__gen_e_acsl__11,1152921504606846975UL);
__gen_e_acsl_cast_8 = __gmpz_get_ui((__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),
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 53c13302ebd1f22a80fdaa894e4bde39eb9cbd90..8b99036ca25f1864c3f9f79ec7f689278753f65b 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
@@ -34,7 +34,7 @@ int main(void)
__e_acsl_assert(123 >= 12,(char *)"Assertion",(char *)"main",
(char *)"123 >= 12",18);
/*@ assert 0xff ≡ 0xff; */
- __e_acsl_assert(0xff == 0xff,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(255 == 255,(char *)"Assertion",(char *)"main",
(char *)"0xff == 0xff",19);
/*@ assert 1 ≢ 2; */
__e_acsl_assert(1 != 2,(char *)"Assertion",(char *)"main",(char *)"1 != 2",
@@ -52,7 +52,7 @@ int main(void)
__e_acsl_assert(123 >= -12,(char *)"Assertion",(char *)"main",
(char *)"123 >= -12",25);
/*@ assert -0xff ≡ -0xff; */
- __e_acsl_assert(-0xff == -0xff,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(-255 == -255,(char *)"Assertion",(char *)"main",
(char *)"-0xff == -0xff",26);
/*@ assert 1 ≢ -2; */
__e_acsl_assert(1 != -2,(char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
index 10820363da0f19523f565acadd7f9e6c5939079d..f6f6cc7d3a0fd45127ffc79a9b9ecac6a9a60457 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
@@ -41,7 +41,7 @@ int main(void)
mpz_t __gen_e_acsl_;
int __gen_e_acsl_le;
__gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
- __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
__gen_e_acsl_le = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_3),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_le <= 0,(char *)"Assertion",(char *)"main",
@@ -55,7 +55,7 @@ int main(void)
mpz_t __gen_e_acsl__2;
int __gen_e_acsl_ge;
__gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
- __gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__2,1L);
__gen_e_acsl_ge = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_y_3),
(__mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_ge >= 0,(char *)"Assertion",(char *)"main",
@@ -72,8 +72,8 @@ int main(void)
mpz_t __gen_e_acsl__3;
mpz_t __gen_e_acsl__4;
int __gen_e_acsl_lt_2;
- __gmpz_init_set_ui(__gen_e_acsl__3,(unsigned long)5);
- __gmpz_init_set_ui(__gen_e_acsl__4,(unsigned long)18);
+ __gmpz_init_set_si(__gen_e_acsl__3,5L);
+ __gmpz_init_set_si(__gen_e_acsl__4,18L);
__gen_e_acsl_lt_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__3),
(__mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_lt_2 < 0,(char *)"Assertion",(char *)"main",
@@ -86,8 +86,8 @@ int main(void)
mpz_t __gen_e_acsl__5;
mpz_t __gen_e_acsl__6;
int __gen_e_acsl_gt_2;
- __gmpz_init_set_ui(__gen_e_acsl__5,(unsigned long)32);
- __gmpz_init_set_ui(__gen_e_acsl__6,(unsigned long)3);
+ __gmpz_init_set_si(__gen_e_acsl__5,32L);
+ __gmpz_init_set_si(__gen_e_acsl__6,3L);
__gen_e_acsl_gt_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__5),
(__mpz_struct const *)(__gen_e_acsl__6));
__e_acsl_assert(__gen_e_acsl_gt_2 > 0,(char *)"Assertion",(char *)"main",
@@ -100,8 +100,8 @@ int main(void)
mpz_t __gen_e_acsl__7;
mpz_t __gen_e_acsl__8;
int __gen_e_acsl_le_2;
- __gmpz_init_set_ui(__gen_e_acsl__7,(unsigned long)12);
- __gmpz_init_set_ui(__gen_e_acsl__8,(unsigned long)13);
+ __gmpz_init_set_si(__gen_e_acsl__7,12L);
+ __gmpz_init_set_si(__gen_e_acsl__8,13L);
__gen_e_acsl_le_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__7),
(__mpz_struct const *)(__gen_e_acsl__8));
__e_acsl_assert(__gen_e_acsl_le_2 <= 0,(char *)"Assertion",
@@ -114,8 +114,8 @@ int main(void)
mpz_t __gen_e_acsl__9;
mpz_t __gen_e_acsl__10;
int __gen_e_acsl_ge_2;
- __gmpz_init_set_ui(__gen_e_acsl__9,(unsigned long)123);
- __gmpz_init_set_ui(__gen_e_acsl__10,(unsigned long)12);
+ __gmpz_init_set_si(__gen_e_acsl__9,123L);
+ __gmpz_init_set_si(__gen_e_acsl__10,12L);
__gen_e_acsl_ge_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__9),
(__mpz_struct const *)(__gen_e_acsl__10));
__e_acsl_assert(__gen_e_acsl_ge_2 >= 0,(char *)"Assertion",
@@ -127,7 +127,7 @@ int main(void)
{
mpz_t __gen_e_acsl__11;
int __gen_e_acsl_eq;
- __gmpz_init_set_ui(__gen_e_acsl__11,(unsigned long)0xff);
+ __gmpz_init_set_si(__gen_e_acsl__11,255L);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__11),
(__mpz_struct const *)(__gen_e_acsl__11));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
@@ -139,8 +139,8 @@ int main(void)
mpz_t __gen_e_acsl__12;
mpz_t __gen_e_acsl__13;
int __gen_e_acsl_ne;
- __gmpz_init_set_ui(__gen_e_acsl__12,(unsigned long)1);
- __gmpz_init_set_ui(__gen_e_acsl__13,(unsigned long)2);
+ __gmpz_init_set_si(__gen_e_acsl__12,1L);
+ __gmpz_init_set_si(__gen_e_acsl__13,2L);
__gen_e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__12),
(__mpz_struct const *)(__gen_e_acsl__13));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
@@ -154,10 +154,10 @@ int main(void)
mpz_t __gen_e_acsl_neg;
mpz_t __gen_e_acsl__15;
int __gen_e_acsl_lt_3;
- __gmpz_init_set_ui(__gen_e_acsl__14,(unsigned long)5);
+ __gmpz_init_set_si(__gen_e_acsl__14,5L);
__gmpz_init(__gen_e_acsl_neg);
__gmpz_neg(__gen_e_acsl_neg,(__mpz_struct const *)(__gen_e_acsl__14));
- __gmpz_init_set_ui(__gen_e_acsl__15,(unsigned long)18);
+ __gmpz_init_set_si(__gen_e_acsl__15,18L);
__gen_e_acsl_lt_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_neg),
(__mpz_struct const *)(__gen_e_acsl__15));
__e_acsl_assert(__gen_e_acsl_lt_3 < 0,(char *)"Assertion",(char *)"main",
@@ -172,8 +172,8 @@ int main(void)
mpz_t __gen_e_acsl__17;
mpz_t __gen_e_acsl_neg_2;
int __gen_e_acsl_gt_3;
- __gmpz_init_set_ui(__gen_e_acsl__16,(unsigned long)32);
- __gmpz_init_set_ui(__gen_e_acsl__17,(unsigned long)3);
+ __gmpz_init_set_si(__gen_e_acsl__16,32L);
+ __gmpz_init_set_si(__gen_e_acsl__17,3L);
__gmpz_init(__gen_e_acsl_neg_2);
__gmpz_neg(__gen_e_acsl_neg_2,(__mpz_struct const *)(__gen_e_acsl__17));
__gen_e_acsl_gt_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__16),
@@ -190,10 +190,10 @@ int main(void)
mpz_t __gen_e_acsl_neg_3;
mpz_t __gen_e_acsl__19;
int __gen_e_acsl_le_3;
- __gmpz_init_set_ui(__gen_e_acsl__18,(unsigned long)12);
+ __gmpz_init_set_si(__gen_e_acsl__18,12L);
__gmpz_init(__gen_e_acsl_neg_3);
__gmpz_neg(__gen_e_acsl_neg_3,(__mpz_struct const *)(__gen_e_acsl__18));
- __gmpz_init_set_ui(__gen_e_acsl__19,(unsigned long)13);
+ __gmpz_init_set_si(__gen_e_acsl__19,13L);
__gen_e_acsl_le_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_neg_3),
(__mpz_struct const *)(__gen_e_acsl__19));
__e_acsl_assert(__gen_e_acsl_le_3 <= 0,(char *)"Assertion",
@@ -208,8 +208,8 @@ int main(void)
mpz_t __gen_e_acsl__21;
mpz_t __gen_e_acsl_neg_4;
int __gen_e_acsl_ge_3;
- __gmpz_init_set_ui(__gen_e_acsl__20,(unsigned long)123);
- __gmpz_init_set_ui(__gen_e_acsl__21,(unsigned long)12);
+ __gmpz_init_set_si(__gen_e_acsl__20,123L);
+ __gmpz_init_set_si(__gen_e_acsl__21,12L);
__gmpz_init(__gen_e_acsl_neg_4);
__gmpz_neg(__gen_e_acsl_neg_4,(__mpz_struct const *)(__gen_e_acsl__21));
__gen_e_acsl_ge_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__20),
@@ -225,7 +225,7 @@ int main(void)
mpz_t __gen_e_acsl__22;
mpz_t __gen_e_acsl_neg_5;
int __gen_e_acsl_eq_2;
- __gmpz_init_set_ui(__gen_e_acsl__22,(unsigned long)0xff);
+ __gmpz_init_set_si(__gen_e_acsl__22,255L);
__gmpz_init(__gen_e_acsl_neg_5);
__gmpz_neg(__gen_e_acsl_neg_5,(__mpz_struct const *)(__gen_e_acsl__22));
__gen_e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_neg_5),
@@ -241,8 +241,8 @@ int main(void)
mpz_t __gen_e_acsl__24;
mpz_t __gen_e_acsl_neg_6;
int __gen_e_acsl_ne_2;
- __gmpz_init_set_ui(__gen_e_acsl__23,(unsigned long)1);
- __gmpz_init_set_ui(__gen_e_acsl__24,(unsigned long)2);
+ __gmpz_init_set_si(__gen_e_acsl__23,1L);
+ __gmpz_init_set_si(__gen_e_acsl__24,2L);
__gmpz_init(__gen_e_acsl_neg_6);
__gmpz_neg(__gen_e_acsl_neg_6,(__mpz_struct const *)(__gen_e_acsl__24));
__gen_e_acsl_ne_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__23),
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 6c4f43d862a81edebb4f9b8f3dc7ff888a39ab88..0a732f3dd50914ca8dd78f7dc8e3131ab25d2090 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
@@ -12,7 +12,7 @@ int main(void)
__e_acsl_assert(0 != 1,(char *)"Assertion",(char *)"main",(char *)"0 != 1",
8);
/*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */
- __e_acsl_assert(1152921504606846975 == 0xfffffffffffffff,
+ __e_acsl_assert(1152921504606846975UL == 1152921504606846975UL,
(char *)"Assertion",(char *)"main",
(char *)"1152921504606846975 == 0xfffffffffffffff",9);
/*@ assert
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
index 74ca167908edd969cce01f21620081c1db19df3c..36625a20cedd94b9856c579f268255efa09ddb9b 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
@@ -7,7 +7,7 @@ int main(void)
{
mpz_t __gen_e_acsl_;
int __gen_e_acsl_eq;
- __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
@@ -21,8 +21,8 @@ int main(void)
mpz_t __gen_e_acsl__2;
mpz_t __gen_e_acsl__3;
int __gen_e_acsl_ne;
- __gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)0);
- __gmpz_init_set_ui(__gen_e_acsl__3,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init_set_si(__gen_e_acsl__3,1L);
__gen_e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__2),
(__mpz_struct const *)(__gen_e_acsl__3));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
@@ -34,7 +34,7 @@ int main(void)
{
mpz_t __gen_e_acsl__4;
int __gen_e_acsl_eq_2;
- __gmpz_init_set_ui(__gen_e_acsl__4,1152921504606846975);
+ __gmpz_init_set_ui(__gen_e_acsl__4,1152921504606846975UL);
__gen_e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__4),
(__mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
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 78842be2f719f0bdc5cbfcb64929050f67283900..a82eeee300c89084acae75bbe704a1ad52003dbc 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c
@@ -39,17 +39,17 @@ int main(void)
int __gen_e_acsl_mod_guard;
mpz_t __gen_e_acsl_mod;
unsigned long __gen_e_acsl__4;
- __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)2);
+ __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_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_init_set_ui(__gen_e_acsl__2,(unsigned long)1);
+ __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_init_set_ui(__gen_e_acsl__3,0UL);
+ __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));
__gmpz_init(__gen_e_acsl_mod);
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 11dd13abee4e604abef27e30ff4382e5b1ce827c..af00a19e9e5e67004dde13c375597ffc124c084c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c
@@ -39,17 +39,17 @@ int main(void)
int __gen_e_acsl_mod_guard;
mpz_t __gen_e_acsl_mod;
int __gen_e_acsl_eq;
- __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)2);
+ __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_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_init_set_ui(__gen_e_acsl__2,(unsigned long)1);
+ __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_init_set_ui(__gen_e_acsl__3,0UL);
+ __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));
__gmpz_init(__gen_e_acsl_mod);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
index f1e22043fb63a9df8d0b6487ac3d6deaab85f7a1..8ee1e05a971bcdfa474a748f2bc43fb0e952fce0 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
@@ -10,7 +10,7 @@ int main(void)
mpz_t __gen_e_acsl_;
int __gen_e_acsl_eq;
__gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init_set_ui(__gen_e_acsl_,0UL);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
@@ -25,7 +25,7 @@ int main(void)
mpz_t __gen_e_acsl__2;
int __gen_e_acsl_ne;
__gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
- __gmpz_init_set_ui(__gen_e_acsl__2,0UL);
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
__gen_e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_2),
(__mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
index cb4a5be82867bb8d266e9fdaf526dcce1738c15f..adec45af80692c0f34dd94f0a9643c33f8f4e830 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
@@ -10,7 +10,7 @@ int main(void)
__gmpz_init(__gen_e_acsl_x);
{
mpz_t __gen_e_acsl__3;
- __gmpz_init_set_ui(__gen_e_acsl__3,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl__3,0L);
__gmpz_set(__gen_e_acsl_x,(__mpz_struct const *)(__gen_e_acsl__3));
__gmpz_clear(__gen_e_acsl__3);
}
@@ -18,7 +18,7 @@ int main(void)
{
mpz_t __gen_e_acsl__4;
int __gen_e_acsl_le;
- __gmpz_init_set_ui(__gen_e_acsl__4,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__4,1L);
__gen_e_acsl_le = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x),
(__mpz_struct const *)(__gen_e_acsl__4));
if (__gen_e_acsl_le <= 0) ; else break;
@@ -28,14 +28,14 @@ int main(void)
mpz_t __gen_e_acsl_;
int __gen_e_acsl_eq;
int __gen_e_acsl_or;
- __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x),
(__mpz_struct const *)(__gen_e_acsl_));
if (__gen_e_acsl_eq == 0) __gen_e_acsl_or = 1;
else {
mpz_t __gen_e_acsl__2;
int __gen_e_acsl_eq_2;
- __gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__2,1L);
__gen_e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x),
(__mpz_struct const *)(__gen_e_acsl__2));
__gen_e_acsl_or = __gen_e_acsl_eq_2 == 0;
@@ -51,7 +51,7 @@ int main(void)
{
mpz_t __gen_e_acsl__5;
mpz_t __gen_e_acsl_add;
- __gmpz_init_set_ui(__gen_e_acsl__5,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__5,1L);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)(__gen_e_acsl_x),
(__mpz_struct const *)(__gen_e_acsl__5));
@@ -76,8 +76,8 @@ int main(void)
mpz_t __gen_e_acsl__7;
mpz_t __gen_e_acsl__8;
mpz_t __gen_e_acsl_add_2;
- __gmpz_init_set_ui(__gen_e_acsl__7,(unsigned long)0);
- __gmpz_init_set_ui(__gen_e_acsl__8,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__7,0L);
+ __gmpz_init_set_si(__gen_e_acsl__8,1L);
__gmpz_init(__gen_e_acsl_add_2);
__gmpz_add(__gen_e_acsl_add_2,(__mpz_struct const *)(__gen_e_acsl__7),
(__mpz_struct const *)(__gen_e_acsl__8));
@@ -90,7 +90,7 @@ int main(void)
{
mpz_t __gen_e_acsl__9;
int __gen_e_acsl_le_2;
- __gmpz_init_set_ui(__gen_e_acsl__9,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__9,1L);
__gen_e_acsl_le_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_2),
(__mpz_struct const *)(__gen_e_acsl__9));
if (__gen_e_acsl_le_2 <= 0) ; else break;
@@ -99,7 +99,7 @@ int main(void)
{
mpz_t __gen_e_acsl__6;
int __gen_e_acsl_eq_3;
- __gmpz_init_set_ui(__gen_e_acsl__6,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__6,1L);
__gen_e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_2),
(__mpz_struct const *)(__gen_e_acsl__6));
__gmpz_clear(__gen_e_acsl__6);
@@ -112,7 +112,7 @@ int main(void)
{
mpz_t __gen_e_acsl__10;
mpz_t __gen_e_acsl_add_3;
- __gmpz_init_set_ui(__gen_e_acsl__10,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__10,1L);
__gmpz_init(__gen_e_acsl_add_3);
__gmpz_add(__gen_e_acsl_add_3,
(__mpz_struct const *)(__gen_e_acsl_x_2),
@@ -138,8 +138,8 @@ int main(void)
mpz_t __gen_e_acsl__11;
mpz_t __gen_e_acsl__12;
mpz_t __gen_e_acsl_add_4;
- __gmpz_init_set_ui(__gen_e_acsl__11,(unsigned long)0);
- __gmpz_init_set_ui(__gen_e_acsl__12,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__11,0L);
+ __gmpz_init_set_si(__gen_e_acsl__12,1L);
__gmpz_init(__gen_e_acsl_add_4);
__gmpz_add(__gen_e_acsl_add_4,(__mpz_struct const *)(__gen_e_acsl__11),
(__mpz_struct const *)(__gen_e_acsl__12));
@@ -152,7 +152,7 @@ int main(void)
{
mpz_t __gen_e_acsl__13;
int __gen_e_acsl_lt;
- __gmpz_init_set_ui(__gen_e_acsl__13,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__13,1L);
__gen_e_acsl_lt = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_3),
(__mpz_struct const *)(__gen_e_acsl__13));
if (__gen_e_acsl_lt < 0) ; else break;
@@ -166,7 +166,7 @@ int main(void)
{
mpz_t __gen_e_acsl__14;
mpz_t __gen_e_acsl_add_5;
- __gmpz_init_set_ui(__gen_e_acsl__14,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__14,1L);
__gmpz_init(__gen_e_acsl_add_5);
__gmpz_add(__gen_e_acsl_add_5,
(__mpz_struct const *)(__gen_e_acsl_x_3),
@@ -190,7 +190,7 @@ int main(void)
__gmpz_init(__gen_e_acsl_x_4);
{
mpz_t __gen_e_acsl__16;
- __gmpz_init_set_ui(__gen_e_acsl__16,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl__16,0L);
__gmpz_set(__gen_e_acsl_x_4,(__mpz_struct const *)(__gen_e_acsl__16));
__gmpz_clear(__gen_e_acsl__16);
}
@@ -198,7 +198,7 @@ int main(void)
{
mpz_t __gen_e_acsl__17;
int __gen_e_acsl_lt_2;
- __gmpz_init_set_ui(__gen_e_acsl__17,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__17,1L);
__gen_e_acsl_lt_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_4),
(__mpz_struct const *)(__gen_e_acsl__17));
if (__gen_e_acsl_lt_2 < 0) ; else break;
@@ -207,7 +207,7 @@ int main(void)
{
mpz_t __gen_e_acsl__15;
int __gen_e_acsl_eq_4;
- __gmpz_init_set_ui(__gen_e_acsl__15,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl__15,0L);
__gen_e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_4),
(__mpz_struct const *)(__gen_e_acsl__15));
__gmpz_clear(__gen_e_acsl__15);
@@ -220,7 +220,7 @@ int main(void)
{
mpz_t __gen_e_acsl__18;
mpz_t __gen_e_acsl_add_6;
- __gmpz_init_set_ui(__gen_e_acsl__18,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__18,1L);
__gmpz_init(__gen_e_acsl_add_6);
__gmpz_add(__gen_e_acsl_add_6,
(__mpz_struct const *)(__gen_e_acsl_x_4),
@@ -251,7 +251,7 @@ int main(void)
__gmpz_init(__gen_e_acsl_z);
{
mpz_t __gen_e_acsl__25;
- __gmpz_init_set_ui(__gen_e_acsl__25,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl__25,0L);
__gmpz_set(__gen_e_acsl_x_5,(__mpz_struct const *)(__gen_e_acsl__25));
__gmpz_clear(__gen_e_acsl__25);
}
@@ -259,7 +259,7 @@ int main(void)
{
mpz_t __gen_e_acsl__26;
int __gen_e_acsl_lt_4;
- __gmpz_init_set_ui(__gen_e_acsl__26,(unsigned long)2);
+ __gmpz_init_set_si(__gen_e_acsl__26,2L);
__gen_e_acsl_lt_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_5),
(__mpz_struct const *)(__gen_e_acsl__26));
if (__gen_e_acsl_lt_4 < 0) ; else break;
@@ -267,7 +267,7 @@ int main(void)
}
{
mpz_t __gen_e_acsl__22;
- __gmpz_init_set_ui(__gen_e_acsl__22,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl__22,0L);
__gmpz_set(__gen_e_acsl_y,(__mpz_struct const *)(__gen_e_acsl__22));
__gmpz_clear(__gen_e_acsl__22);
}
@@ -275,7 +275,7 @@ int main(void)
{
mpz_t __gen_e_acsl__23;
int __gen_e_acsl_lt_3;
- __gmpz_init_set_ui(__gen_e_acsl__23,(unsigned long)5);
+ __gmpz_init_set_si(__gen_e_acsl__23,5L);
__gen_e_acsl_lt_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_y),
(__mpz_struct const *)(__gen_e_acsl__23));
if (__gen_e_acsl_lt_3 < 0) ; else break;
@@ -283,7 +283,7 @@ int main(void)
}
{
mpz_t __gen_e_acsl__20;
- __gmpz_init_set_ui(__gen_e_acsl__20,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl__20,0L);
__gmpz_set(__gen_e_acsl_z,(__mpz_struct const *)(__gen_e_acsl__20));
__gmpz_clear(__gen_e_acsl__20);
}
@@ -303,7 +303,7 @@ int main(void)
__gmpz_add(__gen_e_acsl_add_7,
(__mpz_struct const *)(__gen_e_acsl_x_5),
(__mpz_struct const *)(__gen_e_acsl_z));
- __gmpz_init_set_ui(__gen_e_acsl__19,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl__19,1L);
__gmpz_init(__gen_e_acsl_add_8);
__gmpz_add(__gen_e_acsl_add_8,
(__mpz_struct const *)(__gen_e_acsl_y),
@@ -322,7 +322,7 @@ int main(void)
{
mpz_t __gen_e_acsl__21;
mpz_t __gen_e_acsl_add_9;
- __gmpz_init_set_ui(__gen_e_acsl__21,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__21,1L);
__gmpz_init(__gen_e_acsl_add_9);
__gmpz_add(__gen_e_acsl_add_9,
(__mpz_struct const *)(__gen_e_acsl_z),
@@ -336,7 +336,7 @@ int main(void)
{
mpz_t __gen_e_acsl__24;
mpz_t __gen_e_acsl_add_10;
- __gmpz_init_set_ui(__gen_e_acsl__24,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__24,1L);
__gmpz_init(__gen_e_acsl_add_10);
__gmpz_add(__gen_e_acsl_add_10,
(__mpz_struct const *)(__gen_e_acsl_y),
@@ -350,7 +350,7 @@ int main(void)
{
mpz_t __gen_e_acsl__27;
mpz_t __gen_e_acsl_add_11;
- __gmpz_init_set_ui(__gen_e_acsl__27,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__27,1L);
__gmpz_init(__gen_e_acsl_add_11);
__gmpz_add(__gen_e_acsl_add_11,
(__mpz_struct const *)(__gen_e_acsl_x_5),
@@ -375,12 +375,12 @@ int main(void)
mpz_t __gen_e_acsl_x_6;
__gen_e_acsl_exists = 0;
__gmpz_init(__gen_e_acsl_x_6);
- __gmpz_set_si(__gen_e_acsl_x_6,(long)0);
+ __gmpz_set_si(__gen_e_acsl_x_6,0L);
while (1) {
{
mpz_t __gen_e_acsl__29;
int __gen_e_acsl_lt_5;
- __gmpz_init_set_ui(__gen_e_acsl__29,(unsigned long)10);
+ __gmpz_init_set_si(__gen_e_acsl__29,10L);
__gen_e_acsl_lt_5 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_6),
(__mpz_struct const *)(__gen_e_acsl__29));
if (__gen_e_acsl_lt_5 < 0) ; else break;
@@ -389,7 +389,7 @@ int main(void)
{
mpz_t __gen_e_acsl__28;
int __gen_e_acsl_eq_5;
- __gmpz_init_set_ui(__gen_e_acsl__28,(unsigned long)5);
+ __gmpz_init_set_si(__gen_e_acsl__28,5L);
__gen_e_acsl_eq_5 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_6),
(__mpz_struct const *)(__gen_e_acsl__28));
__gmpz_clear(__gen_e_acsl__28);
@@ -402,7 +402,7 @@ int main(void)
{
mpz_t __gen_e_acsl__30;
mpz_t __gen_e_acsl_add_12;
- __gmpz_init_set_ui(__gen_e_acsl__30,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__30,1L);
__gmpz_init(__gen_e_acsl_add_12);
__gmpz_add(__gen_e_acsl_add_12,
(__mpz_struct const *)(__gen_e_acsl_x_6),
@@ -428,12 +428,12 @@ int main(void)
mpz_t __gen_e_acsl_x_7;
__gen_e_acsl_forall_6 = 1;
__gmpz_init(__gen_e_acsl_x_7);
- __gmpz_set_si(__gen_e_acsl_x_7,(long)0);
+ __gmpz_set_si(__gen_e_acsl_x_7,0L);
while (1) {
{
mpz_t __gen_e_acsl__38;
int __gen_e_acsl_lt_6;
- __gmpz_init_set_ui(__gen_e_acsl__38,(unsigned long)10);
+ __gmpz_init_set_si(__gen_e_acsl__38,10L);
__gen_e_acsl_lt_6 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_7),
(__mpz_struct const *)(__gen_e_acsl__38));
if (__gen_e_acsl_lt_6 < 0) ; else break;
@@ -446,8 +446,8 @@ int main(void)
mpz_t __gen_e_acsl_mod;
int __gen_e_acsl_eq_6;
int __gen_e_acsl_implies;
- __gmpz_init_set_ui(__gen_e_acsl__31,(unsigned long)2);
- __gmpz_init_set_ui(__gen_e_acsl__32,0UL);
+ __gmpz_init_set_si(__gen_e_acsl__31,2L);
+ __gmpz_init_set_si(__gen_e_acsl__32,0L);
__gen_e_acsl_mod_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__31),
(__mpz_struct const *)(__gen_e_acsl__32));
__gmpz_init(__gen_e_acsl_mod);
@@ -467,7 +467,7 @@ int main(void)
__gmpz_init(__gen_e_acsl_y_2);
{
mpz_t __gen_e_acsl__34;
- __gmpz_init_set_ui(__gen_e_acsl__34,(unsigned long)0);
+ __gmpz_init_set_si(__gen_e_acsl__34,0L);
__gmpz_set(__gen_e_acsl_y_2,
(__mpz_struct const *)(__gen_e_acsl__34));
__gmpz_clear(__gen_e_acsl__34);
@@ -479,8 +479,8 @@ int main(void)
int __gen_e_acsl_div_guard;
mpz_t __gen_e_acsl_div;
int __gen_e_acsl_le_5;
- __gmpz_init_set_ui(__gen_e_acsl__35,(unsigned long)2);
- __gmpz_init_set_ui(__gen_e_acsl__36,0UL);
+ __gmpz_init_set_si(__gen_e_acsl__35,2L);
+ __gmpz_init_set_si(__gen_e_acsl__36,0L);
__gen_e_acsl_div_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__35),
(__mpz_struct const *)(__gen_e_acsl__36));
__gmpz_init(__gen_e_acsl_div);
@@ -502,7 +502,7 @@ int main(void)
mpz_t __gen_e_acsl__33;
mpz_t __gen_e_acsl_mul;
int __gen_e_acsl_eq_7;
- __gmpz_init_set_ui(__gen_e_acsl__33,(unsigned long)2);
+ __gmpz_init_set_si(__gen_e_acsl__33,2L);
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,
(__mpz_struct const *)(__gen_e_acsl__33),
@@ -520,7 +520,7 @@ int main(void)
{
mpz_t __gen_e_acsl__37;
mpz_t __gen_e_acsl_add_13;
- __gmpz_init_set_ui(__gen_e_acsl__37,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__37,1L);
__gmpz_init(__gen_e_acsl_add_13);
__gmpz_add(__gen_e_acsl_add_13,
(__mpz_struct const *)(__gen_e_acsl_y_2),
@@ -547,7 +547,7 @@ int main(void)
{
mpz_t __gen_e_acsl__39;
mpz_t __gen_e_acsl_add_14;
- __gmpz_init_set_ui(__gen_e_acsl__39,1UL);
+ __gmpz_init_set_si(__gen_e_acsl__39,1L);
__gmpz_init(__gen_e_acsl_add_14);
__gmpz_add(__gen_e_acsl_add_14,
(__mpz_struct const *)(__gen_e_acsl_x_7),
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
index a27112ee0f4d249874672b6ae0d5b6e0e536b8ea..b2401c11ed4c1f72ca32abab05d71325473daf33 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
@@ -10,10 +10,11 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_size ∈ [--..--]
-[value] using specification for function __gmpz_init_set_ui
+[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
+[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_init_set_str
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
index b22bde80bf3c8e20400b6b2656ceed600662575d..2aa07b37357093db836cc8fd0bba2338c8cbac00 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
@@ -18,7 +18,7 @@ tests/gmp/longlong.i:9:[value] warning: recursive call during value analysis
[value] using specification for function my_pow
tests/gmp/longlong.i:10:[value] warning: signed overflow. assert -2147483648 ≤ tmp*tmp;
tests/gmp/longlong.i:10:[value] warning: signed overflow. assert tmp*tmp ≤ 2147483647;
-[value] using specification for function __gmpz_init_set_ui
+[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_import
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
index e216ce90576f00ec23d15ca81f38f40101b6e0ea..cb8aca989bc7fc910a4eb1769f247bbca1069822 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
@@ -18,7 +18,7 @@ tests/gmp/longlong.i:9:[value] warning: recursive call during value analysis
[value] using specification for function my_pow
tests/gmp/longlong.i:10:[value] warning: signed overflow. assert -2147483648 ≤ tmp*tmp;
tests/gmp/longlong.i:10:[value] warning: signed overflow. assert tmp*tmp ≤ 2147483647;
-[value] using specification for function __gmpz_init_set_ui
+[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_import
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
index 97d849b107675c1fa1da89d80b69febe9adfe0d8..35b4ab588d77d2f527e354c22661c15c61298dab 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
@@ -11,7 +11,6 @@
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_size ∈ [--..--]
[value] using specification for function __gmpz_init_set_si
-[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
index 9a921a8df6ad5f842062546598f66c2bb4b0a0ba..b465a2836de9efe25784c6740f9c7f822cdfd85a 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
@@ -12,7 +12,7 @@
__e_acsl_heap_size ∈ [--..--]
tests/gmp/quantif.i:9:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init
-[value] using specification for function __gmpz_init_set_ui
+[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_set
[value] using specification for function __gmpz_clear
tests/gmp/quantif.i:9:[value] entering loop for the first time
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index cafde44823ec0639d2f05f1c637e09a0d9a98c29..e4247eea1849c3589e849b01133fdcd083a2a8cd 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -138,7 +138,7 @@ let add_cast ~loc ?name env ctx is_mpz_string t_opt e =
Cil.mkCastT ~force:false ~e ~oldt:ty ~newt:ctx, env
let constant_to_exp ~loc t = function
- | Integer(n, repr) ->
+ | Integer(n, _repr) ->
(try
let ity = Typing.get_integer_ty t in
match ity with
@@ -149,9 +149,15 @@ let constant_to_exp ~loc t = function
match cast, kind with
| Some ty, (ILongLong | IULongLong) when Gmpz.is_t ty ->
raise Cil.Not_representable
- | (None | Some _), _ -> Cil.kinteger64 ~loc ~kind ?repr n, false
+ | (None | Some _), _ ->
+ (* do not keep the initial string representation because the
+ generated constant must reflect its type computed by the type
+ system. For instance, when translating [INT_MAX+1], we must
+ generate a [long long] addition and so [1LL]. If we keep the
+ initial string representation, the kind would be ignored in the
+ generated code and so [1] would be generated. *)
+ Cil.kinteger64 ~loc ~kind n, false
with Cil.Not_representable ->
-
(* too big integer *)
Cil.mkString ~loc (Integer.to_string n), true)
| LStr s -> Cil.new_exp ~loc (Const (CStr s)), false
@@ -510,7 +516,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.new_exp ~loc (BinOp(bop, e1, e2, Cil.intType)), env
(* \base_addr, \block_length and \freeable annotations *)
and mmodel_call ~loc kf name ctx env t =
@@ -797,16 +803,16 @@ exception No_simple_translation of term
(* This function is used by plug-in [Cfp]. *)
let term_to_exp typ t =
- let ctx = match typ with
- | None -> Typing.c_int (* useless, but required *)
- | Some typ ->
- if Gmpz.is_t typ then Typing.gmp
- else
- match typ with
- | TInt(ik, _) -> Typing.ikind ik
- | _ -> Typing.c_int (* useless, but required *)
+ (* infer a context from the given [typ] whenever possible *)
+ let ctx_of_typ ty =
+ if Gmpz.is_t ty then Typing.gmp
+ else
+ match ty with
+ | TInt(ik, _) -> Typing.ikind ik
+ | _ -> Typing.other
in
- Typing.type_term ~force:false ~ctx t;
+ let ctx = Extlib.opt_map ctx_of_typ typ in
+ Typing.type_term ~force:false ?ctx t;
let env = Env.empty (new Visitor.frama_c_copy Project_skeleton.dummy) in
let env = Env.push env in
let env = Env.rte env false in
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 388522772149d94924198d1e9ee5061f3475a6d6..f349a4f66f4c50444db2141bc189dd02bf02db8d 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -44,6 +44,7 @@ type integer_ty =
let gmp = Gmp
let c_int = C_type IInt
let ikind ik = C_type ik
+let other = Other
(* the integer_ty corresponding to size_t *)
let size_t () = match Cil.theMachine.Cil.typeOfSizeOf with
@@ -163,18 +164,22 @@ end
(* Compute the smallest type (bigger than [int]) which can contain the whole
interval. It is the \theta operator of the JFLA's paper. *)
-let ty_of_interv ~ctx i =
+let ty_of_interv ?ctx i =
let open Interval in
let is_pos = Integer.ge i.lower Integer.zero in
try
let lkind = Cil.intKindForValue i.lower is_pos in
let ukind = Cil.intKindForValue i.upper is_pos in
- let kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
+ (* kind corresponding to the interval *)
+ let itv_kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
+ (* convert the kind to [IInt] whenever smaller. *)
+ let kind = if Cil.intTypeIncluded itv_kind IInt then IInt else itv_kind in
(* ctx type whenever possible to prevent superfluous casts in the generated
code *)
(match ctx with
- | Gmp | Other -> C_type kind
- | C_type ik -> if Cil.intTypeIncluded kind ik then ctx else C_type kind)
+ | None | Some (Gmp | Other) -> C_type kind
+ | Some (C_type ik as ctx) ->
+ if Cil.intTypeIncluded itv_kind ik then ctx else C_type kind)
with Cil.Not_representable ->
Gmp
@@ -204,8 +209,8 @@ let mk_ctx ~force c =
(* type the term [t] in a context [ctx]. Take --e-acsl-gmp-only into account iff
not [force]. *)
-let rec type_term ~force ~ctx t =
- let ctx = mk_ctx ~force ctx in
+let rec type_term ~force ?ctx t =
+ let ctx = Extlib.opt_map (mk_ctx ~force) ctx in
let dup ty = ty, ty in
let infer t =
Cil.CurrentLoc.set t.term_loc;
@@ -220,7 +225,7 @@ let rec type_term ~force ~ctx t =
let ty =
try
let i = Interval.infer t in
- ty_of_interv ~ctx i
+ ty_of_interv ?ctx i
with Interval.Not_an_integer ->
Other
in
@@ -229,7 +234,7 @@ let rec type_term ~force ~ctx t =
let ty =
try
let i = Interval.infer t in
- ty_of_interv ~ctx i
+ ty_of_interv ?ctx i
with Interval.Not_an_integer ->
Other
in
@@ -245,7 +250,7 @@ let rec type_term ~force ~ctx t =
let i = Interval.infer t in
(* [t'] must be typed, but it is a pointer *)
ignore (type_term ~force:false ~ctx:Other t');
- ty_of_interv ~ctx i
+ ty_of_interv ?ctx i
with Interval.Not_an_integer ->
assert false (* this term is an integer *)
in
@@ -258,7 +263,7 @@ let rec type_term ~force ~ctx t =
(* [t1] and [t2] must be typed, but they are pointers *)
ignore (type_term ~force:false ~ctx:Other t1);
ignore (type_term ~force:false ~ctx:Other t2);
- ty_of_interv ~ctx i
+ ty_of_interv ?ctx i
with Interval.Not_an_integer ->
assert false (* this term is an integer *)
in
@@ -269,7 +274,7 @@ let rec type_term ~force ~ctx t =
try
let i = Interval.infer t in
let i' = Interval.infer t' in
- mk_ctx ~force:false (ty_of_interv ~ctx (Interval.join i i'))
+ mk_ctx ~force:false (ty_of_interv ?ctx (Interval.join i i'))
with Interval.Not_an_integer ->
Other (* real *)
in
@@ -284,7 +289,7 @@ let rec type_term ~force ~ctx t =
let i = Interval.infer t in
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
- let ctx = ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2)) in
+ let ctx = ty_of_interv ?ctx (Interval.join i (Interval.join i1 i2)) in
mk_ctx ~force:false ctx
with Interval.Not_an_integer ->
Other (* real *)
@@ -294,12 +299,12 @@ let rec type_term ~force ~ctx t =
dup ctx
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
- assert (compare ctx c_int >= 0);
+ assert (match ctx with None -> true | Some c -> compare c c_int >= 0);
let ctx =
try
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
- mk_ctx ~force:false (ty_of_interv ~ctx (Interval.join i1 i2))
+ mk_ctx ~force:false (ty_of_interv ?ctx (Interval.join i1 i2))
with Interval.Not_an_integer ->
Other
in
@@ -316,7 +321,7 @@ let rec type_term ~force ~ctx t =
try
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
- ty_of_interv ~ctx (Interval.join i1 i2)
+ ty_of_interv ?ctx (Interval.join i1 i2)
with Interval.Not_an_integer ->
Other
in
@@ -336,7 +341,7 @@ let rec type_term ~force ~ctx t =
let i = Interval.infer t' in
(* nothing more to do: [i] is already more precise than what we
could infer from the arguments of the cast. *)
- ty_of_interv ~ctx i
+ ty_of_interv ?ctx i
with Interval.Not_an_integer ->
Other
in
@@ -351,7 +356,7 @@ let rec type_term ~force ~ctx t =
try
let i2 = Interval.infer t2 in
let i3 = Interval.infer t3 in
- let ctx = ty_of_interv ~ctx (Interval.join i (Interval.join i2 i3)) in
+ let ctx = ty_of_interv ?ctx (Interval.join i (Interval.join i2 i3)) in
mk_ctx ~force:false ctx
with Interval.Not_an_integer ->
Other
@@ -361,7 +366,7 @@ let rec type_term ~force ~ctx t =
dup ctx
| Tat (t, _)
- | TLogic_coerce (_, t) -> dup (type_term ~force ~ctx t).ty
+ | TLogic_coerce (_, t) -> dup (type_term ~force ?ctx t).ty
| TCoerceE (t1, t2) ->
let ctx =
@@ -369,7 +374,7 @@ let rec type_term ~force ~ctx t =
let i = Interval.infer t in
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
- ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2))
+ ty_of_interv ?ctx (Interval.join i (Interval.join i1 i2))
with Interval.Not_an_integer ->
Other
in
@@ -411,7 +416,13 @@ let rec type_term ~force ~ctx t =
| Ttype _
| Tempty_set -> dup Other
in
- Memo.memo (fun t -> let ty, op = infer t in coerce ~ctx ~op ty) t
+ Memo.memo
+ (fun t ->
+ let ty, op = infer t in
+ match ctx with
+ | None -> { ty; op; cast = None }
+ | Some ctx -> coerce ~ctx ~op ty)
+ t
and type_term_lval (host, offset) =
type_term_lhost host;
@@ -532,10 +543,10 @@ let rec type_predicate_named p =
in
coerce ~ctx:c_int ~op c_int
-let type_term ~force ~ctx t =
+let type_term ~force ?ctx t =
Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
- Printer.pp_term t pretty ctx;
- ignore (type_term ~force ~ctx t)
+ Printer.pp_term t (Pretty_utils.pp_opt pretty) ctx;
+ ignore (type_term ~force ?ctx t)
let type_named_predicate ?(must_clear=true) p =
Options.feedback ~dkey ~level:3 "typing predicate '%a'."
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 236258f10326a5049de969405d50b26df42aba14..de5d764a9f708a94b57342f4d5951abbe29fa214 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -61,6 +61,7 @@ type integer_ty = private
val gmp: integer_ty
val c_int: integer_ty
val ikind: ikind -> integer_ty
+val other: integer_ty
(** {3 Useful operations over {!integer_ty}} *)
@@ -80,7 +81,7 @@ val join: integer_ty -> integer_ty -> integer_ty
(** {2 Typing} *)
(******************************************************************************)
-val type_term: force:bool -> ctx:integer_ty -> term -> unit
+val type_term: force:bool -> ?ctx:integer_ty -> term -> unit
(** Compute the type of each subterm of the given term in the given context. If
[force] is true, then the conversion to the given context is done even if
-e-acsl-gmp-only is set. *)