From 21c18cf27d00c274bf7ebb28fcbd7e627430d685 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 13 May 2011 14:22:34 +0000
Subject: [PATCH] first step for support of statement/function contracts
(statement ensures could work but yet untested)
---
.../tests/e-acsl-runtime/oracle/gen_lazy.c | 310 ++++++------
.../e-acsl-runtime/oracle/lazy.res.oracle | 460 +++++++++---------
src/plugins/e-acsl/visit.ml | 147 ++++--
3 files changed, 503 insertions(+), 414 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
index bf375629f92..aea4759f166 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
@@ -590,16 +590,16 @@ int main(void)
e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
(__mpz_struct const *)(e_acsl_2));
if (e_acsl_3 == 0) {
- mpz_t e_acsl_11;
- mpz_t e_acsl_12;
- int e_acsl_13;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)y);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_12),(long)1);
- e_acsl_13 = __gmpz_cmp((__mpz_struct const *)(e_acsl_11),
- (__mpz_struct const *)(e_acsl_12));
- e_acsl_7 = e_acsl_13 == 0;
- __gmpz_clear((__mpz_struct *)(e_acsl_11));
- __gmpz_clear((__mpz_struct *)(e_acsl_12));
+ mpz_t e_acsl_8;
+ mpz_t e_acsl_9;
+ int e_acsl_10;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)y);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_9),(long)1);
+ e_acsl_10 = __gmpz_cmp((__mpz_struct const *)(e_acsl_8),
+ (__mpz_struct const *)(e_acsl_9));
+ e_acsl_7 = e_acsl_10 == 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_8));
+ __gmpz_clear((__mpz_struct *)(e_acsl_9));
} else { e_acsl_7 = 0; }
if (! e_acsl_7) { e_acsl_fail((char *)"(x == 0 && y == 1)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_1));
@@ -607,178 +607,178 @@ int main(void)
}
/*@ assert ¬(x ≢ 0 ∧ y ≡ 1/0); */ ;
- { mpz_t e_acsl_14; mpz_t e_acsl_15; int e_acsl_16; int e_acsl_25;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_14),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_15),(long)0);
- e_acsl_16 = __gmpz_cmp((__mpz_struct const *)(e_acsl_14),
- (__mpz_struct const *)(e_acsl_15));
- if (e_acsl_16 != 0) {
+ { mpz_t e_acsl_19; mpz_t e_acsl_20; int e_acsl_21; int e_acsl_22;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_19),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)0);
+ e_acsl_21 = __gmpz_cmp((__mpz_struct const *)(e_acsl_19),
+ (__mpz_struct const *)(e_acsl_20));
+ if (e_acsl_21 != 0) {
+ mpz_t e_acsl_23;
+ mpz_t e_acsl_24;
+ mpz_t e_acsl_25;
+ mpz_t e_acsl_26;
+ mpz_t e_acsl_27;
+ int e_acsl_28;
mpz_t e_acsl_29;
- mpz_t e_acsl_30;
- mpz_t e_acsl_31;
- mpz_t e_acsl_32;
- mpz_t e_acsl_33;
- int e_acsl_34;
- mpz_t e_acsl_35;
- int e_acsl_36;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_29),(long)y);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_30),(long)1);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_31),(long)0);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_32),(long)0);
- __gmpz_init_set_ui((__mpz_struct *)(e_acsl_33),(unsigned long)0U);
- e_acsl_34 = __gmpz_cmp((__mpz_struct const *)(e_acsl_32),
- (__mpz_struct const *)(e_acsl_33));
- __gmpz_init((__mpz_struct *)(e_acsl_35));
+ int e_acsl_30;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_23),(long)y);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_24),(long)1);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_25),(long)0);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_26),(long)0);
+ __gmpz_init_set_ui((__mpz_struct *)(e_acsl_27),(unsigned long)0U);
+ e_acsl_28 = __gmpz_cmp((__mpz_struct const *)(e_acsl_26),
+ (__mpz_struct const *)(e_acsl_27));
+ __gmpz_init((__mpz_struct *)(e_acsl_29));
/*@ assert 0 ≢ 0U; */ ;
- if (e_acsl_34 == 0) { e_acsl_fail((char *)"(0 == 0U)"); }
- __gmpz_cdiv_q((__mpz_struct *)(e_acsl_35),
- (__mpz_struct const *)(e_acsl_30),
- (__mpz_struct const *)(e_acsl_31));
- e_acsl_36 = __gmpz_cmp((__mpz_struct const *)(e_acsl_29),
- (__mpz_struct const *)(e_acsl_35));
- e_acsl_25 = e_acsl_36 == 0;
+ if (e_acsl_28 == 0) { e_acsl_fail((char *)"(0 == 0U)"); }
+ __gmpz_cdiv_q((__mpz_struct *)(e_acsl_29),
+ (__mpz_struct const *)(e_acsl_24),
+ (__mpz_struct const *)(e_acsl_25));
+ e_acsl_30 = __gmpz_cmp((__mpz_struct const *)(e_acsl_23),
+ (__mpz_struct const *)(e_acsl_29));
+ e_acsl_22 = e_acsl_30 == 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_23));
+ __gmpz_clear((__mpz_struct *)(e_acsl_24));
+ __gmpz_clear((__mpz_struct *)(e_acsl_25));
+ __gmpz_clear((__mpz_struct *)(e_acsl_26));
+ __gmpz_clear((__mpz_struct *)(e_acsl_27));
__gmpz_clear((__mpz_struct *)(e_acsl_29));
- __gmpz_clear((__mpz_struct *)(e_acsl_30));
- __gmpz_clear((__mpz_struct *)(e_acsl_31));
- __gmpz_clear((__mpz_struct *)(e_acsl_32));
- __gmpz_clear((__mpz_struct *)(e_acsl_33));
- __gmpz_clear((__mpz_struct *)(e_acsl_35));
- } else { e_acsl_25 = 0; }
- if (! (! e_acsl_25)) { e_acsl_fail((char *)"(!(x != 0 && y == 1/0))"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_14));
- __gmpz_clear((__mpz_struct *)(e_acsl_15));
+ } else { e_acsl_22 = 0; }
+ if (! (! e_acsl_22)) { e_acsl_fail((char *)"(!(x != 0 && y == 1/0))"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_19));
+ __gmpz_clear((__mpz_struct *)(e_acsl_20));
}
/*@ assert x ≡ 1 ∨ y ≡ 1; */ ;
- { mpz_t e_acsl_37; mpz_t e_acsl_38; int e_acsl_39; int e_acsl_43;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_37),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_38),(long)1);
- e_acsl_39 = __gmpz_cmp((__mpz_struct const *)(e_acsl_37),
- (__mpz_struct const *)(e_acsl_38));
- if (e_acsl_39 == 0) { e_acsl_43 = 1; }
+ { mpz_t e_acsl_34; mpz_t e_acsl_35; int e_acsl_36; int e_acsl_37;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_34),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_35),(long)1);
+ e_acsl_36 = __gmpz_cmp((__mpz_struct const *)(e_acsl_34),
+ (__mpz_struct const *)(e_acsl_35));
+ if (e_acsl_36 == 0) { e_acsl_37 = 1; }
else {
- mpz_t e_acsl_47;
- mpz_t e_acsl_48;
- int e_acsl_49;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_47),(long)y);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_48),(long)1);
- e_acsl_49 = __gmpz_cmp((__mpz_struct const *)(e_acsl_47),
- (__mpz_struct const *)(e_acsl_48));
- e_acsl_43 = e_acsl_49 == 0;
- __gmpz_clear((__mpz_struct *)(e_acsl_47));
- __gmpz_clear((__mpz_struct *)(e_acsl_48));
- } if (! e_acsl_43) { e_acsl_fail((char *)"(x == 1 || y == 1)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_37));
- __gmpz_clear((__mpz_struct *)(e_acsl_38));
+ mpz_t e_acsl_38;
+ mpz_t e_acsl_39;
+ int e_acsl_40;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_38),(long)y);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_39),(long)1);
+ e_acsl_40 = __gmpz_cmp((__mpz_struct const *)(e_acsl_38),
+ (__mpz_struct const *)(e_acsl_39));
+ e_acsl_37 = e_acsl_40 == 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_38));
+ __gmpz_clear((__mpz_struct *)(e_acsl_39));
+ } if (! e_acsl_37) { e_acsl_fail((char *)"(x == 1 || y == 1)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_34));
+ __gmpz_clear((__mpz_struct *)(e_acsl_35));
}
/*@ assert x ≡ 0 ∨ y ≡ 1/0; */ ;
- { mpz_t e_acsl_50; mpz_t e_acsl_51; int e_acsl_52; int e_acsl_61;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_50),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_51),(long)0);
- e_acsl_52 = __gmpz_cmp((__mpz_struct const *)(e_acsl_50),
- (__mpz_struct const *)(e_acsl_51));
- if (e_acsl_52 == 0) { e_acsl_61 = 1; }
+ { mpz_t e_acsl_49; mpz_t e_acsl_50; int e_acsl_51; int e_acsl_52;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_49),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_50),(long)0);
+ e_acsl_51 = __gmpz_cmp((__mpz_struct const *)(e_acsl_49),
+ (__mpz_struct const *)(e_acsl_50));
+ if (e_acsl_51 == 0) { e_acsl_52 = 1; }
+ else {
+ mpz_t e_acsl_53;
+ mpz_t e_acsl_54;
+ mpz_t e_acsl_55;
+ mpz_t e_acsl_56;
+ mpz_t e_acsl_57;
+ int e_acsl_58;
+ mpz_t e_acsl_59;
+ int e_acsl_60;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_53),(long)y);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_54),(long)1);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_55),(long)0);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_56),(long)0);
+ __gmpz_init_set_ui((__mpz_struct *)(e_acsl_57),(unsigned long)0U);
+ e_acsl_58 = __gmpz_cmp((__mpz_struct const *)(e_acsl_56),
+ (__mpz_struct const *)(e_acsl_57));
+ __gmpz_init((__mpz_struct *)(e_acsl_59));
+ /*@ assert 0 ≢ 0U; */ ;
+ if (e_acsl_58 == 0) { e_acsl_fail((char *)"(0 == 0U)"); }
+ __gmpz_cdiv_q((__mpz_struct *)(e_acsl_59),
+ (__mpz_struct const *)(e_acsl_54),
+ (__mpz_struct const *)(e_acsl_55));
+ e_acsl_60 = __gmpz_cmp((__mpz_struct const *)(e_acsl_53),
+ (__mpz_struct const *)(e_acsl_59));
+ e_acsl_52 = e_acsl_60 == 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_53));
+ __gmpz_clear((__mpz_struct *)(e_acsl_54));
+ __gmpz_clear((__mpz_struct *)(e_acsl_55));
+ __gmpz_clear((__mpz_struct *)(e_acsl_56));
+ __gmpz_clear((__mpz_struct *)(e_acsl_57));
+ __gmpz_clear((__mpz_struct *)(e_acsl_59));
+ } if (! e_acsl_52) { e_acsl_fail((char *)"(x == 0 || y == 1/0)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_49));
+ __gmpz_clear((__mpz_struct *)(e_acsl_50));
+ }
+
+ /*@ assert x ≡ 0 ⇒ y ≡ 1; */ ;
+ { mpz_t e_acsl_64; mpz_t e_acsl_65; int e_acsl_66; int e_acsl_67;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_64),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_65),(long)0);
+ e_acsl_66 = __gmpz_cmp((__mpz_struct const *)(e_acsl_64),
+ (__mpz_struct const *)(e_acsl_65));
+ if (! (e_acsl_66 == 0)) { e_acsl_67 = 1; }
else {
- mpz_t e_acsl_65;
- mpz_t e_acsl_66;
- mpz_t e_acsl_67;
mpz_t e_acsl_68;
mpz_t e_acsl_69;
int e_acsl_70;
- mpz_t e_acsl_71;
- int e_acsl_72;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_65),(long)y);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_66),(long)1);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_67),(long)0);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_68),(long)0);
- __gmpz_init_set_ui((__mpz_struct *)(e_acsl_69),(unsigned long)0U);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_68),(long)y);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_69),(long)1);
e_acsl_70 = __gmpz_cmp((__mpz_struct const *)(e_acsl_68),
(__mpz_struct const *)(e_acsl_69));
- __gmpz_init((__mpz_struct *)(e_acsl_71));
- /*@ assert 0 ≢ 0U; */ ;
- if (e_acsl_70 == 0) { e_acsl_fail((char *)"(0 == 0U)"); }
- __gmpz_cdiv_q((__mpz_struct *)(e_acsl_71),
- (__mpz_struct const *)(e_acsl_66),
- (__mpz_struct const *)(e_acsl_67));
- e_acsl_72 = __gmpz_cmp((__mpz_struct const *)(e_acsl_65),
- (__mpz_struct const *)(e_acsl_71));
- e_acsl_61 = e_acsl_72 == 0;
- __gmpz_clear((__mpz_struct *)(e_acsl_65));
- __gmpz_clear((__mpz_struct *)(e_acsl_66));
- __gmpz_clear((__mpz_struct *)(e_acsl_67));
+ e_acsl_67 = e_acsl_70 == 0;
__gmpz_clear((__mpz_struct *)(e_acsl_68));
__gmpz_clear((__mpz_struct *)(e_acsl_69));
- __gmpz_clear((__mpz_struct *)(e_acsl_71));
- } if (! e_acsl_61) { e_acsl_fail((char *)"(x == 0 || y == 1/0)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_50));
- __gmpz_clear((__mpz_struct *)(e_acsl_51));
+ } if (! e_acsl_67) { e_acsl_fail((char *)"(x == 0 ==> y == 1)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_64));
+ __gmpz_clear((__mpz_struct *)(e_acsl_65));
}
- /*@ assert x ≡ 0 ⇒ y ≡ 1; */ ;
- { mpz_t e_acsl_73; mpz_t e_acsl_74; int e_acsl_75; int e_acsl_79;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_73),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_74),(long)0);
- e_acsl_75 = __gmpz_cmp((__mpz_struct const *)(e_acsl_73),
- (__mpz_struct const *)(e_acsl_74));
- if (! (e_acsl_75 == 0)) { e_acsl_79 = 1; }
+ /*@ assert x ≡ 1 ⇒ y ≡ 1/0; */ ;
+ { mpz_t e_acsl_79; mpz_t e_acsl_80; int e_acsl_81; int e_acsl_82;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_79),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_80),(long)1);
+ e_acsl_81 = __gmpz_cmp((__mpz_struct const *)(e_acsl_79),
+ (__mpz_struct const *)(e_acsl_80));
+ if (! (e_acsl_81 == 0)) { e_acsl_82 = 1; }
else {
mpz_t e_acsl_83;
mpz_t e_acsl_84;
- int e_acsl_85;
+ mpz_t e_acsl_85;
+ mpz_t e_acsl_86;
+ mpz_t e_acsl_87;
+ int e_acsl_88;
+ mpz_t e_acsl_89;
+ int e_acsl_90;
__gmpz_init_set_si((__mpz_struct *)(e_acsl_83),(long)y);
__gmpz_init_set_si((__mpz_struct *)(e_acsl_84),(long)1);
- e_acsl_85 = __gmpz_cmp((__mpz_struct const *)(e_acsl_83),
- (__mpz_struct const *)(e_acsl_84));
- e_acsl_79 = e_acsl_85 == 0;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_85),(long)0);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_86),(long)0);
+ __gmpz_init_set_ui((__mpz_struct *)(e_acsl_87),(unsigned long)0U);
+ e_acsl_88 = __gmpz_cmp((__mpz_struct const *)(e_acsl_86),
+ (__mpz_struct const *)(e_acsl_87));
+ __gmpz_init((__mpz_struct *)(e_acsl_89));
+ /*@ assert 0 ≢ 0U; */ ;
+ if (e_acsl_88 == 0) { e_acsl_fail((char *)"(0 == 0U)"); }
+ __gmpz_cdiv_q((__mpz_struct *)(e_acsl_89),
+ (__mpz_struct const *)(e_acsl_84),
+ (__mpz_struct const *)(e_acsl_85));
+ e_acsl_90 = __gmpz_cmp((__mpz_struct const *)(e_acsl_83),
+ (__mpz_struct const *)(e_acsl_89));
+ e_acsl_82 = e_acsl_90 == 0;
__gmpz_clear((__mpz_struct *)(e_acsl_83));
__gmpz_clear((__mpz_struct *)(e_acsl_84));
- } if (! e_acsl_79) { e_acsl_fail((char *)"(x == 0 ==> y == 1)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_73));
- __gmpz_clear((__mpz_struct *)(e_acsl_74));
- }
-
- /*@ assert x ≡ 1 ⇒ y ≡ 1/0; */ ;
- { mpz_t e_acsl_86; mpz_t e_acsl_87; int e_acsl_88; int e_acsl_97;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_86),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_87),(long)1);
- e_acsl_88 = __gmpz_cmp((__mpz_struct const *)(e_acsl_86),
- (__mpz_struct const *)(e_acsl_87));
- if (! (e_acsl_88 == 0)) { e_acsl_97 = 1; }
- else {
- mpz_t e_acsl_101;
- mpz_t e_acsl_102;
- mpz_t e_acsl_103;
- mpz_t e_acsl_104;
- mpz_t e_acsl_105;
- int e_acsl_106;
- mpz_t e_acsl_107;
- int e_acsl_108;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_101),(long)y);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_102),(long)1);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_103),(long)0);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_104),(long)0);
- __gmpz_init_set_ui((__mpz_struct *)(e_acsl_105),(unsigned long)0U);
- e_acsl_106 = __gmpz_cmp((__mpz_struct const *)(e_acsl_104),
- (__mpz_struct const *)(e_acsl_105));
- __gmpz_init((__mpz_struct *)(e_acsl_107));
- /*@ assert 0 ≢ 0U; */ ;
- if (e_acsl_106 == 0) { e_acsl_fail((char *)"(0 == 0U)"); }
- __gmpz_cdiv_q((__mpz_struct *)(e_acsl_107),
- (__mpz_struct const *)(e_acsl_102),
- (__mpz_struct const *)(e_acsl_103));
- e_acsl_108 = __gmpz_cmp((__mpz_struct const *)(e_acsl_101),
- (__mpz_struct const *)(e_acsl_107));
- e_acsl_97 = e_acsl_108 == 0;
- __gmpz_clear((__mpz_struct *)(e_acsl_101));
- __gmpz_clear((__mpz_struct *)(e_acsl_102));
- __gmpz_clear((__mpz_struct *)(e_acsl_103));
- __gmpz_clear((__mpz_struct *)(e_acsl_104));
- __gmpz_clear((__mpz_struct *)(e_acsl_105));
- __gmpz_clear((__mpz_struct *)(e_acsl_107));
- } if (! e_acsl_97) { e_acsl_fail((char *)"(x == 1 ==> y == 1/0)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_86));
- __gmpz_clear((__mpz_struct *)(e_acsl_87));
+ __gmpz_clear((__mpz_struct *)(e_acsl_85));
+ __gmpz_clear((__mpz_struct *)(e_acsl_86));
+ __gmpz_clear((__mpz_struct *)(e_acsl_87));
+ __gmpz_clear((__mpz_struct *)(e_acsl_89));
+ } if (! e_acsl_82) { e_acsl_fail((char *)"(x == 1 ==> y == 1/0)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_79));
+ __gmpz_clear((__mpz_struct *)(e_acsl_80));
}
__retres = 0;
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 4e53b06c5e0..f94afe6073f 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
@@ -16,24 +16,24 @@ 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 mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:135.
+ Called from PROJECT_FILE.i:132.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:136.
+ Called from PROJECT_FILE.i:133.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:137.
+ Called from PROJECT_FILE.i:134.
[value] Done for function mpz_cmp
-PROJECT_FILE.i:138:[value] assigning non deterministic value for the first time
+PROJECT_FILE.i:135:[value] assigning non deterministic value for the first time
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:139.
+ Called from PROJECT_FILE.i:136.
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.
+ Called from PROJECT_FILE.i:137.
[value] Done for function mpz_clear
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:142.
+ Called from PROJECT_FILE.i:139.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -44,78 +44,78 @@ PROJECT_FILE.i:105:[value] Function exit: postcondition got status invalid
[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:143.
+ Called from PROJECT_FILE.i:140.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:143.
+ Called from PROJECT_FILE.i:140.
[value] Done for function mpz_clear
-PROJECT_FILE.i:146:[value] Assertion got status valid.
+PROJECT_FILE.i:143:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:150.
+ Called from PROJECT_FILE.i:147.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:150.
+ Called from PROJECT_FILE.i:147.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:151.
+ Called from PROJECT_FILE.i:148.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:164.
+ Called from PROJECT_FILE.i:158.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:165.
+ Called from PROJECT_FILE.i:159.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:166.
+ Called from PROJECT_FILE.i:160.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:167.
+ Called from PROJECT_FILE.i:161.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_ui <- main.
- Called from PROJECT_FILE.i:168.
+ Called from PROJECT_FILE.i:162.
PROJECT_FILE.i:25:[value] Function mpz_init_set_ui: postcondition got status unknown
[value] Done for function mpz_init_set_ui
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:169.
+ Called from PROJECT_FILE.i:163.
[value] Done for function mpz_cmp
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:170.
+ Called from PROJECT_FILE.i:164.
PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
-PROJECT_FILE.i:171:[value] Assertion got status invalid (stopping propagation)..
+PROJECT_FILE.i:165:[value] Assertion got status invalid (stopping propagation)..
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:184.
+ Called from PROJECT_FILE.i:178.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:184.
+ Called from PROJECT_FILE.i:178.
[value] Done for function mpz_clear
-PROJECT_FILE.i:187:[value] Assertion got status valid.
+PROJECT_FILE.i:181:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:189.
+ Called from PROJECT_FILE.i:183.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:190.
+ Called from PROJECT_FILE.i:184.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:190.
+ Called from PROJECT_FILE.i:184.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:199.
+ Called from PROJECT_FILE.i:190.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:200.
+ Called from PROJECT_FILE.i:191.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:201.
+ Called from PROJECT_FILE.i:192.
[value] Done for function mpz_cmp
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:203.
+ Called from PROJECT_FILE.i:194.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:204.
+ Called from PROJECT_FILE.i:195.
[value] Done for function mpz_clear
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:205.
+ Called from PROJECT_FILE.i:196.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -125,76 +125,76 @@ PROJECT_FILE.i:187:[value] Assertion got status valid.
[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:206.
+ Called from PROJECT_FILE.i:197.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:206.
+ Called from PROJECT_FILE.i:197.
[value] Done for function mpz_clear
-PROJECT_FILE.i:209:[value] Assertion got status valid.
+PROJECT_FILE.i:200:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:213.
+ Called from PROJECT_FILE.i:204.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:213.
+ Called from PROJECT_FILE.i:204.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:214.
+ Called from PROJECT_FILE.i:205.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:228.
+ Called from PROJECT_FILE.i:216.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:229.
+ Called from PROJECT_FILE.i:217.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:230.
+ Called from PROJECT_FILE.i:218.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:231.
+ Called from PROJECT_FILE.i:219.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_ui <- main.
- Called from PROJECT_FILE.i:232.
+ Called from PROJECT_FILE.i:220.
[value] Done for function mpz_init_set_ui
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:233.
+ Called from PROJECT_FILE.i:221.
[value] Done for function mpz_cmp
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:234.
+ Called from PROJECT_FILE.i:222.
[value] Done for function mpz_init
-PROJECT_FILE.i:235:[value] Assertion got status invalid (stopping propagation)..
+PROJECT_FILE.i:223:[value] Assertion got status invalid (stopping propagation)..
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:247.
+ Called from PROJECT_FILE.i:235.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:247.
+ Called from PROJECT_FILE.i:235.
[value] Done for function mpz_clear
-PROJECT_FILE.i:250:[value] Assertion got status valid.
+PROJECT_FILE.i:238:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:252.
+ Called from PROJECT_FILE.i:240.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:253.
+ Called from PROJECT_FILE.i:241.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:253.
+ Called from PROJECT_FILE.i:241.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:262.
+ Called from PROJECT_FILE.i:247.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:263.
+ Called from PROJECT_FILE.i:248.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:264.
+ Called from PROJECT_FILE.i:249.
[value] Done for function mpz_cmp
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:266.
+ Called from PROJECT_FILE.i:251.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:267.
+ Called from PROJECT_FILE.i:252.
[value] Done for function mpz_clear
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:268.
+ Called from PROJECT_FILE.i:253.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -204,48 +204,48 @@ PROJECT_FILE.i:250:[value] Assertion got status valid.
[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:269.
+ Called from PROJECT_FILE.i:254.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:269.
+ Called from PROJECT_FILE.i:254.
[value] Done for function mpz_clear
-PROJECT_FILE.i:272:[value] Assertion got status valid.
+PROJECT_FILE.i:257:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:276.
+ Called from PROJECT_FILE.i:261.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:276.
+ Called from PROJECT_FILE.i:261.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:277.
+ Called from PROJECT_FILE.i:262.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:291.
+ Called from PROJECT_FILE.i:273.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:292.
+ Called from PROJECT_FILE.i:274.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:293.
+ Called from PROJECT_FILE.i:275.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:294.
+ Called from PROJECT_FILE.i:276.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_ui <- main.
- Called from PROJECT_FILE.i:295.
+ Called from PROJECT_FILE.i:277.
[value] Done for function mpz_init_set_ui
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:296.
+ Called from PROJECT_FILE.i:278.
[value] Done for function mpz_cmp
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:297.
+ Called from PROJECT_FILE.i:279.
[value] Done for function mpz_init
-PROJECT_FILE.i:298:[value] Assertion got status invalid (stopping propagation)..
+PROJECT_FILE.i:280:[value] Assertion got status invalid (stopping propagation)..
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:310.
+ Called from PROJECT_FILE.i:292.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:310.
+ Called from PROJECT_FILE.i:292.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
@@ -336,16 +336,16 @@ int main(void)
e_acsl_3 = mpz_cmp((__mpz_struct const *)(e_acsl_1),
(__mpz_struct const *)(e_acsl_2));
if (e_acsl_3 == 0) {
- mpz_t e_acsl_11;
- mpz_t e_acsl_12;
- int e_acsl_13;
- mpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)y);
- mpz_init_set_si((__mpz_struct *)(e_acsl_12),(long)1);
- e_acsl_13 = mpz_cmp((__mpz_struct const *)(e_acsl_11),
- (__mpz_struct const *)(e_acsl_12));
- e_acsl_7 = e_acsl_13 == 0;
- mpz_clear((__mpz_struct *)(e_acsl_11));
- mpz_clear((__mpz_struct *)(e_acsl_12));
+ mpz_t e_acsl_8;
+ mpz_t e_acsl_9;
+ int e_acsl_10;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)y);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_9),(long)1);
+ e_acsl_10 = mpz_cmp((__mpz_struct const *)(e_acsl_8),
+ (__mpz_struct const *)(e_acsl_9));
+ e_acsl_7 = e_acsl_10 == 0;
+ mpz_clear((__mpz_struct *)(e_acsl_8));
+ mpz_clear((__mpz_struct *)(e_acsl_9));
} else { e_acsl_7 = 0; }
if (! e_acsl_7) { e_acsl_fail((char *)"(x == 0 && y == 1)"); }
mpz_clear((__mpz_struct *)(e_acsl_1));
@@ -353,178 +353,178 @@ int main(void)
}
/*@ assert ¬(x ≢ 0 ∧ y ≡ 1/0); */ ;
- { mpz_t e_acsl_14; mpz_t e_acsl_15; int e_acsl_16; int e_acsl_25;
- mpz_init_set_si((__mpz_struct *)(e_acsl_14),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_15),(long)0);
- e_acsl_16 = mpz_cmp((__mpz_struct const *)(e_acsl_14),
- (__mpz_struct const *)(e_acsl_15));
- if (e_acsl_16 != 0) {
+ { mpz_t e_acsl_19; mpz_t e_acsl_20; int e_acsl_21; int e_acsl_22;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_19),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)0);
+ e_acsl_21 = mpz_cmp((__mpz_struct const *)(e_acsl_19),
+ (__mpz_struct const *)(e_acsl_20));
+ if (e_acsl_21 != 0) {
+ mpz_t e_acsl_23;
+ mpz_t e_acsl_24;
+ mpz_t e_acsl_25;
+ mpz_t e_acsl_26;
+ mpz_t e_acsl_27;
+ int e_acsl_28;
mpz_t e_acsl_29;
- mpz_t e_acsl_30;
- mpz_t e_acsl_31;
- mpz_t e_acsl_32;
- mpz_t e_acsl_33;
- int e_acsl_34;
- mpz_t e_acsl_35;
- int e_acsl_36;
- mpz_init_set_si((__mpz_struct *)(e_acsl_29),(long)y);
- mpz_init_set_si((__mpz_struct *)(e_acsl_30),(long)1);
- mpz_init_set_si((__mpz_struct *)(e_acsl_31),(long)0);
- mpz_init_set_si((__mpz_struct *)(e_acsl_32),(long)0);
- mpz_init_set_ui((__mpz_struct *)(e_acsl_33),(unsigned long)0U);
- e_acsl_34 = mpz_cmp((__mpz_struct const *)(e_acsl_32),
- (__mpz_struct const *)(e_acsl_33));
- mpz_init((__mpz_struct *)(e_acsl_35));
+ int e_acsl_30;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_23),(long)y);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_24),(long)1);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_25),(long)0);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_26),(long)0);
+ mpz_init_set_ui((__mpz_struct *)(e_acsl_27),(unsigned long)0U);
+ e_acsl_28 = mpz_cmp((__mpz_struct const *)(e_acsl_26),
+ (__mpz_struct const *)(e_acsl_27));
+ mpz_init((__mpz_struct *)(e_acsl_29));
/*@ assert 0 ≢ 0U; */ ;
- if (e_acsl_34 == 0) { e_acsl_fail((char *)"(0 == 0U)"); }
- mpz_cdiv_q((__mpz_struct *)(e_acsl_35),
- (__mpz_struct const *)(e_acsl_30),
- (__mpz_struct const *)(e_acsl_31));
- e_acsl_36 = mpz_cmp((__mpz_struct const *)(e_acsl_29),
- (__mpz_struct const *)(e_acsl_35));
- e_acsl_25 = e_acsl_36 == 0;
+ if (e_acsl_28 == 0) { e_acsl_fail((char *)"(0 == 0U)"); }
+ mpz_cdiv_q((__mpz_struct *)(e_acsl_29),
+ (__mpz_struct const *)(e_acsl_24),
+ (__mpz_struct const *)(e_acsl_25));
+ e_acsl_30 = mpz_cmp((__mpz_struct const *)(e_acsl_23),
+ (__mpz_struct const *)(e_acsl_29));
+ e_acsl_22 = e_acsl_30 == 0;
+ mpz_clear((__mpz_struct *)(e_acsl_23));
+ mpz_clear((__mpz_struct *)(e_acsl_24));
+ mpz_clear((__mpz_struct *)(e_acsl_25));
+ mpz_clear((__mpz_struct *)(e_acsl_26));
+ mpz_clear((__mpz_struct *)(e_acsl_27));
mpz_clear((__mpz_struct *)(e_acsl_29));
- mpz_clear((__mpz_struct *)(e_acsl_30));
- mpz_clear((__mpz_struct *)(e_acsl_31));
- mpz_clear((__mpz_struct *)(e_acsl_32));
- mpz_clear((__mpz_struct *)(e_acsl_33));
- mpz_clear((__mpz_struct *)(e_acsl_35));
- } else { e_acsl_25 = 0; }
- if (! (! e_acsl_25)) { e_acsl_fail((char *)"(!(x != 0 && y == 1/0))"); }
- mpz_clear((__mpz_struct *)(e_acsl_14));
- mpz_clear((__mpz_struct *)(e_acsl_15));
+ } else { e_acsl_22 = 0; }
+ if (! (! e_acsl_22)) { e_acsl_fail((char *)"(!(x != 0 && y == 1/0))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_19));
+ mpz_clear((__mpz_struct *)(e_acsl_20));
}
/*@ assert x ≡ 1 ∨ y ≡ 1; */ ;
- { mpz_t e_acsl_37; mpz_t e_acsl_38; int e_acsl_39; int e_acsl_43;
- mpz_init_set_si((__mpz_struct *)(e_acsl_37),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_38),(long)1);
- e_acsl_39 = mpz_cmp((__mpz_struct const *)(e_acsl_37),
- (__mpz_struct const *)(e_acsl_38));
- if (e_acsl_39 == 0) { e_acsl_43 = 1; }
+ { mpz_t e_acsl_34; mpz_t e_acsl_35; int e_acsl_36; int e_acsl_37;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_34),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_35),(long)1);
+ e_acsl_36 = mpz_cmp((__mpz_struct const *)(e_acsl_34),
+ (__mpz_struct const *)(e_acsl_35));
+ if (e_acsl_36 == 0) { e_acsl_37 = 1; }
else {
- mpz_t e_acsl_47;
- mpz_t e_acsl_48;
- int e_acsl_49;
- mpz_init_set_si((__mpz_struct *)(e_acsl_47),(long)y);
- mpz_init_set_si((__mpz_struct *)(e_acsl_48),(long)1);
- e_acsl_49 = mpz_cmp((__mpz_struct const *)(e_acsl_47),
- (__mpz_struct const *)(e_acsl_48));
- e_acsl_43 = e_acsl_49 == 0;
- mpz_clear((__mpz_struct *)(e_acsl_47));
- mpz_clear((__mpz_struct *)(e_acsl_48));
- } if (! e_acsl_43) { e_acsl_fail((char *)"(x == 1 || y == 1)"); }
- mpz_clear((__mpz_struct *)(e_acsl_37));
- mpz_clear((__mpz_struct *)(e_acsl_38));
+ mpz_t e_acsl_38;
+ mpz_t e_acsl_39;
+ int e_acsl_40;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_38),(long)y);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_39),(long)1);
+ e_acsl_40 = mpz_cmp((__mpz_struct const *)(e_acsl_38),
+ (__mpz_struct const *)(e_acsl_39));
+ e_acsl_37 = e_acsl_40 == 0;
+ mpz_clear((__mpz_struct *)(e_acsl_38));
+ mpz_clear((__mpz_struct *)(e_acsl_39));
+ } if (! e_acsl_37) { e_acsl_fail((char *)"(x == 1 || y == 1)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_34));
+ mpz_clear((__mpz_struct *)(e_acsl_35));
}
/*@ assert x ≡ 0 ∨ y ≡ 1/0; */ ;
- { mpz_t e_acsl_50; mpz_t e_acsl_51; int e_acsl_52; int e_acsl_61;
- mpz_init_set_si((__mpz_struct *)(e_acsl_50),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_51),(long)0);
- e_acsl_52 = mpz_cmp((__mpz_struct const *)(e_acsl_50),
- (__mpz_struct const *)(e_acsl_51));
- if (e_acsl_52 == 0) { e_acsl_61 = 1; }
+ { mpz_t e_acsl_49; mpz_t e_acsl_50; int e_acsl_51; int e_acsl_52;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_49),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_50),(long)0);
+ e_acsl_51 = mpz_cmp((__mpz_struct const *)(e_acsl_49),
+ (__mpz_struct const *)(e_acsl_50));
+ if (e_acsl_51 == 0) { e_acsl_52 = 1; }
+ else {
+ mpz_t e_acsl_53;
+ mpz_t e_acsl_54;
+ mpz_t e_acsl_55;
+ mpz_t e_acsl_56;
+ mpz_t e_acsl_57;
+ int e_acsl_58;
+ mpz_t e_acsl_59;
+ int e_acsl_60;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_53),(long)y);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_54),(long)1);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_55),(long)0);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_56),(long)0);
+ mpz_init_set_ui((__mpz_struct *)(e_acsl_57),(unsigned long)0U);
+ e_acsl_58 = mpz_cmp((__mpz_struct const *)(e_acsl_56),
+ (__mpz_struct const *)(e_acsl_57));
+ mpz_init((__mpz_struct *)(e_acsl_59));
+ /*@ assert 0 ≢ 0U; */ ;
+ if (e_acsl_58 == 0) { e_acsl_fail((char *)"(0 == 0U)"); }
+ mpz_cdiv_q((__mpz_struct *)(e_acsl_59),
+ (__mpz_struct const *)(e_acsl_54),
+ (__mpz_struct const *)(e_acsl_55));
+ e_acsl_60 = mpz_cmp((__mpz_struct const *)(e_acsl_53),
+ (__mpz_struct const *)(e_acsl_59));
+ e_acsl_52 = e_acsl_60 == 0;
+ mpz_clear((__mpz_struct *)(e_acsl_53));
+ mpz_clear((__mpz_struct *)(e_acsl_54));
+ mpz_clear((__mpz_struct *)(e_acsl_55));
+ mpz_clear((__mpz_struct *)(e_acsl_56));
+ mpz_clear((__mpz_struct *)(e_acsl_57));
+ mpz_clear((__mpz_struct *)(e_acsl_59));
+ } if (! e_acsl_52) { e_acsl_fail((char *)"(x == 0 || y == 1/0)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_49));
+ mpz_clear((__mpz_struct *)(e_acsl_50));
+ }
+
+ /*@ assert x ≡ 0 ⇒ y ≡ 1; */ ;
+ { mpz_t e_acsl_64; mpz_t e_acsl_65; int e_acsl_66; int e_acsl_67;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_64),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_65),(long)0);
+ e_acsl_66 = mpz_cmp((__mpz_struct const *)(e_acsl_64),
+ (__mpz_struct const *)(e_acsl_65));
+ if (! (e_acsl_66 == 0)) { e_acsl_67 = 1; }
else {
- mpz_t e_acsl_65;
- mpz_t e_acsl_66;
- mpz_t e_acsl_67;
mpz_t e_acsl_68;
mpz_t e_acsl_69;
int e_acsl_70;
- mpz_t e_acsl_71;
- int e_acsl_72;
- mpz_init_set_si((__mpz_struct *)(e_acsl_65),(long)y);
- mpz_init_set_si((__mpz_struct *)(e_acsl_66),(long)1);
- mpz_init_set_si((__mpz_struct *)(e_acsl_67),(long)0);
- mpz_init_set_si((__mpz_struct *)(e_acsl_68),(long)0);
- mpz_init_set_ui((__mpz_struct *)(e_acsl_69),(unsigned long)0U);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_68),(long)y);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_69),(long)1);
e_acsl_70 = mpz_cmp((__mpz_struct const *)(e_acsl_68),
(__mpz_struct const *)(e_acsl_69));
- mpz_init((__mpz_struct *)(e_acsl_71));
- /*@ assert 0 ≢ 0U; */ ;
- if (e_acsl_70 == 0) { e_acsl_fail((char *)"(0 == 0U)"); }
- mpz_cdiv_q((__mpz_struct *)(e_acsl_71),
- (__mpz_struct const *)(e_acsl_66),
- (__mpz_struct const *)(e_acsl_67));
- e_acsl_72 = mpz_cmp((__mpz_struct const *)(e_acsl_65),
- (__mpz_struct const *)(e_acsl_71));
- e_acsl_61 = e_acsl_72 == 0;
- mpz_clear((__mpz_struct *)(e_acsl_65));
- mpz_clear((__mpz_struct *)(e_acsl_66));
- mpz_clear((__mpz_struct *)(e_acsl_67));
+ e_acsl_67 = e_acsl_70 == 0;
mpz_clear((__mpz_struct *)(e_acsl_68));
mpz_clear((__mpz_struct *)(e_acsl_69));
- mpz_clear((__mpz_struct *)(e_acsl_71));
- } if (! e_acsl_61) { e_acsl_fail((char *)"(x == 0 || y == 1/0)"); }
- mpz_clear((__mpz_struct *)(e_acsl_50));
- mpz_clear((__mpz_struct *)(e_acsl_51));
+ } if (! e_acsl_67) { e_acsl_fail((char *)"(x == 0 ==> y == 1)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_64));
+ mpz_clear((__mpz_struct *)(e_acsl_65));
}
- /*@ assert x ≡ 0 ⇒ y ≡ 1; */ ;
- { mpz_t e_acsl_73; mpz_t e_acsl_74; int e_acsl_75; int e_acsl_79;
- mpz_init_set_si((__mpz_struct *)(e_acsl_73),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_74),(long)0);
- e_acsl_75 = mpz_cmp((__mpz_struct const *)(e_acsl_73),
- (__mpz_struct const *)(e_acsl_74));
- if (! (e_acsl_75 == 0)) { e_acsl_79 = 1; }
+ /*@ assert x ≡ 1 ⇒ y ≡ 1/0; */ ;
+ { mpz_t e_acsl_79; mpz_t e_acsl_80; int e_acsl_81; int e_acsl_82;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_79),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_80),(long)1);
+ e_acsl_81 = mpz_cmp((__mpz_struct const *)(e_acsl_79),
+ (__mpz_struct const *)(e_acsl_80));
+ if (! (e_acsl_81 == 0)) { e_acsl_82 = 1; }
else {
mpz_t e_acsl_83;
mpz_t e_acsl_84;
- int e_acsl_85;
+ mpz_t e_acsl_85;
+ mpz_t e_acsl_86;
+ mpz_t e_acsl_87;
+ int e_acsl_88;
+ mpz_t e_acsl_89;
+ int e_acsl_90;
mpz_init_set_si((__mpz_struct *)(e_acsl_83),(long)y);
mpz_init_set_si((__mpz_struct *)(e_acsl_84),(long)1);
- e_acsl_85 = mpz_cmp((__mpz_struct const *)(e_acsl_83),
- (__mpz_struct const *)(e_acsl_84));
- e_acsl_79 = e_acsl_85 == 0;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_85),(long)0);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_86),(long)0);
+ mpz_init_set_ui((__mpz_struct *)(e_acsl_87),(unsigned long)0U);
+ e_acsl_88 = mpz_cmp((__mpz_struct const *)(e_acsl_86),
+ (__mpz_struct const *)(e_acsl_87));
+ mpz_init((__mpz_struct *)(e_acsl_89));
+ /*@ assert 0 ≢ 0U; */ ;
+ if (e_acsl_88 == 0) { e_acsl_fail((char *)"(0 == 0U)"); }
+ mpz_cdiv_q((__mpz_struct *)(e_acsl_89),
+ (__mpz_struct const *)(e_acsl_84),
+ (__mpz_struct const *)(e_acsl_85));
+ e_acsl_90 = mpz_cmp((__mpz_struct const *)(e_acsl_83),
+ (__mpz_struct const *)(e_acsl_89));
+ e_acsl_82 = e_acsl_90 == 0;
mpz_clear((__mpz_struct *)(e_acsl_83));
mpz_clear((__mpz_struct *)(e_acsl_84));
- } if (! e_acsl_79) { e_acsl_fail((char *)"(x == 0 ==> y == 1)"); }
- mpz_clear((__mpz_struct *)(e_acsl_73));
- mpz_clear((__mpz_struct *)(e_acsl_74));
- }
-
- /*@ assert x ≡ 1 ⇒ y ≡ 1/0; */ ;
- { mpz_t e_acsl_86; mpz_t e_acsl_87; int e_acsl_88; int e_acsl_97;
- mpz_init_set_si((__mpz_struct *)(e_acsl_86),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_87),(long)1);
- e_acsl_88 = mpz_cmp((__mpz_struct const *)(e_acsl_86),
- (__mpz_struct const *)(e_acsl_87));
- if (! (e_acsl_88 == 0)) { e_acsl_97 = 1; }
- else {
- mpz_t e_acsl_101;
- mpz_t e_acsl_102;
- mpz_t e_acsl_103;
- mpz_t e_acsl_104;
- mpz_t e_acsl_105;
- int e_acsl_106;
- mpz_t e_acsl_107;
- int e_acsl_108;
- mpz_init_set_si((__mpz_struct *)(e_acsl_101),(long)y);
- mpz_init_set_si((__mpz_struct *)(e_acsl_102),(long)1);
- mpz_init_set_si((__mpz_struct *)(e_acsl_103),(long)0);
- mpz_init_set_si((__mpz_struct *)(e_acsl_104),(long)0);
- mpz_init_set_ui((__mpz_struct *)(e_acsl_105),(unsigned long)0U);
- e_acsl_106 = mpz_cmp((__mpz_struct const *)(e_acsl_104),
- (__mpz_struct const *)(e_acsl_105));
- mpz_init((__mpz_struct *)(e_acsl_107));
- /*@ assert 0 ≢ 0U; */ ;
- if (e_acsl_106 == 0) { e_acsl_fail((char *)"(0 == 0U)"); }
- mpz_cdiv_q((__mpz_struct *)(e_acsl_107),
- (__mpz_struct const *)(e_acsl_102),
- (__mpz_struct const *)(e_acsl_103));
- e_acsl_108 = mpz_cmp((__mpz_struct const *)(e_acsl_101),
- (__mpz_struct const *)(e_acsl_107));
- e_acsl_97 = e_acsl_108 == 0;
- mpz_clear((__mpz_struct *)(e_acsl_101));
- mpz_clear((__mpz_struct *)(e_acsl_102));
- mpz_clear((__mpz_struct *)(e_acsl_103));
- mpz_clear((__mpz_struct *)(e_acsl_104));
- mpz_clear((__mpz_struct *)(e_acsl_105));
- mpz_clear((__mpz_struct *)(e_acsl_107));
- } if (! e_acsl_97) { e_acsl_fail((char *)"(x == 1 ==> y == 1/0)"); }
- mpz_clear((__mpz_struct *)(e_acsl_86));
- mpz_clear((__mpz_struct *)(e_acsl_87));
+ mpz_clear((__mpz_struct *)(e_acsl_85));
+ mpz_clear((__mpz_struct *)(e_acsl_86));
+ mpz_clear((__mpz_struct *)(e_acsl_87));
+ mpz_clear((__mpz_struct *)(e_acsl_89));
+ } if (! e_acsl_82) { e_acsl_fail((char *)"(x == 1 ==> y == 1/0)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_79));
+ mpz_clear((__mpz_struct *)(e_acsl_80));
}
__retres = 0;
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 20254dda5f1..94504c62f46 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -123,9 +123,9 @@ module Env : sig
(* Same as [new_var], but dedicated to mpz_t variables initialized by
{!Mpz.init}. *)
- val create_from: t -> t
- (* [create_from env] creates a fresh environment which does not overlap
- generated variables with [env]. *)
+ val no_overlap: from:t -> t -> t
+ (* [no_overlap ~from env] returns env, but ensures that new generated
+ variables will not overlap with those of [from]. *)
val merge: from:t -> t -> t
(* [merge ~from env] copies the generated variables of [from] to [env].
@@ -149,6 +149,10 @@ module Env : sig
(* [block env s] returns the block of statements including [s] and the new
constructs of [env]. *)
+ val block_option: t -> stmt -> block option
+ (* [block_option env s] returns the block of statements including [s] and the
+ new constructs of [env], if any. *)
+
val is_empty: t -> bool
(* Is the given environment empty? *)
@@ -166,17 +170,15 @@ end = struct
let empty =
{ var_cpt = 0; vars = [] ; beginning_of_block = []; end_of_block = [] }
- let create_from env =
- { var_cpt = env.var_cpt;
- vars = env.vars;
- beginning_of_block = [];
- end_of_block = [] }
+ let no_overlap ~from env =
+ { env with var_cpt = Extlib.max_cpt from.var_cpt env.var_cpt }
- let merge ~from env = { env with var_cpt = from.var_cpt; vars = from.vars }
+ let merge ~from env =
+ { env with var_cpt = from.var_cpt; vars = env.vars @ from.vars }
let is_empty env =
if env.beginning_of_block = [] then begin
- assert (env.end_of_block = []);
+ assert (env.end_of_block = [] && env.vars = []);
true
end else
false
@@ -223,6 +225,8 @@ end = struct
b.blocals <- b.blocals @ List.rev env.vars;
b
+ let block_option env s = if is_empty env then None else Some (block env s)
+
end
(* ************************************************************************** *)
@@ -408,7 +412,9 @@ let rec named_predicate_to_exp env p =
| Pand(p1, p2) ->
(* p1 && p2 <==> if p1 then p2 else false *)
let e1, env1 = named_predicate_to_exp env p1 in
- let e2, env2 = named_predicate_to_exp (Env.create_from env1) p2 in
+ let e2, env2 =
+ named_predicate_to_exp (Env.no_overlap ~from:env1 Env.empty) p2
+ in
let env = Env.merge ~from:env2 env1 in
Env.new_var
env
@@ -426,7 +432,9 @@ let rec named_predicate_to_exp env p =
| Por(p1, p2) ->
(* p1 || p2 <==> if p1 then true else p2 *)
let e1, env1 = named_predicate_to_exp env p1 in
- let e2, env2 = named_predicate_to_exp (Env.create_from env1) p2 in
+ let e2, env2 =
+ named_predicate_to_exp (Env.no_overlap ~from:env1 Env.empty) p2
+ in
let env = Env.merge ~from:env2 env1 in
Env.new_var
env
@@ -464,6 +472,61 @@ let rec named_predicate_to_exp env p =
statement (if any) for runtime assertion checking *)
(* ************************************************************************** *)
+let convert_preconditions _only_behaviors env _funspec behaviors =
+ if behaviors <> [] then not_yet "requires of behaviors";
+ let p = Logic_const.ptrue in
+ let e, env = named_predicate_to_exp env p in
+ p, e, env
+
+let convert_postconditions only_behaviors env behaviors =
+ let do_behavior p_acc b =
+ if List.mem b.b_name only_behaviors then begin
+ assert (b.b_assumes = []);
+ List.fold_left
+ (fun p_acc (t, p) ->
+ match t with
+ | Normal -> Logic_const.pand (p_acc, Logic_const.unamed p.ip_content)
+ | Exits | Breaks | Continues | Returns ->
+ not_yet "abnormal termination case in behavior")
+ p_acc
+ b.b_post_cond
+ end else
+ p_acc
+ in
+ (* conjunction of postconditions of behaviors *)
+ let p = List.fold_left do_behavior Logic_const.ptrue behaviors in
+ let e, env = named_predicate_to_exp env p in
+ p, e, env
+
+let convert_behaviors only_behaviors env funspec behaviors =
+ (* [TODO] untested *)
+ List.iter
+ (fun b ->
+ if b.b_assumes <> [] then not_yet "assumes clause in behavior";
+ if b.b_assigns <> WritesAny then not_yet "assigns clause in behavior";
+ if b.b_extended <> [] then not_yet "grammar extensions in behavior")
+ behaviors;
+ let pre_p, pre_e, pre_env =
+ convert_preconditions only_behaviors env funspec behaviors
+ in
+ let pre_block = Env.block_option pre_env (mk_e_acsl_guard pre_e pre_p) in
+ let post_p, post_e, post_env =
+ convert_postconditions
+ only_behaviors (Env.no_overlap ~from:pre_env env) behaviors
+ in
+ let post_block = Env.block_option post_env (mk_e_acsl_guard post_e post_p) in
+ pre_block, post_block, post_env
+
+let convert_spec only_behaviors env spec =
+ if spec.spec_variant <> None then not_yet "variant clause";
+ if spec.spec_terminates <> None then
+ not_yet "terminates clause";
+ if spec.spec_complete_behaviors <> [] then
+ not_yet "complete behaviors";
+ if spec.spec_disjoint_behaviors <> [] then
+ not_yet "disjoint behaviors";
+ convert_behaviors only_behaviors env spec spec.spec_behavior
+
let convert_named_predicate env p =
let e, env = named_predicate_to_exp env p in
assert (Typ.equal (typeOf e) intType);
@@ -474,8 +537,21 @@ let convert_named_predicate env p =
let convert_annotation env annot =
try
match annot.annot_content with
- | AAssert(_l, p) -> convert_named_predicate env p
- | AStmtSpec _ -> not_yet "stmt spec"
+ | AAssert(l, p) ->
+ if l <> [] then not_yet "assertions applied only on some behaviors";
+ convert_named_predicate env p, None
+ | AStmtSpec(only_behaviors, spec) ->
+ let pre_block, post_block, post_env =
+ convert_spec only_behaviors env spec
+ in
+ let env = match pre_block with
+ | None -> env
+ | Some b ->
+ Env.add_stmt
+ (Env.no_overlap ~from:post_env env)
+ (mkStmt ~valid_sid:true (Block b))
+ in
+ env, post_block
| AInvariant _ -> not_yet "invariant"
| AVariant _ -> not_yet "variant"
| AAssigns _ -> not_yet "assigns"
@@ -484,7 +560,7 @@ let convert_annotation env annot =
let msg = Format.sprintf "invalid E-ACSL construct %s." s in
if Options.Check.get () then type_error msg
else Options.warning ~current:true "%s@\nignoring annotation." msg;
- env
+ env, None
let convert_rooted env (User a | AI(_, a)) = convert_annotation env a
@@ -503,6 +579,8 @@ class e_acsl_visitor prj generate = object (self)
((if generate then Cil.copy_visit else Cil.inplace_visit) ())
val mutable gen_vars = []
+ val mutable pre_block = None
+ val mutable post_block = None
method vglob_aux g =
if !first_global then begin
@@ -518,30 +596,40 @@ class e_acsl_visitor prj generate = object (self)
method vvdec vi =
try
let kf = Globals.Functions.get vi in
- let spec = Kernel_function.get_spec kf in
- if spec.spec_behavior <> [] then not_yet "behaviors clause of function";
- if spec.spec_variant <> None then not_yet "variant clause of function";
- if spec.spec_terminates <> None then
- not_yet "terminates clause of function";
- if spec.spec_complete_behaviors <> [] then
- not_yet "complete behaviors of function";
- if spec.spec_disjoint_behaviors <> [] then
- not_yet "disjoint behaviors of function";
+ let pre_b, post_b, env =
+ convert_spec [] Env.empty (Kernel_function.get_spec kf)
+ in
+ pre_block <- pre_b;
+ post_block <- post_b;
+ if pre_b <> None then not_yet "precondition in function contract";
+ if post_b <> None then not_yet "postcondition in function contract";
+ gen_vars <- Env.generated_variables env;
DoChildren
with Not_found ->
DoChildren
method vfundec f =
- let add_gen_vars f = f.slocals <- gen_vars @ f.slocals; f in
+ let contract_vars = gen_vars in
+ let add_gen_vars f =
+ f.slocals <- contract_vars @ gen_vars @ f.slocals;
+ gen_vars <- [];
+ f
+ in
ChangeDoChildrenPost(f, add_gen_vars)
method vstmt_aux stmt =
(* Options.debug ~level:2 "proceeding stmt %d@." stmt.sid;*)
- let env =
+ let env, post_stmts =
Annotations.single_fold_stmt
- (fun ba env -> convert_rooted env ba)
+ (fun ba (env, post_stmts) ->
+ let env, post_block = convert_rooted env ba in
+ let post_stmts = match post_block with
+ | None -> post_stmts
+ | Some b -> mkStmt ~valid_sid:true (Block b) :: post_stmts
+ in
+ env, post_stmts)
stmt
- Env.empty
+ (Env.empty, [])
in
if Env.is_empty env then
DoChildren
@@ -549,7 +637,8 @@ class e_acsl_visitor prj generate = object (self)
assert generate;
let mk_block stmt =
gen_vars <- Env.generated_variables env;
- mkStmt ~valid_sid:true (Block (Env.block env stmt))
+ let s = mkStmt ~valid_sid:true (Block (Env.block env stmt)) in
+ mkStmt ~valid_sid:true (Block (mkBlock (s :: post_stmts)))
in
ChangeDoChildrenPost(stmt, mk_block)
end
--
GitLab