diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index a96446312663b242c17e51b1773bfd63fbc941ee..f4f2bd0278dd8361520e795edd52c3eba2dddac8 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -1,19 +1,7 @@
-- enlever les skip inutiles
-- valid global literal string
-
-################
-# MEMORY MODEL #
-################
-
-- appel de full_init et consort sur des variables générées par e_acsl (at.i)
-- ne générer les instructions que si nécessaire
-- traduction constructions logiques modèle mémoire \valid, \init ...
-
################
# NEXT RELEASE #
################
-- updater doc/Changelog
- [Bernard] avoir une fonction e_acsl_trace_behavior(char *bhv_name) {}
à appeler dès qu'un behavior est activé
- utiliser Rte pour tous les overflows potentiels
@@ -54,8 +42,6 @@
# TESTS #
#########
-- améliorer test "integer_constant.i" quand bug fixed #745
- inclure exemple du E-ACSL Reference Manual
- test arith.i: mettre les exemples du ACSL manual about div and modulo
-- -val-verbose 0 dans les tests...
-- test intensif modèle mémoire
+- tests intensifs modèle mémoire
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i b/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
index ef833849ff249ba11518a63bbe84ac674b943e0d..6086959108b1a8e8029d56591f7aaa3c1ae226b6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
@@ -1,6 +1,5 @@
/* run.config
COMMENT: integer constant + a stmt after the assertion
- COMMENT: waiting for fixing BTS #745
EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && ./gcc_test.sh integer_constant
EXECNOW: LOG gen_integer_constant2.c BIN gen_integer_constant2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant2.c > /dev/null && ./gcc_test.sh integer_constant2
*/
@@ -11,7 +10,7 @@ int main(void) {
/*@ assert 0 != 1; */
/*@ assert 1152921504606846975 == 0xfffffffffffffff; */
- /* /\*@ assert 0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff; *\/ */
+ /*@ assert 0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff; */
return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index 4369887457da29a2ced9dd231e64761dc841eaea..c5557fdfe079742d02d74e871eb6879cd22d46dc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -22,6 +22,27 @@ typedef struct __fc_FILE FILE;
/*@
model __mpz_struct { ℤ n };
*/
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+
+ ensures \initialized(\old(z));
+ allocates \old(z);
+
+ assigns *z;
+ assigns *z \from str, base;
+
+*/
+extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
+ char const *str,
+ int base);
+/*@ requires \valid(x);
+ assigns *x; */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)2147483647;
extern int __fc_heap_status;
@@ -58,14 +79,30 @@ int main(void)
int __retres;
int x;
/*@ assert 0 ≡ 0; */
- e_acsl_assert(0 == 0,(char *)"Assertion",(char *)"0 == 0",9);
+ e_acsl_assert(0 == 0,(char *)"Assertion",(char *)"0 == 0",8);
x = 0;
x ++;
/*@ assert 0 ≢ 1; */
- e_acsl_assert(0 != 1,(char *)"Assertion",(char *)"0 != 1",11);
+ e_acsl_assert(0 != 1,(char *)"Assertion",(char *)"0 != 1",10);
/*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */
e_acsl_assert(1152921504606846975 == 0xfffffffffffffff,(char *)"Assertion",
- (char *)"1152921504606846975 == 0xfffffffffffffff",12);
+ (char *)"1152921504606846975 == 0xfffffffffffffff",11);
+ /*@ assert
+ 0xffffffffffffffffffffffffffffffff ≡
+ 0xffffffffffffffffffffffffffffffff;
+ */
+ {
+ mpz_t __e_acsl;
+ int __e_acsl_eq;
+ __gmpz_init_set_str(__e_acsl,"340282366920938463463374607431768211455",
+ 10);
+ __e_acsl_eq = __gmpz_cmp(__e_acsl,__e_acsl);
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",
+ (char *)"0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff",
+ 13);
+ __gmpz_clear(__e_acsl);
+ }
+
__retres = 0;
__clean();
return (__retres);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
index ab2e44e1ef7cf8633f5e53515624d93971dcf4fd..8800993ab127dea8eb8281c08825df8ee47549e2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
@@ -96,7 +96,7 @@ int main(void)
int __e_acsl_eq;
__gmpz_init_set_si(__e_acsl,(long)0);
__e_acsl_eq = __gmpz_cmp(__e_acsl,__e_acsl);
- e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"0 == 0",9);
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"0 == 0",8);
__gmpz_clear(__e_acsl);
}
@@ -110,7 +110,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_2,(long)0);
__gmpz_init_set_si(__e_acsl_3,(long)1);
__e_acsl_ne = __gmpz_cmp(__e_acsl_2,__e_acsl_3);
- e_acsl_assert(__e_acsl_ne != 0,(char *)"Assertion",(char *)"0 != 1",11);
+ e_acsl_assert(__e_acsl_ne != 0,(char *)"Assertion",(char *)"0 != 1",10);
__gmpz_clear(__e_acsl_2);
__gmpz_clear(__e_acsl_3);
}
@@ -122,10 +122,26 @@ int main(void)
__gmpz_init_set_str(__e_acsl_4,"1152921504606846975",10);
__e_acsl_eq_2 = __gmpz_cmp(__e_acsl_4,__e_acsl_4);
e_acsl_assert(__e_acsl_eq_2 == 0,(char *)"Assertion",
- (char *)"1152921504606846975 == 0xfffffffffffffff",12);
+ (char *)"1152921504606846975 == 0xfffffffffffffff",11);
__gmpz_clear(__e_acsl_4);
}
+ /*@ assert
+ 0xffffffffffffffffffffffffffffffff ≡
+ 0xffffffffffffffffffffffffffffffff;
+ */
+ {
+ mpz_t __e_acsl_5;
+ int __e_acsl_eq_3;
+ __gmpz_init_set_str(__e_acsl_5,"340282366920938463463374607431768211455",
+ 10);
+ __e_acsl_eq_3 = __gmpz_cmp(__e_acsl_5,__e_acsl_5);
+ e_acsl_assert(__e_acsl_eq_3 == 0,(char *)"Assertion",
+ (char *)"0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff",
+ 13);
+ __gmpz_clear(__e_acsl_5);
+ }
+
__retres = 0;
__clean();
return (__retres);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
index 5bdea428011736c1dfb2d850fb93c031749d984e..761045be98ff9ba710284ce82571d4d2e1f08cb9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
@@ -25,70 +25,84 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-tests/e-acsl-runtime/integer_constant.i:9:[value] Assertion got status valid.
+tests/e-acsl-runtime/integer_constant.i:8:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:9.
+ Called from tests/e-acsl-runtime/integer_constant.i:8.
[value] using specification for function __gmpz_init_set_si
./share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
./share/e-acsl/e_acsl_gmp.h:63:[value] Function __gmpz_init_set_si: postcondition got status valid.
./share/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: postcondition got status unknown.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:9.
+ Called from tests/e-acsl-runtime/integer_constant.i:8.
[value] using specification for function __gmpz_cmp
./share/e-acsl/e_acsl_gmp.h:115:[value] Function __gmpz_cmp: precondition got status valid.
./share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got status valid.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_assert <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:9.
+ Called from tests/e-acsl-runtime/integer_constant.i:8.
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
[value] computing for function __gmpz_clear <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:9.
+ Called from tests/e-acsl-runtime/integer_constant.i:8.
[value] using specification for function __gmpz_clear
./share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
[value] Done for function __gmpz_clear
-tests/e-acsl-runtime/integer_constant.i:11:[value] Assertion got status valid.
+tests/e-acsl-runtime/integer_constant.i:10:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:11.
+ Called from tests/e-acsl-runtime/integer_constant.i:10.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:11.
+ Called from tests/e-acsl-runtime/integer_constant.i:10.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:11.
+ Called from tests/e-acsl-runtime/integer_constant.i:10.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_assert <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:11.
+ Called from tests/e-acsl-runtime/integer_constant.i:10.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
[value] computing for function __gmpz_clear <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:11.
+ Called from tests/e-acsl-runtime/integer_constant.i:10.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:11.
+ Called from tests/e-acsl-runtime/integer_constant.i:10.
[value] Done for function __gmpz_clear
-tests/e-acsl-runtime/integer_constant.i:12:[value] Assertion got status valid.
+tests/e-acsl-runtime/integer_constant.i:11:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_str <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:12.
+ Called from tests/e-acsl-runtime/integer_constant.i:11.
[value] using specification for function __gmpz_init_set_str
./share/e-acsl/e_acsl_gmp.h:70:[value] Function __gmpz_init_set_str: precondition got status valid.
./share/e-acsl/e_acsl_gmp.h:72:[value] Function __gmpz_init_set_str: postcondition got status valid.
./share/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: postcondition got status unknown.
[value] Done for function __gmpz_init_set_str
[value] computing for function __gmpz_cmp <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:12.
+ Called from tests/e-acsl-runtime/integer_constant.i:11.
+[value] Done for function __gmpz_cmp
+[value] computing for function e_acsl_assert <- main.
+ Called from tests/e-acsl-runtime/integer_constant.i:11.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_clear <- main.
+ Called from tests/e-acsl-runtime/integer_constant.i:11.
+[value] Done for function __gmpz_clear
+tests/e-acsl-runtime/integer_constant.i:13:[value] Assertion got status valid.
+[value] computing for function __gmpz_init_set_str <- main.
+ Called from tests/e-acsl-runtime/integer_constant.i:13.
+[value] Done for function __gmpz_init_set_str
+[value] computing for function __gmpz_cmp <- main.
+ Called from tests/e-acsl-runtime/integer_constant.i:13.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_assert <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:12.
+ Called from tests/e-acsl-runtime/integer_constant.i:13.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
[value] computing for function __gmpz_clear <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:12.
+ Called from tests/e-acsl-runtime/integer_constant.i:13.
[value] Done for function __gmpz_clear
[value] computing for function __clean <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:16.
+ Called from tests/e-acsl-runtime/integer_constant.i:15.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] Done for function __clean
@@ -198,7 +212,7 @@ int main(void)
int __e_acsl_eq;
__gmpz_init_set_si(__e_acsl,(long)0);
__e_acsl_eq = __gmpz_cmp(__e_acsl,__e_acsl);
- e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"0 == 0",9);
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"0 == 0",8);
__gmpz_clear(__e_acsl);
}
@@ -212,7 +226,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_2,(long)0);
__gmpz_init_set_si(__e_acsl_3,(long)1);
__e_acsl_ne = __gmpz_cmp(__e_acsl_2,__e_acsl_3);
- e_acsl_assert(__e_acsl_ne != 0,(char *)"Assertion",(char *)"0 != 1",11);
+ e_acsl_assert(__e_acsl_ne != 0,(char *)"Assertion",(char *)"0 != 1",10);
__gmpz_clear(__e_acsl_2);
__gmpz_clear(__e_acsl_3);
}
@@ -224,10 +238,26 @@ int main(void)
__gmpz_init_set_str(__e_acsl_4,"1152921504606846975",10);
__e_acsl_eq_2 = __gmpz_cmp(__e_acsl_4,__e_acsl_4);
e_acsl_assert(__e_acsl_eq_2 == 0,(char *)"Assertion",
- (char *)"1152921504606846975 == 0xfffffffffffffff",12);
+ (char *)"1152921504606846975 == 0xfffffffffffffff",11);
__gmpz_clear(__e_acsl_4);
}
+ /*@ assert
+ 0xffffffffffffffffffffffffffffffff ≡
+ 0xffffffffffffffffffffffffffffffff;
+ */
+ {
+ mpz_t __e_acsl_5;
+ int __e_acsl_eq_3;
+ __gmpz_init_set_str(__e_acsl_5,"340282366920938463463374607431768211455",
+ 10);
+ __e_acsl_eq_3 = __gmpz_cmp(__e_acsl_5,__e_acsl_5);
+ e_acsl_assert(__e_acsl_eq_3 == 0,(char *)"Assertion",
+ (char *)"0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff",
+ 13);
+ __gmpz_clear(__e_acsl_5);
+ }
+
__retres = 0;
__clean();
return (__retres);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index ad37eb5e53245920c55c5678d483501086c28186..c6bb1b16cd28ae7b781ff29e071f0fff75f4c036 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -25,24 +25,48 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-tests/e-acsl-runtime/integer_constant.i:9:[value] Assertion got status valid.
+tests/e-acsl-runtime/integer_constant.i:8:[value] Assertion got status valid.
[value] computing for function e_acsl_assert <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:9.
+ Called from tests/e-acsl-runtime/integer_constant.i:8.
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
+tests/e-acsl-runtime/integer_constant.i:10:[value] Assertion got status valid.
+[value] computing for function e_acsl_assert <- main.
+ Called from tests/e-acsl-runtime/integer_constant.i:10.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
tests/e-acsl-runtime/integer_constant.i:11:[value] Assertion got status valid.
[value] computing for function e_acsl_assert <- main.
Called from tests/e-acsl-runtime/integer_constant.i:11.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
-tests/e-acsl-runtime/integer_constant.i:12:[value] Assertion got status valid.
+tests/e-acsl-runtime/integer_constant.i:13:[value] Assertion got status valid.
+[value] computing for function __gmpz_init_set_str <- main.
+ Called from tests/e-acsl-runtime/integer_constant.i:13.
+[value] using specification for function __gmpz_init_set_str
+./share/e-acsl/e_acsl_gmp.h:70:[value] Function __gmpz_init_set_str: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:72:[value] Function __gmpz_init_set_str: postcondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: postcondition got status unknown.
+[value] Done for function __gmpz_init_set_str
+[value] computing for function __gmpz_cmp <- main.
+ Called from tests/e-acsl-runtime/integer_constant.i:13.
+[value] using specification for function __gmpz_cmp
+./share/e-acsl/e_acsl_gmp.h:115:[value] Function __gmpz_cmp: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got status valid.
+[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_assert <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:12.
+ Called from tests/e-acsl-runtime/integer_constant.i:13.
+./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_clear <- main.
+ Called from tests/e-acsl-runtime/integer_constant.i:13.
+[value] using specification for function __gmpz_clear
+./share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
+[value] Done for function __gmpz_clear
[value] computing for function __clean <- main.
- Called from tests/e-acsl-runtime/integer_constant.i:16.
+ Called from tests/e-acsl-runtime/integer_constant.i:15.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] Done for function __clean
@@ -77,6 +101,27 @@ typedef struct __fc_FILE FILE;
/*@
model __mpz_struct { ℤ n };
*/
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+
+ ensures \initialized(\old(z));
+ allocates \old(z);
+
+ assigns *z;
+ assigns *z \from str, base;
+
+*/
+extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
+ char const *str,
+ int base);
+/*@ requires \valid(x);
+ assigns *x; */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)2147483647;
extern int __fc_heap_status;
@@ -114,14 +159,30 @@ int main(void)
int __retres;
int x;
/*@ assert 0 ≡ 0; */
- e_acsl_assert(0 == 0,(char *)"Assertion",(char *)"0 == 0",9);
+ e_acsl_assert(0 == 0,(char *)"Assertion",(char *)"0 == 0",8);
x = 0;
x ++;
/*@ assert 0 ≢ 1; */
- e_acsl_assert(0 != 1,(char *)"Assertion",(char *)"0 != 1",11);
+ e_acsl_assert(0 != 1,(char *)"Assertion",(char *)"0 != 1",10);
/*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */
e_acsl_assert(1152921504606846975 == 0xfffffffffffffff,(char *)"Assertion",
- (char *)"1152921504606846975 == 0xfffffffffffffff",12);
+ (char *)"1152921504606846975 == 0xfffffffffffffff",11);
+ /*@ assert
+ 0xffffffffffffffffffffffffffffffff ≡
+ 0xffffffffffffffffffffffffffffffff;
+ */
+ {
+ mpz_t __e_acsl;
+ int __e_acsl_eq;
+ __gmpz_init_set_str(__e_acsl,"340282366920938463463374607431768211455",
+ 10);
+ __e_acsl_eq = __gmpz_cmp(__e_acsl,__e_acsl);
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",
+ (char *)"0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff",
+ 13);
+ __gmpz_clear(__e_acsl);
+ }
+
__retres = 0;
__clean();
return (__retres);