From 0cb6d45c309dbef2c71220776249b4bd984470df Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 7 Oct 2021 14:13:19 +0200
Subject: [PATCH] [e-acsl:tests] update oracle wrt rebase's changes
---
.../oracle/extended_quantifiers.res.oracle | 28 +++++++++----------
.../arith/oracle/gen_extended_quantifiers.c | 8 +++---
2 files changed, 18 insertions(+), 18 deletions(-)
diff --git a/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle
index 482ab448a92..3fcbe6979c0 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle
@@ -60,38 +60,38 @@
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:21: Warning:
assertion got status unknown.
-[eva:alarm] tests/arith/extended_quantifiers.c:24: Warning:
- signed overflow.
- assert __gen_e_acsl_k_10 + __gen_e_acsl_one_10 ≤ 2147483647;
-[eva:alarm] tests/arith/extended_quantifiers.c:24: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/extended_quantifiers.c:24: Warning:
- assertion got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:25: Warning:
signed overflow.
- assert __gen_e_acsl_k_12 + __gen_e_acsl_one_11 ≤ 2147483647;
+ assert __gen_e_acsl_k_10 + __gen_e_acsl_one_10 ≤ 2147483647;
[eva:alarm] tests/arith/extended_quantifiers.c:25: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:25: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:26: Warning:
signed overflow.
- assert __gen_e_acsl_k_13 + __gen_e_acsl_one_12 ≤ 2147483647;
+ assert __gen_e_acsl_k_12 + __gen_e_acsl_one_11 ≤ 2147483647;
[eva:alarm] tests/arith/extended_quantifiers.c:26: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:26: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning:
- signed overflow. assert 2 * __gen_e_acsl_k_15 ≤ 2147483647;
+ signed overflow.
+ assert __gen_e_acsl_k_13 + __gen_e_acsl_one_12 ≤ 2147483647;
[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning:
+ signed overflow. assert 2 * __gen_e_acsl_k_15 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning:
signed overflow.
assert __gen_e_acsl_k_15 + __gen_e_acsl_one_13 ≤ 2147483647;
-[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning:
+[eva:alarm] tests/arith/extended_quantifiers.c:29: Warning:
signed overflow. assert 2 * __gen_e_acsl_k_16 ≤ 2147483647;
-[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning:
+[eva:alarm] tests/arith/extended_quantifiers.c:29: Warning:
signed overflow.
assert __gen_e_acsl_k_16 + __gen_e_acsl_one_14 ≤ 2147483647;
-[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning:
+[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning:
+[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning:
assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
index 9ce1b434c48..0dc365800f3 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
@@ -398,7 +398,7 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
__e_acsl_assert(__gen_e_acsl_ge >= 0,1,"Assertion","main",
"\\product(1, 100, \\lambda integer k; k) >= 3628800",
- "tests/arith/extended_quantifiers.c",24);
+ "tests/arith/extended_quantifiers.c",25);
__gmpz_clear(__gen_e_acsl_lambda_10);
__gmpz_clear(__gen_e_acsl_accumulator_10);
__gmpz_clear(__gen_e_acsl__7);
@@ -431,7 +431,7 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_accumulator_11 == 3628800UL,1,"Assertion",
"main",
"\\product(1, 10, \\lambda integer k; k) == 3628800",
- "tests/arith/extended_quantifiers.c",25);
+ "tests/arith/extended_quantifiers.c",26);
}
/*@ assert \product(1, 10, \lambda ℤ k; k) ≡ 3628800; */ ;
{
@@ -473,7 +473,7 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,1,"Assertion","main",
"\\product(-10, 10, \\lambda integer k; k) == 0",
- "tests/arith/extended_quantifiers.c",26);
+ "tests/arith/extended_quantifiers.c",27);
__gmpz_clear(__gen_e_acsl_lambda_12);
__gmpz_clear(__gen_e_acsl_accumulator_12);
__gmpz_clear(__gen_e_acsl__8);
@@ -553,7 +553,7 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_14));
__e_acsl_assert(__gen_e_acsl_eq_3 == 0,1,"Assertion","main",
"\\product(-20, -1, \\lambda integer k; 2 * k) ==\n\\product(1, 20, \\lambda integer k; 2 * k)",
- "tests/arith/extended_quantifiers.c",27);
+ "tests/arith/extended_quantifiers.c",28);
__gmpz_clear(__gen_e_acsl_lambda_13);
__gmpz_clear(__gen_e_acsl_accumulator_13);
__gmpz_clear(__gen_e_acsl_lambda_14);
--
GitLab