diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index 8c3d2b5d938bfe388b6fe2039b9751ddbf7d51f5..ccbd44262d02f5542a2159ab0e36dcb6f5275643 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -671,40 +671,6 @@ PROJECT_FILE.i:291:[value] Assertion got status valid.
PROJECT_FILE.i:294:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
-[from] Computing for function mpz_init_set_si
-[from] Done for function mpz_init_set_si
-[from] Computing for function mpz_init
-[from] Done for function mpz_init
-[from] Computing for function mpz_neg
-[from] Done for function mpz_neg
-[from] Computing for function mpz_cmp
-[from] Done for function mpz_cmp
-[from] Computing for function e_acsl_fail
-[from] Computing for function printf <-e_acsl_fail
-[from] Done for function printf
-PROJECT_FILE.i:125:[from] warning: variadic call detected. Using only 1 argument(s).
-[from] Computing for function exit <-e_acsl_fail
-[from] Done for function exit
-PROJECT_FILE.i:125:[from] Non terminating function (no dependencies)
-[from] Done for function e_acsl_fail
-[from] Computing for function mpz_clear
-[from] Done for function mpz_clear
-[from] Computing for function mpz_com
-[from] Done for function mpz_com
-[from] Computing for function mpz_add
-[from] Done for function mpz_add
-[from] Computing for function mpz_sub
-[from] Done for function mpz_sub
-[from] Computing for function mpz_mul
-[from] Done for function mpz_mul
-[from] Computing for function mpz_get_si
-[from] Done for function mpz_get_si
-[from] Computing for function mpz_cdiv_q
-[from] Done for function mpz_cdiv_q
-[from] Computing for function mpz_init_set_str
-[from] Done for function mpz_init_set_str
-[from] Computing for function mpz_mod_ui
-[from] Done for function mpz_mod_ui
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
index 305eb99a8ac94cc02c0e8cff90b1f82f73ed1e51..12014f01f2a109aeb6a6564c5b09a24c15e3b57b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
@@ -36,14 +36,6 @@ PROJECT_FILE.i:141:[value] Assertion got status unknown.
[value] Done for function e_acsl_fail
[value] Recording results for main
[value] done for function main
-[from] Computing for function e_acsl_fail
-[from] Computing for function printf <-e_acsl_fail
-[from] Done for function printf
-PROJECT_FILE.i:125:[from] warning: variadic call detected. Using only 1 argument(s).
-[from] Computing for function exit <-e_acsl_fail
-[from] Done for function exit
-PROJECT_FILE.i:125:[from] Non terminating function (no dependencies)
-[from] Done for function e_acsl_fail
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
index bc71784ef73faada91cb1de204c3208bf07cbca1..e972922f1d3a226ae438170284eb98207059fbf9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
@@ -51,22 +51,6 @@ PROJECT_FILE.i:96:[value] Function mpz_get_ui: precondition got status valid.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
-[from] Computing for function mpz_init_set_str
-[from] Done for function mpz_init_set_str
-[from] Computing for function mpz_get_si
-[from] Done for function mpz_get_si
-[from] Computing for function e_acsl_fail
-[from] Computing for function printf <-e_acsl_fail
-[from] Done for function printf
-PROJECT_FILE.i:125:[from] warning: variadic call detected. Using only 1 argument(s).
-[from] Computing for function exit <-e_acsl_fail
-[from] Done for function exit
-PROJECT_FILE.i:125:[from] Non terminating function (no dependencies)
-[from] Done for function e_acsl_fail
-[from] Computing for function mpz_clear
-[from] Done for function mpz_clear
-[from] Computing for function mpz_get_ui
-[from] Done for function mpz_get_ui
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index 6351bee0d37da771b214486544895fbe4697a9d4..e1913f4de8659e147ef4c024d88d68cc840e1bc4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -293,24 +293,6 @@ PROJECT_FILE.i:229:[value] Assertion got status valid.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
-[from] Computing for function mpz_init_set_si
-[from] Done for function mpz_init_set_si
-[from] Computing for function mpz_cmp
-[from] Done for function mpz_cmp
-[from] Computing for function e_acsl_fail
-[from] Computing for function printf <-e_acsl_fail
-[from] Done for function printf
-PROJECT_FILE.i:125:[from] warning: variadic call detected. Using only 1 argument(s).
-[from] Computing for function exit <-e_acsl_fail
-[from] Done for function exit
-PROJECT_FILE.i:125:[from] Non terminating function (no dependencies)
-[from] Done for function e_acsl_fail
-[from] Computing for function mpz_clear
-[from] Done for function mpz_clear
-[from] Computing for function mpz_init
-[from] Done for function mpz_init
-[from] Computing for function mpz_neg
-[from] Done for function mpz_neg
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
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 20093f2ad7fa09a8365aea2b74595e8a6e776fb6..1386c2973e1e2d285e197f7d82ddb16f59b8adeb 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
@@ -570,7 +570,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
extern void exit(int status);
void e_acsl_fail(char *msg)
{
- printf((char const *)"%s\n",msg);
+ printf("%s\n",msg);
exit(1);
return;
}
@@ -830,23 +830,23 @@ int main(void)
x += y;
/*@ requires x ≡ 5; */
- /*@ requires y ≡ 2; */
{ mpz_t e_acsl_86; mpz_t e_acsl_87; int e_acsl_88;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_86),(long)y);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_87),(long)2);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_86),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_87),(long)5);
e_acsl_88 = __gmpz_cmp((__mpz_struct const *)(e_acsl_86),
(__mpz_struct const *)(e_acsl_87));
- if (! (e_acsl_88 == 0)) { e_acsl_fail((char *)"(y == 2)"); }
+ if (! (e_acsl_88 == 0)) { e_acsl_fail((char *)"(x == 5)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_86));
__gmpz_clear((__mpz_struct *)(e_acsl_87));
}
+ /*@ requires y ≡ 2; */
{ mpz_t e_acsl_89; mpz_t e_acsl_90; int e_acsl_91;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_89),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_90),(long)5);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_89),(long)y);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_90),(long)2);
e_acsl_91 = __gmpz_cmp((__mpz_struct const *)(e_acsl_89),
(__mpz_struct const *)(e_acsl_90));
- if (! (e_acsl_91 == 0)) { e_acsl_fail((char *)"(x == 5)"); }
+ if (! (e_acsl_91 == 0)) { e_acsl_fail((char *)"(y == 2)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_89));
__gmpz_clear((__mpz_struct *)(e_acsl_90));
}
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 f6e48bcfecdbc15fafcbc10a995724afe0256218..47ba90c5082ead24e82b6a5b25d79058ffac1d49 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
@@ -37,20 +37,6 @@ PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
-[from] Computing for function mpz_init_set_str
-[from] Done for function mpz_init_set_str
-[from] Computing for function mpz_cmp
-[from] Done for function mpz_cmp
-[from] Computing for function e_acsl_fail
-[from] Computing for function printf <-e_acsl_fail
-[from] Done for function printf
-PROJECT_FILE.i:125:[from] warning: variadic call detected. Using only 1 argument(s).
-[from] Computing for function exit <-e_acsl_fail
-[from] Done for function exit
-PROJECT_FILE.i:125:[from] Non terminating function (no dependencies)
-[from] Done for function e_acsl_fail
-[from] Computing for function mpz_clear
-[from] Done for function mpz_clear
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
index 1d54dc22a3546873d78163ce7c5a1b886c3ea9d7..87c7511db3b55a074bf3628eb51418a2b1f4acc7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
@@ -193,20 +193,6 @@ PROJECT_FILE.i:251:[value] Assertion got status invalid (stopping propagation).
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
-[from] Computing for function mpz_init_set_si
-[from] Done for function mpz_init_set_si
-[from] Computing for function mpz_cmp
-[from] Done for function mpz_cmp
-[from] Computing for function mpz_clear
-[from] Done for function mpz_clear
-[from] Computing for function e_acsl_fail
-[from] Computing for function printf <-e_acsl_fail
-[from] Done for function printf
-PROJECT_FILE.i:125:[from] warning: variadic call detected. Using only 1 argument(s).
-[from] Computing for function exit <-e_acsl_fail
-[from] Done for function exit
-PROJECT_FILE.i:125:[from] Non terminating function (no dependencies)
-[from] Done for function e_acsl_fail
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
index 6f6d95e3edbf2f076fbf00ccb7500f42f4025be4..e5886051f7960f9d6ad39e0900e80e0f75c7d9e4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
@@ -161,20 +161,6 @@ PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
-[from] Computing for function mpz_init_set_si
-[from] Done for function mpz_init_set_si
-[from] Computing for function mpz_cmp
-[from] Done for function mpz_cmp
-[from] Computing for function e_acsl_fail
-[from] Computing for function printf <-e_acsl_fail
-[from] Done for function printf
-PROJECT_FILE.i:125:[from] warning: variadic call detected. Using only 1 argument(s).
-[from] Computing for function exit <-e_acsl_fail
-[from] Done for function exit
-PROJECT_FILE.i:125:[from] Non terminating function (no dependencies)
-[from] Done for function e_acsl_fail
-[from] Computing for function mpz_clear
-[from] Done for function mpz_clear
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
index e2d48d0b40d8aba6a621513cbd3b67a6473ea780..e7827eda3aafd98687826b9c9a675a363c841703 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
@@ -37,20 +37,6 @@ PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
PROJECT_FILE.i:145:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
-[from] Computing for function mpz_init_set_si
-[from] Done for function mpz_init_set_si
-[from] Computing for function mpz_cmp
-[from] Done for function mpz_cmp
-[from] Computing for function e_acsl_fail
-[from] Computing for function printf <-e_acsl_fail
-[from] Done for function printf
-PROJECT_FILE.i:125:[from] warning: variadic call detected. Using only 1 argument(s).
-[from] Computing for function exit <-e_acsl_fail
-[from] Done for function exit
-PROJECT_FILE.i:125:[from] Non terminating function (no dependencies)
-[from] Done for function e_acsl_fail
-[from] Computing for function mpz_clear
-[from] Done for function mpz_clear
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
index 7a43b69b087ed77c2b5d1fe10dfff1ad76e9c161..cfb7ac64d98ac30248d3599ca365f615409177d6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
@@ -525,32 +525,6 @@ PROJECT_FILE.i:231:[value] Assertion got status valid.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
-[from] Computing for function mpz_init_set_si
-[from] Done for function mpz_init_set_si
-[from] Computing for function mpz_cmp
-[from] Done for function mpz_cmp
-[from] Computing for function e_acsl_fail
-[from] Computing for function printf <-e_acsl_fail
-[from] Done for function printf
-PROJECT_FILE.i:125:[from] warning: variadic call detected. Using only 1 argument(s).
-[from] Computing for function exit <-e_acsl_fail
-[from] Done for function exit
-PROJECT_FILE.i:125:[from] Non terminating function (no dependencies)
-[from] Done for function e_acsl_fail
-[from] Computing for function mpz_clear
-[from] Done for function mpz_clear
-[from] Computing for function mpz_init
-[from] Done for function mpz_init
-[from] Computing for function mpz_mul
-[from] Done for function mpz_mul
-[from] Computing for function mpz_cdiv_q
-[from] Done for function mpz_cdiv_q
-[from] Computing for function mpz_get_si
-[from] Done for function mpz_get_si
-[from] Computing for function mpz_add
-[from] Done for function mpz_add
-[from] Computing for function mpz_sub
-[from] Done for function mpz_sub
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
index 723f3b5095d64432f85d58b609dc1175c2430e2b..1d2785ee44751b82379ee8d9bb917d5df4594e1e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
@@ -61,20 +61,6 @@ PROJECT_FILE.i:139:[value] Assertion got status valid.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
-[from] Computing for function mpz_init_set_si
-[from] Done for function mpz_init_set_si
-[from] Computing for function mpz_cmp
-[from] Done for function mpz_cmp
-[from] Computing for function e_acsl_fail
-[from] Computing for function printf <-e_acsl_fail
-[from] Done for function printf
-PROJECT_FILE.i:125:[from] warning: variadic call detected. Using only 1 argument(s).
-[from] Computing for function exit <-e_acsl_fail
-[from] Done for function exit
-PROJECT_FILE.i:125:[from] Non terminating function (no dependencies)
-[from] Done for function e_acsl_fail
-[from] Computing for function mpz_clear
-[from] Done for function mpz_clear
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
index b483a01554aa877d72cc5e5c308556d7a98eae1e..de4c8e14948fb79cfaae09094a0e142c29fdacda 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
@@ -4,15 +4,15 @@
[value] Values of globals at initialization
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:137.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status valid.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:137.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
Called from PROJECT_FILE.i:138.
-PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
-PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
+PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid.
+PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:139.
@@ -21,13 +21,13 @@ PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:140.
-PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
+PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:140.
@@ -187,13 +187,13 @@ PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
Called from PROJECT_FILE.i:201.
-PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown
+PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status valid.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
Called from PROJECT_FILE.i:202.
-PROJECT_FILE.i:60:[value] Function mpz_add: precondition got status valid
-PROJECT_FILE.i:61:[value] Function mpz_add: precondition got status valid
-PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
+PROJECT_FILE.i:60:[value] Function mpz_add: precondition got status valid.
+PROJECT_FILE.i:61:[value] Function mpz_add: precondition got status valid.
+PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid.
[value] Done for function mpz_add
[value] computing for function mpz_cmp <- main.
Called from PROJECT_FILE.i:203.
@@ -483,16 +483,16 @@ PROJECT_FILE.i:256:[value] assigning non deterministic value for the first time
Called from PROJECT_FILE.i:316.
[value] Done for function mpz_clear
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:323.
+ Called from PROJECT_FILE.i:322.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:323.
+ Called from PROJECT_FILE.i:322.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:324.
+ Called from PROJECT_FILE.i:323.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:325.
+ Called from PROJECT_FILE.i:324.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -502,10 +502,10 @@ PROJECT_FILE.i:256:[value] assigning non deterministic value for the first time
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:326.
+ Called from PROJECT_FILE.i:325.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:326.
+ Called from PROJECT_FILE.i:325.
[value] Done for function mpz_clear
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:330.
@@ -886,23 +886,23 @@ int main(void)
x += y;
/*@ requires x ≡ 5; */
- /*@ requires y ≡ 2; */
{ mpz_t e_acsl_86; mpz_t e_acsl_87; int e_acsl_88;
- mpz_init_set_si((__mpz_struct *)(e_acsl_86),(long)y);
- mpz_init_set_si((__mpz_struct *)(e_acsl_87),(long)2);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_86),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_87),(long)5);
e_acsl_88 = mpz_cmp((__mpz_struct const *)(e_acsl_86),
(__mpz_struct const *)(e_acsl_87));
- if (! (e_acsl_88 == 0)) { e_acsl_fail((char *)"(y == 2)"); }
+ if (! (e_acsl_88 == 0)) { e_acsl_fail((char *)"(x == 5)"); }
mpz_clear((__mpz_struct *)(e_acsl_86));
mpz_clear((__mpz_struct *)(e_acsl_87));
}
+ /*@ requires y ≡ 2; */
{ mpz_t e_acsl_89; mpz_t e_acsl_90; int e_acsl_91;
- mpz_init_set_si((__mpz_struct *)(e_acsl_89),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_90),(long)5);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_89),(long)y);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_90),(long)2);
e_acsl_91 = mpz_cmp((__mpz_struct const *)(e_acsl_89),
(__mpz_struct const *)(e_acsl_90));
- if (! (e_acsl_91 == 0)) { e_acsl_fail((char *)"(x == 5)"); }
+ if (! (e_acsl_91 == 0)) { e_acsl_fail((char *)"(y == 2)"); }
mpz_clear((__mpz_struct *)(e_acsl_89));
mpz_clear((__mpz_struct *)(e_acsl_90));
}