From 5467035764643e01bdfe024e8fa5e10f626d317b Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Thu, 15 Nov 2018 15:11:50 +0100
Subject: [PATCH] Empty quantif
---
src/plugins/e-acsl/doc/Changelog | 7 +-
src/plugins/e-acsl/quantif.ml | 41 ++
.../e-acsl/tests/gmp/oracle/gen_quantif.c | 171 +++--
.../e-acsl/tests/gmp/oracle/gen_quantif2.c | 690 +++++++++---------
.../tests/gmp/oracle/quantif.0.res.oracle | 33 +-
.../tests/gmp/oracle/quantif.1.res.oracle | 31 +-
src/plugins/e-acsl/tests/gmp/quantif.i | 8 +-
7 files changed, 494 insertions(+), 487 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 567f7012139..2329e350cf8 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,13 +19,16 @@
# configure configure
###############################################################################
+- E-ACSL [2018/11/15] Predicates with empty quantifications
+ directly generate \true or \false instead of nested loops.
+
##########################
Plugin E-ACSL 18.0 (Argon)
##########################
-* E-ACSL [2018/11/13] Fix typing bug in quantifications when the
- guards of the quantifier variable cannot be represented into
- its type.
+ guards of the quantifier variable cannot be represented into
+ its type.
-* runtime [2018/11/13] Fix bug #!2405 about memory initialization
in presence of GCC constructors.
-* E-ACSL [2018/10/23] Fix bug #2406 about monitoring of variables
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index 30a72c560b5..dfc19db37bb 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -101,6 +101,36 @@ let compute_quantif_guards quantif bounded_vars hyps =
Error.untypable msg);
List.rev acc
+(* It could happen that the bounds provided for a quantified [lv] are empty
+ in the sense that [min <= lv <= max] but [min > max]. In such cases, \true
+ (or \false depending on the quantification) should be generated instead of
+ nested loops.
+ [has_empty_quantif_with_false_negative] partially detects such cases:
+ Case 1: an empty qunatification was detected for sure, return true.
+ Case 2: we don't know, return false. *)
+let rec has_empty_quantif_with_false_negative = function
+ | [] ->
+ (* case 2 *)
+ false
+ | (t1, rel1, _, rel2, t2) :: guards ->
+ let i1 = Interval.infer t1 in
+ let i2 = Interval.infer t2 in
+ if Ival.is_singleton_int i1 && Ival.is_singleton_int i2 then
+ (* we know the precise values of the bounds *)
+ let lower_bound, _ = Misc.finite_min_and_max i1 in
+ let upper_bound, _ = Misc.finite_min_and_max i2 in
+ let res = match rel1, rel2 with
+ | Rle, Rle -> lower_bound > upper_bound
+ | Rle, Rlt -> lower_bound >= upper_bound
+ | Rlt, Rle -> lower_bound >= upper_bound
+ | Rlt, Rlt -> lower_bound >= Z.sub upper_bound Z.one
+ | _ -> assert false
+ in
+ if res then (* case 1 *) res
+ else has_empty_quantif_with_false_negative guards
+ else
+ has_empty_quantif_with_false_negative guards
+
let () = Typing.compute_quantif_guards_ref := compute_quantif_guards
module Label_ids =
@@ -117,6 +147,16 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
in
(* universal quantification over integers (or a subtype of integer) *)
let guards = compute_quantif_guards p bounded_vars hyps in
+ let has_empty_quantif_with_false_negative =
+ has_empty_quantif_with_false_negative guards
+ in
+ match has_empty_quantif_with_false_negative, is_forall with
+ | true, true ->
+ Cil.one ~loc, env
+ | true, false ->
+ Cil.zero ~loc, env
+ | false, _ ->
+ begin
(* transform [guards] into [lscope_var list],
and update logic scope in the process *)
let lvs_guards, env = List.fold_right
@@ -179,6 +219,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
end_loop_ref := end_loop;
let env = Env.add_stmt env end_loop in
res, env
+ end
let quantif_to_exp kf env p =
let loc = p.pred_loc in
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
index 9b077626b45..3da7cdb090e 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
@@ -49,15 +49,15 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_forall_2,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x; 0 < x <= 1 ==> x == 1",10);
}
- /*@ assert ∀ ℤ x; 0 < x < 1 ⇒ \false; */
+ /*@ assert ∀ ℤ x; 0 ≤ x < 1 ⇒ x ≡ 0; */
{
int __gen_e_acsl_forall_3;
int __gen_e_acsl_x_3;
__gen_e_acsl_forall_3 = 1;
- __gen_e_acsl_x_3 = 0 + 1;
+ __gen_e_acsl_x_3 = 0;
while (1) {
if (__gen_e_acsl_x_3 < 1) ; else break;
- if (0) ;
+ if (__gen_e_acsl_x_3 == 0) ;
else {
__gen_e_acsl_forall_3 = 0;
goto e_acsl_end_loop3;
@@ -66,81 +66,62 @@ int main(void)
}
e_acsl_end_loop3: ;
__e_acsl_assert(__gen_e_acsl_forall_3,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 < x < 1 ==> \\false",11);
- }
- /*@ assert ∀ ℤ x; 0 ≤ x < 1 ⇒ x ≡ 0; */
- {
- int __gen_e_acsl_forall_4;
- int __gen_e_acsl_x_4;
- __gen_e_acsl_forall_4 = 1;
- __gen_e_acsl_x_4 = 0;
- while (1) {
- if (__gen_e_acsl_x_4 < 1) ; else break;
- if (__gen_e_acsl_x_4 == 0) ;
- else {
- __gen_e_acsl_forall_4 = 0;
- goto e_acsl_end_loop4;
- }
- __gen_e_acsl_x_4 ++;
- }
- e_acsl_end_loop4: ;
- __e_acsl_assert(__gen_e_acsl_forall_4,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 <= x < 1 ==> x == 0",12);
+ (char *)"\\forall integer x; 0 <= x < 1 ==> x == 0",11);
}
/*@ assert
∀ ℤ x, ℤ y, ℤ z;
0 ≤ x < 2 ∧ 0 ≤ y < 5 ∧ 0 ≤ z ≤ y ⇒ x + z ≤ y + 1;
*/
{
- int __gen_e_acsl_forall_5;
- int __gen_e_acsl_x_5;
+ int __gen_e_acsl_forall_4;
+ int __gen_e_acsl_x_4;
int __gen_e_acsl_y;
int __gen_e_acsl_z;
- __gen_e_acsl_forall_5 = 1;
- __gen_e_acsl_x_5 = 0;
+ __gen_e_acsl_forall_4 = 1;
+ __gen_e_acsl_x_4 = 0;
while (1) {
- if (__gen_e_acsl_x_5 < 2) ; else break;
+ if (__gen_e_acsl_x_4 < 2) ; else break;
__gen_e_acsl_y = 0;
while (1) {
if (__gen_e_acsl_y < 5) ; else break;
__gen_e_acsl_z = 0;
while (1) {
if (__gen_e_acsl_z <= __gen_e_acsl_y) ; else break;
- if (__gen_e_acsl_x_5 + __gen_e_acsl_z <= __gen_e_acsl_y + 1)
+ if (__gen_e_acsl_x_4 + __gen_e_acsl_z <= __gen_e_acsl_y + 1)
;
else {
- __gen_e_acsl_forall_5 = 0;
- goto e_acsl_end_loop5;
+ __gen_e_acsl_forall_4 = 0;
+ goto e_acsl_end_loop4;
}
__gen_e_acsl_z ++;
}
__gen_e_acsl_y ++;
}
- __gen_e_acsl_x_5 ++;
+ __gen_e_acsl_x_4 ++;
}
- e_acsl_end_loop5: ;
- __e_acsl_assert(__gen_e_acsl_forall_5,(char *)"Assertion",(char *)"main",
+ e_acsl_end_loop4: ;
+ __e_acsl_assert(__gen_e_acsl_forall_4,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x, integer y, integer z;\n 0 <= x < 2 && 0 <= y < 5 && 0 <= z <= y ==> x + z <= y + 1",
- 16);
+ 15);
}
/*@ assert ∃ int x; 0 ≤ x < 10 ∧ x ≡ 5; */
{
int __gen_e_acsl_exists;
- int __gen_e_acsl_x_6;
+ int __gen_e_acsl_x_5;
__gen_e_acsl_exists = 0;
- __gen_e_acsl_x_6 = 0;
+ __gen_e_acsl_x_5 = 0;
while (1) {
- if (__gen_e_acsl_x_6 < 10) ; else break;
- if (! (__gen_e_acsl_x_6 == 5)) ;
+ if (__gen_e_acsl_x_5 < 10) ; else break;
+ if (! (__gen_e_acsl_x_5 == 5)) ;
else {
__gen_e_acsl_exists = 1;
- goto e_acsl_end_loop6;
+ goto e_acsl_end_loop5;
}
- __gen_e_acsl_x_6 ++;
+ __gen_e_acsl_x_5 ++;
}
- e_acsl_end_loop6: ;
+ e_acsl_end_loop5: ;
__e_acsl_assert(__gen_e_acsl_exists,(char *)"Assertion",(char *)"main",
- (char *)"\\exists int x; 0 <= x < 10 && x == 5",21);
+ (char *)"\\exists int x; 0 <= x < 10 && x == 5",20);
}
/*@ assert
∀ int x;
@@ -148,44 +129,44 @@ int main(void)
x % 2 ≡ 0 ⇒ (∃ ℤ y; 0 ≤ y ≤ x / 2 ∧ x ≡ 2 * y);
*/
{
- int __gen_e_acsl_forall_6;
- int __gen_e_acsl_x_7;
- __gen_e_acsl_forall_6 = 1;
- __gen_e_acsl_x_7 = 0;
+ int __gen_e_acsl_forall_5;
+ int __gen_e_acsl_x_6;
+ __gen_e_acsl_forall_5 = 1;
+ __gen_e_acsl_x_6 = 0;
while (1) {
- if (__gen_e_acsl_x_7 < 10) ; else break;
+ if (__gen_e_acsl_x_6 < 10) ; else break;
{
int __gen_e_acsl_implies;
- if (! (__gen_e_acsl_x_7 % 2 == 0)) __gen_e_acsl_implies = 1;
+ if (! (__gen_e_acsl_x_6 % 2 == 0)) __gen_e_acsl_implies = 1;
else {
int __gen_e_acsl_exists_2;
int __gen_e_acsl_y_2;
__gen_e_acsl_exists_2 = 0;
__gen_e_acsl_y_2 = 0;
while (1) {
- if (__gen_e_acsl_y_2 <= __gen_e_acsl_x_7 / 2) ; else break;
- if (! (__gen_e_acsl_x_7 == 2 * __gen_e_acsl_y_2)) ;
+ if (__gen_e_acsl_y_2 <= __gen_e_acsl_x_6 / 2) ; else break;
+ if (! (__gen_e_acsl_x_6 == 2 * __gen_e_acsl_y_2)) ;
else {
__gen_e_acsl_exists_2 = 1;
- goto e_acsl_end_loop7;
+ goto e_acsl_end_loop6;
}
__gen_e_acsl_y_2 ++;
}
- e_acsl_end_loop7: ;
+ e_acsl_end_loop6: ;
__gen_e_acsl_implies = __gen_e_acsl_exists_2;
}
if (__gen_e_acsl_implies) ;
else {
- __gen_e_acsl_forall_6 = 0;
- goto e_acsl_end_loop8;
+ __gen_e_acsl_forall_5 = 0;
+ goto e_acsl_end_loop7;
}
}
- __gen_e_acsl_x_7 ++;
+ __gen_e_acsl_x_6 ++;
}
- e_acsl_end_loop8: ;
- __e_acsl_assert(__gen_e_acsl_forall_6,(char *)"Assertion",(char *)"main",
+ e_acsl_end_loop7: ;
+ __e_acsl_assert(__gen_e_acsl_forall_5,(char *)"Assertion",(char *)"main",
(char *)"\\forall int x;\n 0 <= x < 10 ==>\n x % 2 == 0 ==> (\\exists integer y; 0 <= y <= x / 2 && x == 2 * y)",
- 25);
+ 24);
}
{
int buf[10];
@@ -193,9 +174,9 @@ int main(void)
unsigned long len = (unsigned long)9;
/*@ assert ∀ ℤ i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
{
- int __gen_e_acsl_forall_7;
+ int __gen_e_acsl_forall_6;
int __gen_e_acsl_i;
- __gen_e_acsl_forall_7 = 1;
+ __gen_e_acsl_forall_6 = 1;
__gen_e_acsl_i = 0;
while (1) {
if (__gen_e_acsl_i < 10) ; else break;
@@ -207,23 +188,23 @@ int main(void)
(void *)0);
if (__gen_e_acsl_valid) ;
else {
- __gen_e_acsl_forall_7 = 0;
- goto e_acsl_end_loop9;
+ __gen_e_acsl_forall_6 = 0;
+ goto e_acsl_end_loop8;
}
}
__gen_e_acsl_i ++;
}
- e_acsl_end_loop9: ;
- __e_acsl_assert(__gen_e_acsl_forall_7,(char *)"Assertion",
+ e_acsl_end_loop8: ;
+ __e_acsl_assert(__gen_e_acsl_forall_6,(char *)"Assertion",
(char *)"main",
(char *)"\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])",
- 31);
+ 30);
}
/*@ assert ∀ char i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
{
- int __gen_e_acsl_forall_8;
+ int __gen_e_acsl_forall_7;
int __gen_e_acsl_i_2;
- __gen_e_acsl_forall_8 = 1;
+ __gen_e_acsl_forall_7 = 1;
__gen_e_acsl_i_2 = (char)0;
while (1) {
if (__gen_e_acsl_i_2 < 10) ; else break;
@@ -235,23 +216,23 @@ int main(void)
(void *)0);
if (__gen_e_acsl_valid_2) ;
else {
- __gen_e_acsl_forall_8 = 0;
- goto e_acsl_end_loop10;
+ __gen_e_acsl_forall_7 = 0;
+ goto e_acsl_end_loop9;
}
}
__gen_e_acsl_i_2 ++;
}
- e_acsl_end_loop10: ;
- __e_acsl_assert(__gen_e_acsl_forall_8,(char *)"Assertion",
+ e_acsl_end_loop9: ;
+ __e_acsl_assert(__gen_e_acsl_forall_7,(char *)"Assertion",
(char *)"main",
(char *)"\\forall char i; 0 <= i < 10 ==> \\valid(&buf[i])",
- 32);
+ 31);
}
/*@ assert ∀ ℤ i; 0 ≤ i < len ⇒ \valid(&buf[i]); */
{
- int __gen_e_acsl_forall_9;
+ int __gen_e_acsl_forall_8;
unsigned long __gen_e_acsl_i_3;
- __gen_e_acsl_forall_9 = 1;
+ __gen_e_acsl_forall_8 = 1;
__gen_e_acsl_i_3 = 0UL;
while (1) {
if (__gen_e_acsl_i_3 < len) ; else break;
@@ -263,23 +244,23 @@ int main(void)
(void *)0);
if (__gen_e_acsl_valid_3) ;
else {
- __gen_e_acsl_forall_9 = 0;
- goto e_acsl_end_loop11;
+ __gen_e_acsl_forall_8 = 0;
+ goto e_acsl_end_loop10;
}
}
__gen_e_acsl_i_3 ++;
}
- e_acsl_end_loop11: ;
- __e_acsl_assert(__gen_e_acsl_forall_9,(char *)"Assertion",
+ e_acsl_end_loop10: ;
+ __e_acsl_assert(__gen_e_acsl_forall_8,(char *)"Assertion",
(char *)"main",
(char *)"\\forall integer i; 0 <= i < len ==> \\valid(&buf[i])",
- 33);
+ 32);
}
/*@ assert ∀ ℤ i; 0 ≤ i ≤ len ⇒ \valid(&buf[i]); */
{
- int __gen_e_acsl_forall_10;
+ int __gen_e_acsl_forall_9;
__e_acsl_mpz_t __gen_e_acsl_i_4;
- __gen_e_acsl_forall_10 = 1;
+ __gen_e_acsl_forall_9 = 1;
__gmpz_init(__gen_e_acsl_i_4);
{
__e_acsl_mpz_t __gen_e_acsl_;
@@ -308,8 +289,8 @@ int main(void)
(void *)0);
if (__gen_e_acsl_valid_4) ;
else {
- __gen_e_acsl_forall_10 = 0;
- goto e_acsl_end_loop12;
+ __gen_e_acsl_forall_9 = 0;
+ goto e_acsl_end_loop11;
}
}
{
@@ -326,15 +307,31 @@ int main(void)
__gmpz_clear(__gen_e_acsl_add);
}
}
- e_acsl_end_loop12: ;
- __e_acsl_assert(__gen_e_acsl_forall_10,(char *)"Assertion",
+ e_acsl_end_loop11: ;
+ __e_acsl_assert(__gen_e_acsl_forall_9,(char *)"Assertion",
(char *)"main",
(char *)"\\forall integer i; 0 <= i <= len ==> \\valid(&buf[i])",
- 34);
+ 33);
__gmpz_clear(__gen_e_acsl_i_4);
__e_acsl_delete_block((void *)(buf));
}
}
+ /*@ assert ∀ ℤ x; 0 < x < 1 ⇒ \false; */
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
+ (char *)"\\forall integer x; 0 < x < 1 ==> \\false",37);
+ /*@ assert ¬(∃ char c; 10 ≤ c < 10 ∧ c ≡ 10); */
+ __e_acsl_assert(! 0,(char *)"Assertion",(char *)"main",
+ (char *)"!(\\exists char c; 10 <= c < 10 && c == 10)",38);
+ /*@ assert \let u = 5;
+ ∀ ℤ x, ℤ y; 0 ≤ x < 2 ∧ 4 < y < u ⇒ \false;
+ */
+ {
+ int __gen_e_acsl_u;
+ __gen_e_acsl_u = 5;
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
+ (char *)"\\let u = 5;\n\\forall integer x, integer y; 0 <= x < 2 && 4 < y < u ==> \\false",
+ 40);
+ }
__retres = 0;
__e_acsl_memory_clean();
return __retres;
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 505ab56a8bc..4559cf6c2d5 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
@@ -136,27 +136,18 @@ int main(void)
(char *)"\\forall integer x; 0 < x <= 1 ==> x == 1",10);
__gmpz_clear(__gen_e_acsl_x_2);
}
- /*@ assert ∀ ℤ x; 0 < x < 1 ⇒ \false; */
+ /*@ assert ∀ ℤ x; 0 ≤ x < 1 ⇒ x ≡ 0; */
{
int __gen_e_acsl_forall_3;
__e_acsl_mpz_t __gen_e_acsl_x_3;
__gen_e_acsl_forall_3 = 1;
__gmpz_init(__gen_e_acsl_x_3);
{
- __e_acsl_mpz_t __gen_e_acsl__11;
__e_acsl_mpz_t __gen_e_acsl__12;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __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,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
+ __gmpz_init_set_si(__gen_e_acsl__12,0L);
__gmpz_set(__gen_e_acsl_x_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
- __gmpz_clear(__gen_e_acsl__11);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
__gmpz_clear(__gen_e_acsl__12);
- __gmpz_clear(__gen_e_acsl_add_4);
}
while (1) {
{
@@ -168,138 +159,91 @@ int main(void)
if (__gen_e_acsl_lt < 0) ; else break;
__gmpz_clear(__gen_e_acsl__13);
}
- if (0) ;
- else {
- __gen_e_acsl_forall_3 = 0;
- goto e_acsl_end_loop3;
+ {
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ int __gen_e_acsl_eq_4;
+ __gmpz_init_set_si(__gen_e_acsl__11,0L);
+ __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __gmpz_clear(__gen_e_acsl__11);
+ if (__gen_e_acsl_eq_4 == 0) ;
+ else {
+ __gen_e_acsl_forall_3 = 0;
+ goto e_acsl_end_loop3;
+ }
}
{
__e_acsl_mpz_t __gen_e_acsl__14;
- __e_acsl_mpz_t __gen_e_acsl_add_5;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
__gmpz_init_set_str(__gen_e_acsl__14,"1",10);
- __gmpz_init(__gen_e_acsl_add_5);
- __gmpz_add(__gen_e_acsl_add_5,
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
__gmpz_set(__gen_e_acsl_x_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
__gmpz_clear(__gen_e_acsl__14);
- __gmpz_clear(__gen_e_acsl_add_5);
+ __gmpz_clear(__gen_e_acsl_add_4);
}
}
e_acsl_end_loop3: ;
__e_acsl_assert(__gen_e_acsl_forall_3,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 < x < 1 ==> \\false",11);
+ (char *)"\\forall integer x; 0 <= x < 1 ==> x == 0",11);
__gmpz_clear(__gen_e_acsl_x_3);
}
- /*@ assert ∀ ℤ x; 0 ≤ x < 1 ⇒ x ≡ 0; */
- {
- int __gen_e_acsl_forall_4;
- __e_acsl_mpz_t __gen_e_acsl_x_4;
- __gen_e_acsl_forall_4 = 1;
- __gmpz_init(__gen_e_acsl_x_4);
- {
- __e_acsl_mpz_t __gen_e_acsl__16;
- __gmpz_init_set_si(__gen_e_acsl__16,0L);
- __gmpz_set(__gen_e_acsl_x_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
- __gmpz_clear(__gen_e_acsl__16);
- }
- while (1) {
- {
- __e_acsl_mpz_t __gen_e_acsl__17;
- int __gen_e_acsl_lt_2;
- __gmpz_init_set_si(__gen_e_acsl__17,1L);
- __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__17));
- if (__gen_e_acsl_lt_2 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__17);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__15;
- int __gen_e_acsl_eq_4;
- __gmpz_init_set_si(__gen_e_acsl__15,0L);
- __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
- __gmpz_clear(__gen_e_acsl__15);
- if (__gen_e_acsl_eq_4 == 0) ;
- else {
- __gen_e_acsl_forall_4 = 0;
- goto e_acsl_end_loop4;
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__18;
- __e_acsl_mpz_t __gen_e_acsl_add_6;
- __gmpz_init_set_str(__gen_e_acsl__18,"1",10);
- __gmpz_init(__gen_e_acsl_add_6);
- __gmpz_add(__gen_e_acsl_add_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__18));
- __gmpz_set(__gen_e_acsl_x_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
- __gmpz_clear(__gen_e_acsl__18);
- __gmpz_clear(__gen_e_acsl_add_6);
- }
- }
- e_acsl_end_loop4: ;
- __e_acsl_assert(__gen_e_acsl_forall_4,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 <= x < 1 ==> x == 0",12);
- __gmpz_clear(__gen_e_acsl_x_4);
- }
/*@ assert
∀ ℤ x, ℤ y, ℤ z;
0 ≤ x < 2 ∧ 0 ≤ y < 5 ∧ 0 ≤ z ≤ y ⇒ x + z ≤ y + 1;
*/
{
- int __gen_e_acsl_forall_5;
- __e_acsl_mpz_t __gen_e_acsl_x_5;
+ int __gen_e_acsl_forall_4;
+ __e_acsl_mpz_t __gen_e_acsl_x_4;
__e_acsl_mpz_t __gen_e_acsl_y;
__e_acsl_mpz_t __gen_e_acsl_z;
- __gen_e_acsl_forall_5 = 1;
- __gmpz_init(__gen_e_acsl_x_5);
+ __gen_e_acsl_forall_4 = 1;
+ __gmpz_init(__gen_e_acsl_x_4);
__gmpz_init(__gen_e_acsl_y);
__gmpz_init(__gen_e_acsl_z);
{
- __e_acsl_mpz_t __gen_e_acsl__25;
- __gmpz_init_set_si(__gen_e_acsl__25,0L);
- __gmpz_set(__gen_e_acsl_x_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
- __gmpz_clear(__gen_e_acsl__25);
+ __e_acsl_mpz_t __gen_e_acsl__21;
+ __gmpz_init_set_si(__gen_e_acsl__21,0L);
+ __gmpz_set(__gen_e_acsl_x_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
+ __gmpz_clear(__gen_e_acsl__21);
}
while (1) {
{
- __e_acsl_mpz_t __gen_e_acsl__26;
- int __gen_e_acsl_lt_4;
- __gmpz_init_set_si(__gen_e_acsl__26,2L);
- __gen_e_acsl_lt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
- if (__gen_e_acsl_lt_4 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__26);
+ __e_acsl_mpz_t __gen_e_acsl__22;
+ int __gen_e_acsl_lt_3;
+ __gmpz_init_set_si(__gen_e_acsl__22,2L);
+ __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__22));
+ if (__gen_e_acsl_lt_3 < 0) ; else break;
+ __gmpz_clear(__gen_e_acsl__22);
}
{
- __e_acsl_mpz_t __gen_e_acsl__22;
- __gmpz_init_set_si(__gen_e_acsl__22,0L);
+ __e_acsl_mpz_t __gen_e_acsl__18;
+ __gmpz_init_set_si(__gen_e_acsl__18,0L);
__gmpz_set(__gen_e_acsl_y,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__22));
- __gmpz_clear(__gen_e_acsl__22);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__18));
+ __gmpz_clear(__gen_e_acsl__18);
}
while (1) {
{
- __e_acsl_mpz_t __gen_e_acsl__23;
- int __gen_e_acsl_lt_3;
- __gmpz_init_set_si(__gen_e_acsl__23,5L);
- __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_y),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__23));
- if (__gen_e_acsl_lt_3 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__23);
+ __e_acsl_mpz_t __gen_e_acsl__19;
+ int __gen_e_acsl_lt_2;
+ __gmpz_init_set_si(__gen_e_acsl__19,5L);
+ __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_y),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__19));
+ if (__gen_e_acsl_lt_2 < 0) ; else break;
+ __gmpz_clear(__gen_e_acsl__19);
}
{
- __e_acsl_mpz_t __gen_e_acsl__20;
- __gmpz_init_set_si(__gen_e_acsl__20,0L);
+ __e_acsl_mpz_t __gen_e_acsl__16;
+ __gmpz_init_set_si(__gen_e_acsl__16,0L);
__gmpz_set(__gen_e_acsl_z,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__20));
- __gmpz_clear(__gen_e_acsl__20);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
+ __gmpz_clear(__gen_e_acsl__16);
}
while (1) {
{
@@ -309,134 +253,134 @@ int main(void)
if (__gen_e_acsl_le_4 <= 0) ; else break;
}
{
- __e_acsl_mpz_t __gen_e_acsl_add_7;
- __e_acsl_mpz_t __gen_e_acsl__19;
- __e_acsl_mpz_t __gen_e_acsl_add_8;
+ __e_acsl_mpz_t __gen_e_acsl_add_5;
+ __e_acsl_mpz_t __gen_e_acsl__15;
+ __e_acsl_mpz_t __gen_e_acsl_add_6;
int __gen_e_acsl_le_3;
- __gmpz_init(__gen_e_acsl_add_7);
- __gmpz_add(__gen_e_acsl_add_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
+ __gmpz_init(__gen_e_acsl_add_5);
+ __gmpz_add(__gen_e_acsl_add_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_z));
- __gmpz_init_set_si(__gen_e_acsl__19,1L);
- __gmpz_init(__gen_e_acsl_add_8);
- __gmpz_add(__gen_e_acsl_add_8,
+ __gmpz_init_set_si(__gen_e_acsl__15,1L);
+ __gmpz_init(__gen_e_acsl_add_6);
+ __gmpz_add(__gen_e_acsl_add_6,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_y),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__19));
- __gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_8));
- __gmpz_clear(__gen_e_acsl_add_7);
- __gmpz_clear(__gen_e_acsl__19);
- __gmpz_clear(__gen_e_acsl_add_8);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
+ __gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
+ __gmpz_clear(__gen_e_acsl_add_5);
+ __gmpz_clear(__gen_e_acsl__15);
+ __gmpz_clear(__gen_e_acsl_add_6);
if (__gen_e_acsl_le_3 <= 0) ;
else {
- __gen_e_acsl_forall_5 = 0;
- goto e_acsl_end_loop5;
+ __gen_e_acsl_forall_4 = 0;
+ goto e_acsl_end_loop4;
}
}
{
- __e_acsl_mpz_t __gen_e_acsl__21;
- __e_acsl_mpz_t __gen_e_acsl_add_9;
- __gmpz_init_set_str(__gen_e_acsl__21,"1",10);
- __gmpz_init(__gen_e_acsl_add_9);
- __gmpz_add(__gen_e_acsl_add_9,
+ __e_acsl_mpz_t __gen_e_acsl__17;
+ __e_acsl_mpz_t __gen_e_acsl_add_7;
+ __gmpz_init_set_str(__gen_e_acsl__17,"1",10);
+ __gmpz_init(__gen_e_acsl_add_7);
+ __gmpz_add(__gen_e_acsl_add_7,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_z),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__17));
__gmpz_set(__gen_e_acsl_z,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_9));
- __gmpz_clear(__gen_e_acsl__21);
- __gmpz_clear(__gen_e_acsl_add_9);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
+ __gmpz_clear(__gen_e_acsl__17);
+ __gmpz_clear(__gen_e_acsl_add_7);
}
}
{
- __e_acsl_mpz_t __gen_e_acsl__24;
- __e_acsl_mpz_t __gen_e_acsl_add_10;
- __gmpz_init_set_str(__gen_e_acsl__24,"1",10);
- __gmpz_init(__gen_e_acsl_add_10);
- __gmpz_add(__gen_e_acsl_add_10,
+ __e_acsl_mpz_t __gen_e_acsl__20;
+ __e_acsl_mpz_t __gen_e_acsl_add_8;
+ __gmpz_init_set_str(__gen_e_acsl__20,"1",10);
+ __gmpz_init(__gen_e_acsl_add_8);
+ __gmpz_add(__gen_e_acsl_add_8,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_y),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__20));
__gmpz_set(__gen_e_acsl_y,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_10));
- __gmpz_clear(__gen_e_acsl__24);
- __gmpz_clear(__gen_e_acsl_add_10);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_8));
+ __gmpz_clear(__gen_e_acsl__20);
+ __gmpz_clear(__gen_e_acsl_add_8);
}
}
{
- __e_acsl_mpz_t __gen_e_acsl__27;
- __e_acsl_mpz_t __gen_e_acsl_add_11;
- __gmpz_init_set_str(__gen_e_acsl__27,"1",10);
- __gmpz_init(__gen_e_acsl_add_11);
- __gmpz_add(__gen_e_acsl_add_11,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__27));
- __gmpz_set(__gen_e_acsl_x_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_11));
- __gmpz_clear(__gen_e_acsl__27);
- __gmpz_clear(__gen_e_acsl_add_11);
+ __e_acsl_mpz_t __gen_e_acsl__23;
+ __e_acsl_mpz_t __gen_e_acsl_add_9;
+ __gmpz_init_set_str(__gen_e_acsl__23,"1",10);
+ __gmpz_init(__gen_e_acsl_add_9);
+ __gmpz_add(__gen_e_acsl_add_9,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__23));
+ __gmpz_set(__gen_e_acsl_x_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_9));
+ __gmpz_clear(__gen_e_acsl__23);
+ __gmpz_clear(__gen_e_acsl_add_9);
}
}
- e_acsl_end_loop5: ;
- __e_acsl_assert(__gen_e_acsl_forall_5,(char *)"Assertion",(char *)"main",
+ e_acsl_end_loop4: ;
+ __e_acsl_assert(__gen_e_acsl_forall_4,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x, integer y, integer z;\n 0 <= x < 2 && 0 <= y < 5 && 0 <= z <= y ==> x + z <= y + 1",
- 16);
- __gmpz_clear(__gen_e_acsl_x_5);
+ 15);
+ __gmpz_clear(__gen_e_acsl_x_4);
__gmpz_clear(__gen_e_acsl_y);
__gmpz_clear(__gen_e_acsl_z);
}
/*@ assert ∃ int x; 0 ≤ x < 10 ∧ x ≡ 5; */
{
int __gen_e_acsl_exists;
- __e_acsl_mpz_t __gen_e_acsl_x_6;
+ __e_acsl_mpz_t __gen_e_acsl_x_5;
__gen_e_acsl_exists = 0;
- __gmpz_init(__gen_e_acsl_x_6);
+ __gmpz_init(__gen_e_acsl_x_5);
{
- __e_acsl_mpz_t __gen_e_acsl__29;
- __gmpz_init_set_si(__gen_e_acsl__29,0L);
- __gmpz_set(__gen_e_acsl_x_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
- __gmpz_clear(__gen_e_acsl__29);
+ __e_acsl_mpz_t __gen_e_acsl__25;
+ __gmpz_init_set_si(__gen_e_acsl__25,0L);
+ __gmpz_set(__gen_e_acsl_x_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
+ __gmpz_clear(__gen_e_acsl__25);
}
while (1) {
{
- __e_acsl_mpz_t __gen_e_acsl__30;
- int __gen_e_acsl_lt_5;
- __gmpz_init_set_si(__gen_e_acsl__30,10L);
- __gen_e_acsl_lt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__30));
- if (__gen_e_acsl_lt_5 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__30);
+ __e_acsl_mpz_t __gen_e_acsl__26;
+ int __gen_e_acsl_lt_4;
+ __gmpz_init_set_si(__gen_e_acsl__26,10L);
+ __gen_e_acsl_lt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
+ if (__gen_e_acsl_lt_4 < 0) ; else break;
+ __gmpz_clear(__gen_e_acsl__26);
}
{
- __e_acsl_mpz_t __gen_e_acsl__28;
+ __e_acsl_mpz_t __gen_e_acsl__24;
int __gen_e_acsl_eq_5;
- __gmpz_init_set_si(__gen_e_acsl__28,5L);
- __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__28));
- __gmpz_clear(__gen_e_acsl__28);
+ __gmpz_init_set_si(__gen_e_acsl__24,5L);
+ __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
+ __gmpz_clear(__gen_e_acsl__24);
if (! (__gen_e_acsl_eq_5 == 0)) ;
else {
__gen_e_acsl_exists = 1;
- goto e_acsl_end_loop6;
+ goto e_acsl_end_loop5;
}
}
{
- __e_acsl_mpz_t __gen_e_acsl__31;
- __e_acsl_mpz_t __gen_e_acsl_add_12;
- __gmpz_init_set_str(__gen_e_acsl__31,"1",10);
- __gmpz_init(__gen_e_acsl_add_12);
- __gmpz_add(__gen_e_acsl_add_12,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__31));
- __gmpz_set(__gen_e_acsl_x_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_12));
- __gmpz_clear(__gen_e_acsl__31);
- __gmpz_clear(__gen_e_acsl_add_12);
+ __e_acsl_mpz_t __gen_e_acsl__27;
+ __e_acsl_mpz_t __gen_e_acsl_add_10;
+ __gmpz_init_set_str(__gen_e_acsl__27,"1",10);
+ __gmpz_init(__gen_e_acsl_add_10);
+ __gmpz_add(__gen_e_acsl_add_10,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__27));
+ __gmpz_set(__gen_e_acsl_x_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_10));
+ __gmpz_clear(__gen_e_acsl__27);
+ __gmpz_clear(__gen_e_acsl_add_10);
}
}
- e_acsl_end_loop6: ;
+ e_acsl_end_loop5: ;
__e_acsl_assert(__gen_e_acsl_exists,(char *)"Assertion",(char *)"main",
- (char *)"\\exists int x; 0 <= x < 10 && x == 5",21);
- __gmpz_clear(__gen_e_acsl_x_6);
+ (char *)"\\exists int x; 0 <= x < 10 && x == 5",20);
+ __gmpz_clear(__gen_e_acsl_x_5);
}
/*@ assert
∀ int x;
@@ -444,47 +388,47 @@ int main(void)
x % 2 ≡ 0 ⇒ (∃ ℤ y; 0 ≤ y ≤ x / 2 ∧ x ≡ 2 * y);
*/
{
- int __gen_e_acsl_forall_6;
- __e_acsl_mpz_t __gen_e_acsl_x_7;
- __gen_e_acsl_forall_6 = 1;
- __gmpz_init(__gen_e_acsl_x_7);
+ int __gen_e_acsl_forall_5;
+ __e_acsl_mpz_t __gen_e_acsl_x_6;
+ __gen_e_acsl_forall_5 = 1;
+ __gmpz_init(__gen_e_acsl_x_6);
{
- __e_acsl_mpz_t __gen_e_acsl__39;
- __gmpz_init_set_si(__gen_e_acsl__39,0L);
- __gmpz_set(__gen_e_acsl_x_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__39));
- __gmpz_clear(__gen_e_acsl__39);
+ __e_acsl_mpz_t __gen_e_acsl__35;
+ __gmpz_init_set_si(__gen_e_acsl__35,0L);
+ __gmpz_set(__gen_e_acsl_x_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__35));
+ __gmpz_clear(__gen_e_acsl__35);
}
while (1) {
{
- __e_acsl_mpz_t __gen_e_acsl__40;
- int __gen_e_acsl_lt_6;
- __gmpz_init_set_si(__gen_e_acsl__40,10L);
- __gen_e_acsl_lt_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__40));
- if (__gen_e_acsl_lt_6 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__40);
+ __e_acsl_mpz_t __gen_e_acsl__36;
+ int __gen_e_acsl_lt_5;
+ __gmpz_init_set_si(__gen_e_acsl__36,10L);
+ __gen_e_acsl_lt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__36));
+ if (__gen_e_acsl_lt_5 < 0) ; else break;
+ __gmpz_clear(__gen_e_acsl__36);
}
{
- __e_acsl_mpz_t __gen_e_acsl__32;
- __e_acsl_mpz_t __gen_e_acsl__33;
+ __e_acsl_mpz_t __gen_e_acsl__28;
+ __e_acsl_mpz_t __gen_e_acsl__29;
int __gen_e_acsl_mod_guard;
__e_acsl_mpz_t __gen_e_acsl_mod;
int __gen_e_acsl_eq_6;
int __gen_e_acsl_implies;
- __gmpz_init_set_si(__gen_e_acsl__32,2L);
- __gmpz_init_set_si(__gen_e_acsl__33,0L);
- __gen_e_acsl_mod_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__32),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
+ __gmpz_init_set_si(__gen_e_acsl__28,2L);
+ __gmpz_init_set_si(__gen_e_acsl__29,0L);
+ __gen_e_acsl_mod_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__28),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
__gmpz_init(__gen_e_acsl_mod);
/*@ assert E_ACSL: 2 ≢ 0; */
__e_acsl_assert(! (__gen_e_acsl_mod_guard == 0),(char *)"Assertion",
- (char *)"main",(char *)"2 == 0",26);
+ (char *)"main",(char *)"2 == 0",25);
__gmpz_tdiv_r(__gen_e_acsl_mod,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__28));
__gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mod),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
if (! (__gen_e_acsl_eq_6 == 0)) __gen_e_acsl_implies = 1;
else {
int __gen_e_acsl_exists_2;
@@ -492,103 +436,103 @@ int main(void)
__gen_e_acsl_exists_2 = 0;
__gmpz_init(__gen_e_acsl_y_2);
{
- __e_acsl_mpz_t __gen_e_acsl__35;
- __gmpz_init_set_si(__gen_e_acsl__35,0L);
+ __e_acsl_mpz_t __gen_e_acsl__31;
+ __gmpz_init_set_si(__gen_e_acsl__31,0L);
__gmpz_set(__gen_e_acsl_y_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__35));
- __gmpz_clear(__gen_e_acsl__35);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__31));
+ __gmpz_clear(__gen_e_acsl__31);
}
while (1) {
{
- __e_acsl_mpz_t __gen_e_acsl__36;
- __e_acsl_mpz_t __gen_e_acsl__37;
+ __e_acsl_mpz_t __gen_e_acsl__32;
+ __e_acsl_mpz_t __gen_e_acsl__33;
int __gen_e_acsl_div_guard;
__e_acsl_mpz_t __gen_e_acsl_div;
int __gen_e_acsl_le_5;
- __gmpz_init_set_si(__gen_e_acsl__36,2L);
- __gmpz_init_set_si(__gen_e_acsl__37,0L);
- __gen_e_acsl_div_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__36),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__37));
+ __gmpz_init_set_si(__gen_e_acsl__32,2L);
+ __gmpz_init_set_si(__gen_e_acsl__33,0L);
+ __gen_e_acsl_div_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__32),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
__gmpz_init(__gen_e_acsl_div);
/*@ assert E_ACSL: 2 ≢ 0; */
__e_acsl_assert(! (__gen_e_acsl_div_guard == 0),
(char *)"Assertion",(char *)"main",
- (char *)"2 == 0",26);
+ (char *)"2 == 0",25);
__gmpz_tdiv_q(__gen_e_acsl_div,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__36));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
__gen_e_acsl_le_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_div));
if (__gen_e_acsl_le_5 <= 0) ; else break;
- __gmpz_clear(__gen_e_acsl__36);
- __gmpz_clear(__gen_e_acsl__37);
+ __gmpz_clear(__gen_e_acsl__32);
+ __gmpz_clear(__gen_e_acsl__33);
__gmpz_clear(__gen_e_acsl_div);
}
{
- __e_acsl_mpz_t __gen_e_acsl__34;
+ __e_acsl_mpz_t __gen_e_acsl__30;
__e_acsl_mpz_t __gen_e_acsl_mul;
int __gen_e_acsl_eq_7;
- __gmpz_init_set_si(__gen_e_acsl__34,2L);
+ __gmpz_init_set_si(__gen_e_acsl__30,2L);
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__34),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__30),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
- __gen_e_acsl_eq_7 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_7),
+ __gen_e_acsl_eq_7 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
- __gmpz_clear(__gen_e_acsl__34);
+ __gmpz_clear(__gen_e_acsl__30);
__gmpz_clear(__gen_e_acsl_mul);
if (! (__gen_e_acsl_eq_7 == 0)) ;
else {
__gen_e_acsl_exists_2 = 1;
- goto e_acsl_end_loop7;
+ goto e_acsl_end_loop6;
}
}
{
- __e_acsl_mpz_t __gen_e_acsl__38;
- __e_acsl_mpz_t __gen_e_acsl_add_13;
- __gmpz_init_set_str(__gen_e_acsl__38,"1",10);
- __gmpz_init(__gen_e_acsl_add_13);
- __gmpz_add(__gen_e_acsl_add_13,
+ __e_acsl_mpz_t __gen_e_acsl__34;
+ __e_acsl_mpz_t __gen_e_acsl_add_11;
+ __gmpz_init_set_str(__gen_e_acsl__34,"1",10);
+ __gmpz_init(__gen_e_acsl_add_11);
+ __gmpz_add(__gen_e_acsl_add_11,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__38));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__34));
__gmpz_set(__gen_e_acsl_y_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_13));
- __gmpz_clear(__gen_e_acsl__38);
- __gmpz_clear(__gen_e_acsl_add_13);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_11));
+ __gmpz_clear(__gen_e_acsl__34);
+ __gmpz_clear(__gen_e_acsl_add_11);
}
}
- e_acsl_end_loop7: ;
+ e_acsl_end_loop6: ;
__gen_e_acsl_implies = __gen_e_acsl_exists_2;
__gmpz_clear(__gen_e_acsl_y_2);
}
- __gmpz_clear(__gen_e_acsl__32);
- __gmpz_clear(__gen_e_acsl__33);
+ __gmpz_clear(__gen_e_acsl__28);
+ __gmpz_clear(__gen_e_acsl__29);
__gmpz_clear(__gen_e_acsl_mod);
if (__gen_e_acsl_implies) ;
else {
- __gen_e_acsl_forall_6 = 0;
- goto e_acsl_end_loop8;
+ __gen_e_acsl_forall_5 = 0;
+ goto e_acsl_end_loop7;
}
}
{
- __e_acsl_mpz_t __gen_e_acsl__41;
- __e_acsl_mpz_t __gen_e_acsl_add_14;
- __gmpz_init_set_str(__gen_e_acsl__41,"1",10);
- __gmpz_init(__gen_e_acsl_add_14);
- __gmpz_add(__gen_e_acsl_add_14,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__41));
- __gmpz_set(__gen_e_acsl_x_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_14));
- __gmpz_clear(__gen_e_acsl__41);
- __gmpz_clear(__gen_e_acsl_add_14);
+ __e_acsl_mpz_t __gen_e_acsl__37;
+ __e_acsl_mpz_t __gen_e_acsl_add_12;
+ __gmpz_init_set_str(__gen_e_acsl__37,"1",10);
+ __gmpz_init(__gen_e_acsl_add_12);
+ __gmpz_add(__gen_e_acsl_add_12,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__37));
+ __gmpz_set(__gen_e_acsl_x_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_12));
+ __gmpz_clear(__gen_e_acsl__37);
+ __gmpz_clear(__gen_e_acsl_add_12);
}
}
- e_acsl_end_loop8: ;
- __e_acsl_assert(__gen_e_acsl_forall_6,(char *)"Assertion",(char *)"main",
+ e_acsl_end_loop7: ;
+ __e_acsl_assert(__gen_e_acsl_forall_5,(char *)"Assertion",(char *)"main",
(char *)"\\forall int x;\n 0 <= x < 10 ==>\n x % 2 == 0 ==> (\\exists integer y; 0 <= y <= x / 2 && x == 2 * y)",
- 25);
- __gmpz_clear(__gen_e_acsl_x_7);
+ 24);
+ __gmpz_clear(__gen_e_acsl_x_6);
}
{
int buf[10];
@@ -596,26 +540,26 @@ int main(void)
unsigned long len = (unsigned long)9;
/*@ assert ∀ ℤ i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
{
- int __gen_e_acsl_forall_7;
+ int __gen_e_acsl_forall_6;
__e_acsl_mpz_t __gen_e_acsl_i;
- __gen_e_acsl_forall_7 = 1;
+ __gen_e_acsl_forall_6 = 1;
__gmpz_init(__gen_e_acsl_i);
{
- __e_acsl_mpz_t __gen_e_acsl__42;
- __gmpz_init_set_si(__gen_e_acsl__42,0L);
+ __e_acsl_mpz_t __gen_e_acsl__38;
+ __gmpz_init_set_si(__gen_e_acsl__38,0L);
__gmpz_set(__gen_e_acsl_i,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__42));
- __gmpz_clear(__gen_e_acsl__42);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__38));
+ __gmpz_clear(__gen_e_acsl__38);
}
while (1) {
{
- __e_acsl_mpz_t __gen_e_acsl__43;
- int __gen_e_acsl_lt_7;
- __gmpz_init_set_si(__gen_e_acsl__43,10L);
- __gen_e_acsl_lt_7 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__43));
- if (__gen_e_acsl_lt_7 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__43);
+ __e_acsl_mpz_t __gen_e_acsl__39;
+ int __gen_e_acsl_lt_6;
+ __gmpz_init_set_si(__gen_e_acsl__39,10L);
+ __gen_e_acsl_lt_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__39));
+ if (__gen_e_acsl_lt_6 < 0) ; else break;
+ __gmpz_clear(__gen_e_acsl__39);
}
{
long __gen_e_acsl_i_2;
@@ -627,53 +571,53 @@ int main(void)
(void *)0);
if (__gen_e_acsl_valid) ;
else {
- __gen_e_acsl_forall_7 = 0;
- goto e_acsl_end_loop9;
+ __gen_e_acsl_forall_6 = 0;
+ goto e_acsl_end_loop8;
}
}
{
- __e_acsl_mpz_t __gen_e_acsl__44;
- __e_acsl_mpz_t __gen_e_acsl_add_15;
- __gmpz_init_set_str(__gen_e_acsl__44,"1",10);
- __gmpz_init(__gen_e_acsl_add_15);
- __gmpz_add(__gen_e_acsl_add_15,
+ __e_acsl_mpz_t __gen_e_acsl__40;
+ __e_acsl_mpz_t __gen_e_acsl_add_13;
+ __gmpz_init_set_str(__gen_e_acsl__40,"1",10);
+ __gmpz_init(__gen_e_acsl_add_13);
+ __gmpz_add(__gen_e_acsl_add_13,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_i),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__44));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__40));
__gmpz_set(__gen_e_acsl_i,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_15));
- __gmpz_clear(__gen_e_acsl__44);
- __gmpz_clear(__gen_e_acsl_add_15);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_13));
+ __gmpz_clear(__gen_e_acsl__40);
+ __gmpz_clear(__gen_e_acsl_add_13);
}
}
- e_acsl_end_loop9: ;
- __e_acsl_assert(__gen_e_acsl_forall_7,(char *)"Assertion",
+ e_acsl_end_loop8: ;
+ __e_acsl_assert(__gen_e_acsl_forall_6,(char *)"Assertion",
(char *)"main",
(char *)"\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])",
- 31);
+ 30);
__gmpz_clear(__gen_e_acsl_i);
}
/*@ assert ∀ char i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
{
- int __gen_e_acsl_forall_8;
+ int __gen_e_acsl_forall_7;
__e_acsl_mpz_t __gen_e_acsl_i_3;
- __gen_e_acsl_forall_8 = 1;
+ __gen_e_acsl_forall_7 = 1;
__gmpz_init(__gen_e_acsl_i_3);
{
- __e_acsl_mpz_t __gen_e_acsl__45;
- __gmpz_init_set_si(__gen_e_acsl__45,0L);
+ __e_acsl_mpz_t __gen_e_acsl__41;
+ __gmpz_init_set_si(__gen_e_acsl__41,0L);
__gmpz_set(__gen_e_acsl_i_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__45));
- __gmpz_clear(__gen_e_acsl__45);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__41));
+ __gmpz_clear(__gen_e_acsl__41);
}
while (1) {
{
- __e_acsl_mpz_t __gen_e_acsl__46;
- int __gen_e_acsl_lt_8;
- __gmpz_init_set_si(__gen_e_acsl__46,10L);
- __gen_e_acsl_lt_8 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__46));
- if (__gen_e_acsl_lt_8 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__46);
+ __e_acsl_mpz_t __gen_e_acsl__42;
+ int __gen_e_acsl_lt_7;
+ __gmpz_init_set_si(__gen_e_acsl__42,10L);
+ __gen_e_acsl_lt_7 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__42));
+ if (__gen_e_acsl_lt_7 < 0) ; else break;
+ __gmpz_clear(__gen_e_acsl__42);
}
{
long __gen_e_acsl_i_4;
@@ -685,52 +629,52 @@ int main(void)
(void *)0);
if (__gen_e_acsl_valid_2) ;
else {
- __gen_e_acsl_forall_8 = 0;
- goto e_acsl_end_loop10;
+ __gen_e_acsl_forall_7 = 0;
+ goto e_acsl_end_loop9;
}
}
{
- __e_acsl_mpz_t __gen_e_acsl__47;
- __e_acsl_mpz_t __gen_e_acsl_add_16;
- __gmpz_init_set_str(__gen_e_acsl__47,"1",10);
- __gmpz_init(__gen_e_acsl_add_16);
- __gmpz_add(__gen_e_acsl_add_16,
+ __e_acsl_mpz_t __gen_e_acsl__43;
+ __e_acsl_mpz_t __gen_e_acsl_add_14;
+ __gmpz_init_set_str(__gen_e_acsl__43,"1",10);
+ __gmpz_init(__gen_e_acsl_add_14);
+ __gmpz_add(__gen_e_acsl_add_14,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__47));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__43));
__gmpz_set(__gen_e_acsl_i_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_16));
- __gmpz_clear(__gen_e_acsl__47);
- __gmpz_clear(__gen_e_acsl_add_16);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_14));
+ __gmpz_clear(__gen_e_acsl__43);
+ __gmpz_clear(__gen_e_acsl_add_14);
}
}
- e_acsl_end_loop10: ;
- __e_acsl_assert(__gen_e_acsl_forall_8,(char *)"Assertion",
+ e_acsl_end_loop9: ;
+ __e_acsl_assert(__gen_e_acsl_forall_7,(char *)"Assertion",
(char *)"main",
(char *)"\\forall char i; 0 <= i < 10 ==> \\valid(&buf[i])",
- 32);
+ 31);
__gmpz_clear(__gen_e_acsl_i_3);
}
/*@ assert ∀ ℤ i; 0 ≤ i < len ⇒ \valid(&buf[i]); */
{
- int __gen_e_acsl_forall_9;
+ int __gen_e_acsl_forall_8;
__e_acsl_mpz_t __gen_e_acsl_i_5;
- __gen_e_acsl_forall_9 = 1;
+ __gen_e_acsl_forall_8 = 1;
__gmpz_init(__gen_e_acsl_i_5);
{
- __e_acsl_mpz_t __gen_e_acsl__48;
- __gmpz_init_set_si(__gen_e_acsl__48,0L);
+ __e_acsl_mpz_t __gen_e_acsl__44;
+ __gmpz_init_set_si(__gen_e_acsl__44,0L);
__gmpz_set(__gen_e_acsl_i_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__48));
- __gmpz_clear(__gen_e_acsl__48);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__44));
+ __gmpz_clear(__gen_e_acsl__44);
}
while (1) {
{
__e_acsl_mpz_t __gen_e_acsl_len;
- int __gen_e_acsl_lt_9;
+ int __gen_e_acsl_lt_8;
__gmpz_init_set_ui(__gen_e_acsl_len,len);
- __gen_e_acsl_lt_9 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_5),
+ __gen_e_acsl_lt_8 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_5),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_len));
- if (__gen_e_acsl_lt_9 < 0) ; else break;
+ if (__gen_e_acsl_lt_8 < 0) ; else break;
__gmpz_clear(__gen_e_acsl_len);
}
{
@@ -743,43 +687,43 @@ int main(void)
(void *)0);
if (__gen_e_acsl_valid_3) ;
else {
- __gen_e_acsl_forall_9 = 0;
- goto e_acsl_end_loop11;
+ __gen_e_acsl_forall_8 = 0;
+ goto e_acsl_end_loop10;
}
}
{
- __e_acsl_mpz_t __gen_e_acsl__49;
- __e_acsl_mpz_t __gen_e_acsl_add_17;
- __gmpz_init_set_str(__gen_e_acsl__49,"1",10);
- __gmpz_init(__gen_e_acsl_add_17);
- __gmpz_add(__gen_e_acsl_add_17,
+ __e_acsl_mpz_t __gen_e_acsl__45;
+ __e_acsl_mpz_t __gen_e_acsl_add_15;
+ __gmpz_init_set_str(__gen_e_acsl__45,"1",10);
+ __gmpz_init(__gen_e_acsl_add_15);
+ __gmpz_add(__gen_e_acsl_add_15,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_i_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__49));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__45));
__gmpz_set(__gen_e_acsl_i_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_17));
- __gmpz_clear(__gen_e_acsl__49);
- __gmpz_clear(__gen_e_acsl_add_17);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_15));
+ __gmpz_clear(__gen_e_acsl__45);
+ __gmpz_clear(__gen_e_acsl_add_15);
}
}
- e_acsl_end_loop11: ;
- __e_acsl_assert(__gen_e_acsl_forall_9,(char *)"Assertion",
+ e_acsl_end_loop10: ;
+ __e_acsl_assert(__gen_e_acsl_forall_8,(char *)"Assertion",
(char *)"main",
(char *)"\\forall integer i; 0 <= i < len ==> \\valid(&buf[i])",
- 33);
+ 32);
__gmpz_clear(__gen_e_acsl_i_5);
}
/*@ assert ∀ ℤ i; 0 ≤ i ≤ len ⇒ \valid(&buf[i]); */
{
- int __gen_e_acsl_forall_10;
+ int __gen_e_acsl_forall_9;
__e_acsl_mpz_t __gen_e_acsl_i_7;
- __gen_e_acsl_forall_10 = 1;
+ __gen_e_acsl_forall_9 = 1;
__gmpz_init(__gen_e_acsl_i_7);
{
- __e_acsl_mpz_t __gen_e_acsl__50;
- __gmpz_init_set_si(__gen_e_acsl__50,0L);
+ __e_acsl_mpz_t __gen_e_acsl__46;
+ __gmpz_init_set_si(__gen_e_acsl__46,0L);
__gmpz_set(__gen_e_acsl_i_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__50));
- __gmpz_clear(__gen_e_acsl__50);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__46));
+ __gmpz_clear(__gen_e_acsl__46);
}
while (1) {
{
@@ -801,33 +745,49 @@ int main(void)
(void *)0);
if (__gen_e_acsl_valid_4) ;
else {
- __gen_e_acsl_forall_10 = 0;
- goto e_acsl_end_loop12;
+ __gen_e_acsl_forall_9 = 0;
+ goto e_acsl_end_loop11;
}
}
{
- __e_acsl_mpz_t __gen_e_acsl__51;
- __e_acsl_mpz_t __gen_e_acsl_add_18;
- __gmpz_init_set_str(__gen_e_acsl__51,"1",10);
- __gmpz_init(__gen_e_acsl_add_18);
- __gmpz_add(__gen_e_acsl_add_18,
+ __e_acsl_mpz_t __gen_e_acsl__47;
+ __e_acsl_mpz_t __gen_e_acsl_add_16;
+ __gmpz_init_set_str(__gen_e_acsl__47,"1",10);
+ __gmpz_init(__gen_e_acsl_add_16);
+ __gmpz_add(__gen_e_acsl_add_16,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_i_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__51));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__47));
__gmpz_set(__gen_e_acsl_i_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_18));
- __gmpz_clear(__gen_e_acsl__51);
- __gmpz_clear(__gen_e_acsl_add_18);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_16));
+ __gmpz_clear(__gen_e_acsl__47);
+ __gmpz_clear(__gen_e_acsl_add_16);
}
}
- e_acsl_end_loop12: ;
- __e_acsl_assert(__gen_e_acsl_forall_10,(char *)"Assertion",
+ e_acsl_end_loop11: ;
+ __e_acsl_assert(__gen_e_acsl_forall_9,(char *)"Assertion",
(char *)"main",
(char *)"\\forall integer i; 0 <= i <= len ==> \\valid(&buf[i])",
- 34);
+ 33);
__gmpz_clear(__gen_e_acsl_i_7);
__e_acsl_delete_block((void *)(buf));
}
}
+ /*@ assert ∀ ℤ x; 0 < x < 1 ⇒ \false; */
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
+ (char *)"\\forall integer x; 0 < x < 1 ==> \\false",37);
+ /*@ assert ¬(∃ char c; 10 ≤ c < 10 ∧ c ≡ 10); */
+ __e_acsl_assert(! 0,(char *)"Assertion",(char *)"main",
+ (char *)"!(\\exists char c; 10 <= c < 10 && c == 10)",38);
+ /*@ assert \let u = 5;
+ ∀ ℤ x, ℤ y; 0 ≤ x < 2 ∧ 4 < y < u ⇒ \false;
+ */
+ {
+ int __gen_e_acsl_u;
+ __gen_e_acsl_u = 5;
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
+ (char *)"\\let u = 5;\n\\forall integer x, integer y; 0 <= x < 2 && 4 < y < u ==> \\false",
+ 40);
+ }
__retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
index 25fae0b8e5c..cb1d4c89b81 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
@@ -16,33 +16,32 @@
[eva:alarm] tests/gmp/quantif.i:10: Warning: assertion got status unknown.
[eva] tests/gmp/quantif.i:10: starting to merge loop iterations
[eva:alarm] tests/gmp/quantif.i:11: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:12: Warning: assertion got status unknown.
-[eva] tests/gmp/quantif.i:12: starting to merge loop iterations
-[eva:alarm] tests/gmp/quantif.i:16: Warning: assertion got status unknown.
-[eva] tests/gmp/quantif.i:16: starting to merge loop iterations
-[eva:alarm] tests/gmp/quantif.i:16: Warning:
+[eva] tests/gmp/quantif.i:11: starting to merge loop iterations
+[eva:alarm] tests/gmp/quantif.i:15: Warning: assertion got status unknown.
+[eva] tests/gmp/quantif.i:15: starting to merge loop iterations
+[eva:alarm] tests/gmp/quantif.i:15: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:21: Warning: assertion got status unknown.
-[eva] tests/gmp/quantif.i:21: starting to merge loop iterations
-[eva:alarm] tests/gmp/quantif.i:25: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:20: Warning: assertion got status unknown.
+[eva] tests/gmp/quantif.i:20: starting to merge loop iterations
+[eva:alarm] tests/gmp/quantif.i:24: Warning: assertion got status unknown.
+[eva] tests/gmp/quantif.i:24: starting to merge loop iterations
[eva] tests/gmp/quantif.i:25: starting to merge loop iterations
-[eva] tests/gmp/quantif.i:26: starting to merge loop iterations
-[eva:alarm] tests/gmp/quantif.i:25: Warning:
+[eva:alarm] tests/gmp/quantif.i:24: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __e_acsl_store_block
-[eva:alarm] tests/gmp/quantif.i:31: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:30: Warning: assertion got status unknown.
[eva] using specification for function __e_acsl_valid
+[eva] tests/gmp/quantif.i:30: starting to merge loop iterations
+[eva:alarm] tests/gmp/quantif.i:30: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva] tests/gmp/quantif.i:31: starting to merge loop iterations
[eva:alarm] tests/gmp/quantif.i:31: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/quantif.i:32: Warning: assertion got status unknown.
[eva] tests/gmp/quantif.i:32: starting to merge loop iterations
[eva:alarm] tests/gmp/quantif.i:32: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:33: Warning: assertion got status unknown.
-[eva] tests/gmp/quantif.i:33: starting to merge loop iterations
-[eva:alarm] tests/gmp/quantif.i:33: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:34: Warning: assertion got status unknown.
[eva] using specification for function __gmpz_init
[eva] using specification for function __gmpz_init_set_si
[eva] using specification for function __gmpz_set
@@ -51,8 +50,10 @@
[eva] using specification for function __gmpz_cmp
[eva] using specification for function __gmpz_get_si
[eva] using specification for function __gmpz_add
-[eva:alarm] tests/gmp/quantif.i:34: Warning:
+[eva:alarm] tests/gmp/quantif.i:33: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __e_acsl_delete_block
+[eva:alarm] tests/gmp/quantif.i:37: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:40: Warning: assertion got status unknown.
[eva] using specification for function __e_acsl_memory_clean
[eva] done for function main
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 dfd80721227..7a6b1edc0f8 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
@@ -27,40 +27,39 @@
[eva:alarm] tests/gmp/quantif.i:11: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/quantif.i:11: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:12: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:12: Warning:
+[eva:alarm] tests/gmp/quantif.i:15: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:15: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:16: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:16: Warning:
+[eva:alarm] tests/gmp/quantif.i:20: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:20: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:21: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:21: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:25: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:26: Warning:
+[eva:alarm] tests/gmp/quantif.i:24: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:25: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpz_tdiv_r
-[eva:alarm] tests/gmp/quantif.i:26: Warning:
+[eva:alarm] tests/gmp/quantif.i:25: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpz_tdiv_q
[eva] using specification for function __gmpz_mul
-[eva:alarm] tests/gmp/quantif.i:25: Warning:
+[eva:alarm] tests/gmp/quantif.i:24: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __e_acsl_store_block
-[eva:alarm] tests/gmp/quantif.i:31: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:30: Warning: assertion got status unknown.
[eva] using specification for function __gmpz_get_si
[eva] using specification for function __e_acsl_valid
+[eva:alarm] tests/gmp/quantif.i:30: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:31: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/quantif.i:32: Warning: assertion got status unknown.
+[eva] using specification for function __gmpz_init_set_ui
[eva:alarm] tests/gmp/quantif.i:32: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:33: Warning: assertion got status unknown.
-[eva] using specification for function __gmpz_init_set_ui
[eva:alarm] tests/gmp/quantif.i:33: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:34: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:34: Warning:
- function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __e_acsl_delete_block
+[eva:alarm] tests/gmp/quantif.i:37: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:40: Warning: assertion got status unknown.
[eva] using specification for function __e_acsl_memory_clean
[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/quantif.i b/src/plugins/e-acsl/tests/gmp/quantif.i
index 3a32e9a36b0..e7b792fd139 100644
--- a/src/plugins/e-acsl/tests/gmp/quantif.i
+++ b/src/plugins/e-acsl/tests/gmp/quantif.i
@@ -8,7 +8,6 @@ int main(void) {
/*@ assert \forall integer x; 0 <= x <= 1 ==> x == 0 || x == 1; */
/*@ assert \forall integer x; 0 < x <= 1 ==> x == 1; */
- /*@ assert \forall integer x; 0 < x < 1 ==> \false; */
/*@ assert \forall integer x; 0 <= x < 1 ==> x == 0; */
/* // multiple universal quantifications */
@@ -34,5 +33,12 @@ int main(void) {
/*@ assert \forall integer i; 0 <= i <= len ==> \valid(buf+i); */
}
+ // Empty quantifications
+ /*@ assert \forall integer x; 0 < x < 1 ==> \false; */
+ /*@ assert ! \exists char c; 10 <= c < 10 && c == 10; */ ;
+ /*@ assert
+ \let u = 5;
+ \forall integer x,y; 0 <= x < 2 && 4 < y < u ==> \false; */ ;
+
return 0;
}
--
GitLab