From f9cff19de1d2c1b729531b40ff228626ca302e6c Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 29 Sep 2011 08:02:30 +0000
Subject: [PATCH] updating oracles according to kernel changes
---
.../e-acsl-runtime/oracle/arith.res.oracle | 34 --------------
.../e-acsl-runtime/oracle/array.res.oracle | 8 ----
.../e-acsl-runtime/oracle/cast.res.oracle | 16 -------
.../oracle/comparison.res.oracle | 18 --------
.../e-acsl-runtime/oracle/gen_stmt_contract.c | 16 +++----
.../oracle/integer_constant.res.oracle | 14 ------
.../e-acsl-runtime/oracle/lazy.res.oracle | 14 ------
.../oracle/nested_code_annot.res.oracle | 14 ------
.../oracle/other_constants.res.oracle | 14 ------
.../e-acsl-runtime/oracle/ptr.res.oracle | 26 -----------
.../e-acsl-runtime/oracle/sizeof.res.oracle | 14 ------
.../oracle/stmt_contract.res.oracle | 44 +++++++++----------
12 files changed, 30 insertions(+), 202 deletions(-)
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 8c3d2b5d938..ccbd44262d0 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 305eb99a8ac..12014f01f2a 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 bc71784ef73..e972922f1d3 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 6351bee0d37..e1913f4de86 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 20093f2ad7f..1386c2973e1 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 f6e48bcfecd..47ba90c5082 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 1d54dc22a35..87c7511db3b 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 6f6d95e3edb..e5886051f79 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 e2d48d0b40d..e7827eda3aa 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 7a43b69b087..cfb7ac64d98 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 723f3b5095d..1d2785ee447 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 b483a01554a..de4c8e14948 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));
}
--
GitLab