diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i b/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
index e3002072d798c5c8aa42a6664015e5675e016be9..89d51537c241d2c97838d214355977e9e1676bb7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
@@ -63,6 +63,17 @@ int l() {
@ ensures X == \old(X) + Y; */
void m(void) { X += Y; }
+// mix requires, ensures and assumes
+/*@ requires X > 0;
+ @ requires X < 10;
+ @ behavior b1:
+ @ assumes X == 7;
+ @ ensures X == 8;
+ @ behavior b2:
+ @ assumes X == 5;
+ @ ensures X == 98; */
+void n(void) { X ++; }
+
int main(void) {
f();
g();
@@ -72,5 +83,6 @@ int main(void) {
k();
l();
m();
+ n();
return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
index 29db38b07613efb88a79c23afaaf3cf95ab4437e..1349b58541fa9d9824ca4063b13ee7af6e9e0cb5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
@@ -5,7 +5,7 @@
X ∈ {0}
Y ∈ {2}
[value] computing for function f <- main.
- Called from PROJECT_FILE.i:697.
+ Called from PROJECT_FILE.i:792.
[value] computing for function __gmpz_init_set_si <- f <- main.
Called from PROJECT_FILE.i:251.
[value] using specification for function __gmpz_init_set_si
@@ -37,7 +37,7 @@ PROJECT_FILE.i:243:[value] Function f: postcondition got status valid.
[value] Recording results for f
[value] Done for function f
[value] computing for function g <- main.
- Called from PROJECT_FILE.i:698.
+ Called from PROJECT_FILE.i:793.
[value] computing for function __gmpz_init_set_si <- g <- main.
Called from PROJECT_FILE.i:273.
[value] Done for function __gmpz_init_set_si
@@ -75,7 +75,7 @@ PROJECT_FILE.i:263:[value] Function g: postcondition got status valid.
[value] Recording results for g
[value] Done for function g
[value] computing for function h <- main.
- Called from PROJECT_FILE.i:699.
+ Called from PROJECT_FILE.i:794.
PROJECT_FILE.i:288:[value] Function h: precondition got status valid.
[value] computing for function __gmpz_init_set_si <- h <- main.
Called from PROJECT_FILE.i:295.
@@ -99,7 +99,7 @@ PROJECT_FILE.i:288:[value] Function h: precondition got status valid.
[value] Recording results for h
[value] Done for function h
[value] computing for function i <- main.
- Called from PROJECT_FILE.i:700.
+ Called from PROJECT_FILE.i:795.
PROJECT_FILE.i:307:[value] Function i: precondition got status valid.
PROJECT_FILE.i:308:[value] Function i: precondition got status valid.
[value] computing for function __gmpz_init_set_si <- i <- main.
@@ -143,7 +143,7 @@ PROJECT_FILE.i:308:[value] Function i: precondition got status valid.
[value] Recording results for i
[value] Done for function i
[value] computing for function j <- main.
- Called from PROJECT_FILE.i:701.
+ Called from PROJECT_FILE.i:796.
PROJECT_FILE.i:337:[value] Function j, behavior b1: precondition got status valid.
PROJECT_FILE.i:341:[value] Function j, behavior b2: precondition got status valid.
PROJECT_FILE.i:342:[value] Function j, behavior b2: precondition got status valid.
@@ -265,7 +265,7 @@ PROJECT_FILE.i:343:[value] Function j, behavior b2: postcondition got status val
[value] Recording results for j
[value] Done for function j
[value] computing for function k <- main.
- Called from PROJECT_FILE.i:702.
+ Called from PROJECT_FILE.i:797.
PROJECT_FILE.i:411:[value] Function k, behavior b1: assumption got status invalid; precondition not evaluated.
PROJECT_FILE.i:416:[value] Function k, behavior b2: precondition got status valid.
PROJECT_FILE.i:417:[value] Function k, behavior b2: precondition got status valid.
@@ -402,7 +402,7 @@ PROJECT_FILE.i:446:[value] assigning non deterministic value for the first time
[value] Recording results for k
[value] Done for function k
[value] computing for function l <- main.
- Called from PROJECT_FILE.i:703.
+ Called from PROJECT_FILE.i:798.
PROJECT_FILE.i:525:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_si <- l <- main.
Called from PROJECT_FILE.i:530.
@@ -446,7 +446,7 @@ PROJECT_FILE.i:522:[value] Function l: postcondition got status valid.
[value] Recording results for l
[value] Done for function l
[value] computing for function m <- main.
- Called from PROJECT_FILE.i:704.
+ Called from PROJECT_FILE.i:799.
[value] computing for function __gmpz_init_set_si <- m <- main.
Called from PROJECT_FILE.i:578.
[value] Done for function __gmpz_init_set_si
@@ -599,6 +599,114 @@ PROJECT_FILE.i:561:[value] Function m, behavior b2: postcondition got status val
PROJECT_FILE.i:562:[value] Function m, behavior b2: postcondition got status valid.
[value] Recording results for m
[value] Done for function m
+[value] computing for function n <- main.
+ Called from PROJECT_FILE.i:800.
+PROJECT_FILE.i:694:[value] Function n: precondition got status valid.
+PROJECT_FILE.i:695:[value] Function n: precondition got status valid.
+[value] computing for function __gmpz_init_set_si <- n <- main.
+ Called from PROJECT_FILE.i:716.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- n <- main.
+ Called from PROJECT_FILE.i:717.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- n <- main.
+ Called from PROJECT_FILE.i:718.
+[value] Done for function __gmpz_cmp
+[value] computing for function e_acsl_assert <- n <- main.
+ Called from PROJECT_FILE.i:719.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_init_set_si <- n <- main.
+ Called from PROJECT_FILE.i:720.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- n <- main.
+ Called from PROJECT_FILE.i:721.
+[value] Done for function __gmpz_cmp
+[value] computing for function e_acsl_assert <- n <- main.
+ Called from PROJECT_FILE.i:722.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_clear <- n <- main.
+ Called from PROJECT_FILE.i:723.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- n <- main.
+ Called from PROJECT_FILE.i:724.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- n <- main.
+ Called from PROJECT_FILE.i:725.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init_set_si <- n <- main.
+ Called from PROJECT_FILE.i:730.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- n <- main.
+ Called from PROJECT_FILE.i:731.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- n <- main.
+ Called from PROJECT_FILE.i:732.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- n <- main.
+ Called from PROJECT_FILE.i:734.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- n <- main.
+ Called from PROJECT_FILE.i:735.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init_set_si <- n <- main.
+ Called from PROJECT_FILE.i:742.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- n <- main.
+ Called from PROJECT_FILE.i:743.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- n <- main.
+ Called from PROJECT_FILE.i:744.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- n <- main.
+ Called from PROJECT_FILE.i:746.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- n <- main.
+ Called from PROJECT_FILE.i:747.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init_set_si <- n <- main.
+ Called from PROJECT_FILE.i:761.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- n <- main.
+ Called from PROJECT_FILE.i:762.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- n <- main.
+ Called from PROJECT_FILE.i:763.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- n <- main.
+ Called from PROJECT_FILE.i:765.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- n <- main.
+ Called from PROJECT_FILE.i:766.
+[value] Done for function __gmpz_clear
+[value] computing for function e_acsl_assert <- n <- main.
+ Called from PROJECT_FILE.i:768.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_init_set_si <- n <- main.
+ Called from PROJECT_FILE.i:775.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- n <- main.
+ Called from PROJECT_FILE.i:776.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- n <- main.
+ Called from PROJECT_FILE.i:777.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- n <- main.
+ Called from PROJECT_FILE.i:779.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- n <- main.
+ Called from PROJECT_FILE.i:780.
+[value] Done for function __gmpz_clear
+[value] computing for function e_acsl_assert <- n <- main.
+ Called from PROJECT_FILE.i:782.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+PROJECT_FILE.i:698:[value] Function n, behavior b1: postcondition got status valid.
+PROJECT_FILE.i:702:[value] Function n, behavior b2: assumes got status invalid; post-condition not evaluated.
+[value] Recording results for n
+[value] Done for function n
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
@@ -622,8 +730,12 @@ PROJECT_FILE.i:562:[value] Function m, behavior b2: postcondition got status val
__e_acsl_at_2 ∈ {0; 1}
__e_acsl_at_3 ∈ {0; 1}
__e_acsl_at_4 ∈ {5}
+[value] Values at end of function n:
+ X ∈ {8}
+ __e_acsl_at ∈ {0; 1}
+ __e_acsl_at_2 ∈ {0; 1}
[value] Values at end of function main:
- X ∈ {7}
+ X ∈ {8}
__retres ∈ {0}
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
@@ -1192,6 +1304,109 @@ void m(void)
}
+/*@ requires X > 0;
+ requires X < 10;
+ behavior b1:
+ assumes X ≡ 7;
+ ensures X ≡ 8;
+
+ behavior b2:
+ assumes X ≡ 5;
+ ensures X ≡ 98;
+
+
+*/
+void n(void)
+{
+ int __e_acsl_at;
+ int __e_acsl_at_2;
+ {
+ mpz_t __e_acsl_X;
+ mpz_t __e_acsl;
+ int __e_acsl_gt;
+ mpz_t __e_acsl_2;
+ int __e_acsl_lt;
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_X),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl),(long)0);
+ __e_acsl_gt = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X),
+ (__mpz_struct const *)(__e_acsl));
+ e_acsl_assert(__e_acsl_gt > 0,(char *)"Precondition",(char *)"(X > 0)",
+ 67);
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_2),(long)10);
+ __e_acsl_lt = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X),
+ (__mpz_struct const *)(__e_acsl_2));
+ e_acsl_assert(__e_acsl_lt < 0,(char *)"Precondition",(char *)"(X < 10)",
+ 68);
+ __gmpz_clear((__mpz_struct *)(__e_acsl_X));
+ __gmpz_clear((__mpz_struct *)(__e_acsl));
+ __gmpz_clear((__mpz_struct *)(__e_acsl_2));
+ {
+ mpz_t __e_acsl_X_4;
+ mpz_t __e_acsl_5;
+ int __e_acsl_eq_3;
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_X_4),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_5),(long)5);
+ __e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_4),
+ (__mpz_struct const *)(__e_acsl_5));
+ __e_acsl_at_2 = __e_acsl_eq_3 == 0;
+ __gmpz_clear((__mpz_struct *)(__e_acsl_X_4));
+ __gmpz_clear((__mpz_struct *)(__e_acsl_5));
+ }
+
+ {
+ mpz_t __e_acsl_X_2;
+ mpz_t __e_acsl_3;
+ int __e_acsl_eq;
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_X_2),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_3),(long)7);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_2),
+ (__mpz_struct const *)(__e_acsl_3));
+ __e_acsl_at = __e_acsl_eq == 0;
+ __gmpz_clear((__mpz_struct *)(__e_acsl_X_2));
+ __gmpz_clear((__mpz_struct *)(__e_acsl_3));
+ }
+
+ X ++;
+ }
+
+ {
+ int __e_acsl_implies;
+ int __e_acsl_implies_2;
+ if (! __e_acsl_at) { __e_acsl_implies = 1; }
+ else {
+ mpz_t __e_acsl_X_3;
+ mpz_t __e_acsl_4;
+ int __e_acsl_eq_2;
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_X_3),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_4),(long)8);
+ __e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_3),
+ (__mpz_struct const *)(__e_acsl_4));
+ __e_acsl_implies = __e_acsl_eq_2 == 0;
+ __gmpz_clear((__mpz_struct *)(__e_acsl_X_3));
+ __gmpz_clear((__mpz_struct *)(__e_acsl_4));
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"(\\old(X == 7) ==> X == 8)",71);
+ if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
+ else {
+ mpz_t __e_acsl_X_5;
+ mpz_t __e_acsl_6;
+ int __e_acsl_eq_4;
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_X_5),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_6),(long)98);
+ __e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_5),
+ (__mpz_struct const *)(__e_acsl_6));
+ __e_acsl_implies_2 = __e_acsl_eq_4 == 0;
+ __gmpz_clear((__mpz_struct *)(__e_acsl_X_5));
+ __gmpz_clear((__mpz_struct *)(__e_acsl_6));
+ }
+ e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"(\\old(X == 5) ==> X == 98)",74);
+ return;
+ }
+
+}
+
int main(void)
{
int __retres;
@@ -1203,6 +1418,7 @@ int main(void)
k();
l();
m();
+ n();
__retres = 0;
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
index 88e50b41ba606374001a820595751010bab36374..e7e2a7b86f573bd80d934867a7668bd0b012cc9c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
@@ -5,7 +5,7 @@
X ∈ {0}
Y ∈ {2}
[value] computing for function f <- main.
- Called from PROJECT_FILE.i:414.
+ Called from PROJECT_FILE.i:451.
[value] computing for function e_acsl_assert <- f <- main.
Called from PROJECT_FILE.i:247.
PROJECT_FILE.i:231:[value] Function e_acsl_assert: precondition got status valid.
@@ -15,7 +15,7 @@ PROJECT_FILE.i:243:[value] Function f: postcondition got status valid.
[value] Recording results for f
[value] Done for function f
[value] computing for function g <- main.
- Called from PROJECT_FILE.i:415.
+ Called from PROJECT_FILE.i:452.
[value] computing for function e_acsl_assert <- g <- main.
Called from PROJECT_FILE.i:256.
[value] Recording results for e_acsl_assert
@@ -29,7 +29,7 @@ PROJECT_FILE.i:252:[value] Function g: postcondition got status valid.
[value] Recording results for g
[value] Done for function g
[value] computing for function h <- main.
- Called from PROJECT_FILE.i:416.
+ Called from PROJECT_FILE.i:453.
PROJECT_FILE.i:261:[value] Function h: precondition got status valid.
[value] computing for function e_acsl_assert <- h <- main.
Called from PROJECT_FILE.i:264.
@@ -38,7 +38,7 @@ PROJECT_FILE.i:261:[value] Function h: precondition got status valid.
[value] Recording results for h
[value] Done for function h
[value] computing for function i <- main.
- Called from PROJECT_FILE.i:417.
+ Called from PROJECT_FILE.i:454.
PROJECT_FILE.i:269:[value] Function i: precondition got status valid.
PROJECT_FILE.i:270:[value] Function i: precondition got status valid.
[value] computing for function e_acsl_assert <- i <- main.
@@ -52,7 +52,7 @@ PROJECT_FILE.i:270:[value] Function i: precondition got status valid.
[value] Recording results for i
[value] Done for function i
[value] computing for function j <- main.
- Called from PROJECT_FILE.i:418.
+ Called from PROJECT_FILE.i:455.
PROJECT_FILE.i:280:[value] Function j, behavior b1: precondition got status valid.
PROJECT_FILE.i:284:[value] Function j, behavior b2: precondition got status valid.
PROJECT_FILE.i:285:[value] Function j, behavior b2: precondition got status valid.
@@ -81,7 +81,7 @@ PROJECT_FILE.i:286:[value] Function j, behavior b2: postcondition got status val
[value] Recording results for j
[value] Done for function j
[value] computing for function k <- main.
- Called from PROJECT_FILE.i:419.
+ Called from PROJECT_FILE.i:456.
PROJECT_FILE.i:305:[value] Function k, behavior b1: assumption got status invalid; precondition not evaluated.
PROJECT_FILE.i:310:[value] Function k, behavior b2: precondition got status valid.
PROJECT_FILE.i:311:[value] Function k, behavior b2: precondition got status valid.
@@ -100,7 +100,7 @@ PROJECT_FILE.i:311:[value] Function k, behavior b2: precondition got status vali
[value] Recording results for k
[value] Done for function k
[value] computing for function l <- main.
- Called from PROJECT_FILE.i:420.
+ Called from PROJECT_FILE.i:457.
PROJECT_FILE.i:348:[value] Assertion got status valid.
[value] computing for function e_acsl_assert <- l <- main.
Called from PROJECT_FILE.i:349.
@@ -114,7 +114,7 @@ PROJECT_FILE.i:345:[value] Function l: postcondition got status valid.
[value] Recording results for l
[value] Done for function l
[value] computing for function m <- main.
- Called from PROJECT_FILE.i:421.
+ Called from PROJECT_FILE.i:458.
[value] computing for function e_acsl_assert <- m <- main.
Called from PROJECT_FILE.i:394.
[value] Recording results for e_acsl_assert
@@ -132,6 +132,30 @@ PROJECT_FILE.i:362:[value] Function m, behavior b2: postcondition got status val
PROJECT_FILE.i:363:[value] Function m, behavior b2: postcondition got status valid.
[value] Recording results for m
[value] Done for function m
+[value] computing for function n <- main.
+ Called from PROJECT_FILE.i:459.
+PROJECT_FILE.i:411:[value] Function n: precondition got status valid.
+PROJECT_FILE.i:412:[value] Function n: precondition got status valid.
+[value] computing for function e_acsl_assert <- n <- main.
+ Called from PROJECT_FILE.i:427.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function e_acsl_assert <- n <- main.
+ Called from PROJECT_FILE.i:428.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function e_acsl_assert <- n <- main.
+ Called from PROJECT_FILE.i:437.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function e_acsl_assert <- n <- main.
+ Called from PROJECT_FILE.i:441.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+PROJECT_FILE.i:415:[value] Function n, behavior b1: postcondition got status valid.
+PROJECT_FILE.i:419:[value] Function n, behavior b2: assumes got status invalid; post-condition not evaluated.
+[value] Recording results for n
+[value] Done for function n
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
@@ -155,8 +179,12 @@ PROJECT_FILE.i:363:[value] Function m, behavior b2: postcondition got status val
__e_acsl_at_2 ∈ {1}
__e_acsl_at_3 ∈ {1}
__e_acsl_at_4 ∈ {5}
+[value] Values at end of function n:
+ X ∈ {8}
+ __e_acsl_at ∈ {1}
+ __e_acsl_at_2 ∈ {0}
[value] Values at end of function main:
- X ∈ {7}
+ X ∈ {8}
__retres ∈ {0}
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
@@ -356,6 +384,43 @@ void m(void)
}
+/*@ requires X > 0;
+ requires X < 10;
+ behavior b1:
+ assumes X ≡ 7;
+ ensures X ≡ 8;
+
+ behavior b2:
+ assumes X ≡ 5;
+ ensures X ≡ 98;
+
+
+*/
+void n(void)
+{
+ int __e_acsl_at;
+ int __e_acsl_at_2;
+ e_acsl_assert(X > 0,(char *)"Precondition",(char *)"(X > 0)",67);
+ e_acsl_assert(X < 10,(char *)"Precondition",(char *)"(X < 10)",68);
+ __e_acsl_at_2 = X == 5;
+ __e_acsl_at = X == 7;
+ X ++;
+ {
+ int __e_acsl_implies;
+ int __e_acsl_implies_2;
+ if (! __e_acsl_at) { __e_acsl_implies = 1; }
+ else { __e_acsl_implies = X == 8; }
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"(\\old(X == 7) ==> X == 8)",71);
+ if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
+ else { __e_acsl_implies_2 = X == 98; }
+ e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"(\\old(X == 5) ==> X == 98)",74);
+ return;
+ }
+
+}
+
int main(void)
{
int __retres;
@@ -367,6 +432,7 @@ int main(void)
k();
l();
m();
+ n();
__retres = 0;
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
index 0285beae055f9d7a7f6682885d0818ebcf4f295d..58f94f55cfdc1927dbdb9ecd53103c18c6a70988 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
@@ -196,6 +196,43 @@ void m(void)
}
+/*@ requires X > 0;
+ requires X < 10;
+ behavior b1:
+ assumes X ≡ 7;
+ ensures X ≡ 8;
+
+ behavior b2:
+ assumes X ≡ 5;
+ ensures X ≡ 98;
+
+
+*/
+void n(void)
+{
+ int __e_acsl_at;
+ int __e_acsl_at_2;
+ e_acsl_assert(X > 0,(char *)"Precondition",(char *)"(X > 0)",67);
+ e_acsl_assert(X < 10,(char *)"Precondition",(char *)"(X < 10)",68);
+ __e_acsl_at_2 = X == 5;
+ __e_acsl_at = X == 7;
+ X ++;
+ {
+ int __e_acsl_implies;
+ int __e_acsl_implies_2;
+ if (! __e_acsl_at) { __e_acsl_implies = 1; }
+ else { __e_acsl_implies = X == 8; }
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"(\\old(X == 7) ==> X == 8)",71);
+ if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
+ else { __e_acsl_implies_2 = X == 98; }
+ e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"(\\old(X == 5) ==> X == 98)",74);
+ return;
+ }
+
+}
+
int main(void)
{
int __retres;
@@ -207,6 +244,7 @@ int main(void)
k();
l();
m();
+ n();
__retres = 0;
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
index fba1ec725786986b5f47396b5094b8bf781f2503..3d6b00f3429fd1c661fb1ecfb4a49eb825162ba6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
@@ -561,6 +561,109 @@ void m(void)
}
+/*@ requires X > 0;
+ requires X < 10;
+ behavior b1:
+ assumes X ≡ 7;
+ ensures X ≡ 8;
+
+ behavior b2:
+ assumes X ≡ 5;
+ ensures X ≡ 98;
+
+
+*/
+void n(void)
+{
+ int __e_acsl_at;
+ int __e_acsl_at_2;
+ {
+ mpz_t __e_acsl_X;
+ mpz_t __e_acsl;
+ int __e_acsl_gt;
+ mpz_t __e_acsl_2;
+ int __e_acsl_lt;
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_X),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl),(long)0);
+ __e_acsl_gt = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X),
+ (__mpz_struct const *)(__e_acsl));
+ e_acsl_assert(__e_acsl_gt > 0,(char *)"Precondition",(char *)"(X > 0)",
+ 67);
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_2),(long)10);
+ __e_acsl_lt = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X),
+ (__mpz_struct const *)(__e_acsl_2));
+ e_acsl_assert(__e_acsl_lt < 0,(char *)"Precondition",(char *)"(X < 10)",
+ 68);
+ __gmpz_clear((__mpz_struct *)(__e_acsl_X));
+ __gmpz_clear((__mpz_struct *)(__e_acsl));
+ __gmpz_clear((__mpz_struct *)(__e_acsl_2));
+ {
+ mpz_t __e_acsl_X_4;
+ mpz_t __e_acsl_5;
+ int __e_acsl_eq_3;
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_X_4),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_5),(long)5);
+ __e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_4),
+ (__mpz_struct const *)(__e_acsl_5));
+ __e_acsl_at_2 = __e_acsl_eq_3 == 0;
+ __gmpz_clear((__mpz_struct *)(__e_acsl_X_4));
+ __gmpz_clear((__mpz_struct *)(__e_acsl_5));
+ }
+
+ {
+ mpz_t __e_acsl_X_2;
+ mpz_t __e_acsl_3;
+ int __e_acsl_eq;
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_X_2),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_3),(long)7);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_2),
+ (__mpz_struct const *)(__e_acsl_3));
+ __e_acsl_at = __e_acsl_eq == 0;
+ __gmpz_clear((__mpz_struct *)(__e_acsl_X_2));
+ __gmpz_clear((__mpz_struct *)(__e_acsl_3));
+ }
+
+ X ++;
+ }
+
+ {
+ int __e_acsl_implies;
+ int __e_acsl_implies_2;
+ if (! __e_acsl_at) { __e_acsl_implies = 1; }
+ else {
+ mpz_t __e_acsl_X_3;
+ mpz_t __e_acsl_4;
+ int __e_acsl_eq_2;
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_X_3),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_4),(long)8);
+ __e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_3),
+ (__mpz_struct const *)(__e_acsl_4));
+ __e_acsl_implies = __e_acsl_eq_2 == 0;
+ __gmpz_clear((__mpz_struct *)(__e_acsl_X_3));
+ __gmpz_clear((__mpz_struct *)(__e_acsl_4));
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"(\\old(X == 7) ==> X == 8)",71);
+ if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
+ else {
+ mpz_t __e_acsl_X_5;
+ mpz_t __e_acsl_6;
+ int __e_acsl_eq_4;
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_X_5),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(__e_acsl_6),(long)98);
+ __e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_5),
+ (__mpz_struct const *)(__e_acsl_6));
+ __e_acsl_implies_2 = __e_acsl_eq_4 == 0;
+ __gmpz_clear((__mpz_struct *)(__e_acsl_X_5));
+ __gmpz_clear((__mpz_struct *)(__e_acsl_6));
+ }
+ e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"(\\old(X == 5) ==> X == 98)",74);
+ return;
+ }
+
+}
+
int main(void)
{
int __retres;
@@ -572,6 +675,7 @@ int main(void)
k();
l();
m();
+ n();
__retres = 0;
return (__retres);
}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 4e1ca198c5e152fe41b2e6a6e0edc87e4f9cddec..51c9282a99dc21dd0dad3936156e38bb966e1f71 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -515,13 +515,16 @@ let convert_preconditions env behaviors =
let assumes_pred = assumes_predicate b in
List.fold_left
(fun env p ->
- let loc = p.ip_loc in
- let p =
- Logic_const.pimplies
- ~loc
- (assumes_pred, Logic_const.unamed ~loc p.ip_content)
+ let do_it env =
+ let loc = p.ip_loc in
+ let p =
+ Logic_const.pimplies
+ ~loc
+ (assumes_pred, Logic_const.unamed ~loc p.ip_content)
+ in
+ convert_named_predicate env p
in
- convert_named_predicate env p)
+ Error.handle do_it env)
env
b.b_requires
in
@@ -534,22 +537,25 @@ let convert_postconditions env behaviors =
let assumes_pred = assumes_predicate b in
List.fold_left
(fun env (t, p) ->
- if b.b_assigns <> WritesAny then
- Error.not_yet "assigns clause in behavior";
- if b.b_extended <> [] then
- Error.not_yet "grammar extensions in behavior";
- match t with
- | Normal ->
- let loc = p.ip_loc in
- let p = p.ip_content in
- let p =
- Logic_const.pimplies
- ~loc
- (Logic_const.pold ~loc assumes_pred, Logic_const.unamed ~loc p)
- in
- convert_named_predicate env p
- | Exits | Breaks | Continues | Returns ->
- Error.not_yet "@[abnormal termination case in behavior@]")
+ let do_it env =
+ if b.b_assigns <> WritesAny then
+ Error.not_yet "assigns clause in behavior";
+ if b.b_extended <> [] then
+ Error.not_yet "grammar extensions in behavior";
+ match t with
+ | Normal ->
+ let loc = p.ip_loc in
+ let p = p.ip_content in
+ let p =
+ Logic_const.pimplies
+ ~loc
+ (Logic_const.pold ~loc assumes_pred, Logic_const.unamed ~loc p)
+ in
+ convert_named_predicate env p
+ | Exits | Breaks | Continues | Returns ->
+ Error.not_yet "@[abnormal termination case in behavior@]"
+ in
+ Error.handle do_it env)
env
b.b_post_cond
in