diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 7b63124a1cfafb9b40c9e3426550073491bd7ee0..af8f4f3c9462fc5801d88447d98992e1f2199804 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -13,8 +13,6 @@ the plug-in would generate something like
- mkcall ne devrait pas générer de nouvelles variables pour une même fonction
-[TODO?] mettre des locations intelligentes
-
- garde pour les casts quand overflows potentiels
(même pas de warnings aujourd'hui)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i b/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
index 66fe087cc2a1038cc064ca6e3d61474ab2a3030b..8e3d7aca223a0cf6e1aaab3b2d7ff15f57d9293c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
@@ -1,8 +1,9 @@
/* run.config
COMMENT: addrOf
- EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/addrOf.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_addrOf.out ./tests/e-acsl-runtime/result/gen_addrOf.c
+ EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/addrOf.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_addrOf.out ./tests/e-acsl-runtime/result/gen_addrOf.c && ./tests/e-acsl-runtime/result/gen_addrOf.out
*/
-void main() {
+int main(void) {
int x = 0;
/*@ assert &x == &x; */ ;
+ return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i b/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
index 148415d0fa41ec37b9652f88cbbd5bb37dd270e8..9232fe25d4cf20db9523acfd04f084020025c1f2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
@@ -4,7 +4,7 @@
EXECNOW: LOG gen_arith.c BIN gen_arith.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/arith.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_arith.out -lgmp ./tests/e-acsl-runtime/result/gen_arith.c
*/
-void main() {
+int main(void) {
int x = -3;
int y = 2;
@@ -28,4 +28,6 @@ void main() {
// /*@ assert 0 == !1; */ ;
/* subtyping relation: 0 should be promoted to boolean below
How to handle this? See BTS #751 */
+
+ return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i b/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
index d0faa4247612be309bfc735a2cfd5b7dab6fdc35..a93d8a436376dbc6ffe8c8908159781c69e13803 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
@@ -1,11 +1,12 @@
/* run.config
COMMENT: cast
- EXECNOW: LOG gen_cast.c BIN gen_cast.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/cast.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_cast.out ./tests/e-acsl-runtime/result/gen_cast.c
+ EXECNOW: LOG gen_cast.c BIN gen_cast.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/cast.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_cast.out ./tests/e-acsl-runtime/result/gen_cast.c && ./tests/e-acsl-runtime/result/gen_cast.out
*/
-void main() {
+int main(void) {
long x = 0;
int y = 0;
/*@ assert (int)x == y; */ ;
/*@ assert x == (long)y; */ ;
+ return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i b/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
index 7b9ede66903b9839cb88031bf0a3bfa9dbe50763..2a3bbed26ce930b4bec9967f6fc033c9f2768b28 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
@@ -1,9 +1,9 @@
/* run.config
COMMENT: comparison operators
- EXECNOW: LOG gen_comparison.c BIN gen_comparison.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/comparison.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_comparison.out -lgmp ./tests/e-acsl-runtime/result/gen_comparison.c
+ EXECNOW: LOG gen_comparison.c BIN gen_comparison.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/comparison.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_comparison.out -lgmp ./tests/e-acsl-runtime/result/gen_comparison.c && ./tests/e-acsl-runtime/result/gen_comparison.out
*/
-void main() {
+int main(void) {
int x = 0, y = 1;
/*@ assert x < y; */
/*@ assert y > x; */
@@ -18,4 +18,5 @@ void main() {
/*@ assert 123 >= 12; */
/*@ assert 0xff == 0xff; */
/*@ assert 1 != 2; */
+ return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/false.i b/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
index cd0a76b0dd5f52a71e72528105ee6d6fa1a3a9e0..051451ade6db2837f64d1ade436cd2ce14be7015 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
@@ -1,8 +1,9 @@
/* run.config
COMMENT: assert \false
- EXECNOW: LOG gen_false.c BIN gen_false.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/false.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_false.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_false.out ./tests/e-acsl-runtime/result/gen_false.c
+ EXECNOW: LOG gen_false.c BIN gen_false.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/false.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_false.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_false.out ./tests/e-acsl-runtime/result/gen_false.c && ./tests/e-acsl-runtime/result/gen_false.out
*/
-void main() {
+int main(void) {
int x = 0;
if (x) /*@ assert \false; */ ;
+ return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i b/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
index 36c04c8d72e929034bef6a4aed4c7789c274bb0b..ed63e1f988aaf31a4c2be99a2aa44649e2b2c547 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
@@ -1,12 +1,15 @@
/* run.config
- COMMENT: integer constant
+ COMMENT: integer constant + a stmt after the assertion
COMMENT: waiting for fixing BTS #745
- EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/integer_constant.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_integer_constant.out -lgmp ./tests/e-acsl-runtime/result/gen_integer_constant.c
+ EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/integer_constant.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_integer_constant.out -lgmp ./tests/e-acsl-runtime/result/gen_integer_constant.c && ./tests/e-acsl-runtime/result/gen_integer_constant.out
*/
-void main() {
- /*@ assert 0 == 0; */
+int main(void) {
+ int x;
+ /*@ assert 0 == 0; */ x = 0;
/*@ assert 0 != 1; */
/*@ assert 0xfffffffffffffff == 0xfffffffffffffff; */
/* /\*@ assert 0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff; *\/ */
+
+ return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/not.i b/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
index a0a15273c626c1478210c494d5e892950c6ef9de..452dd89b8e894bad1adeca5f5dd4b80c2f9a6d18 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
@@ -1,9 +1,10 @@
/* run.config
COMMENT: predicate [!p]
- EXECNOW: LOG gen_not.c BIN gen_not.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/not.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_not.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_not.out ./tests/e-acsl-runtime/result/gen_not.c
+ EXECNOW: LOG gen_not.c BIN gen_not.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/not.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_not.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_not.out ./tests/e-acsl-runtime/result/gen_not.c && ./tests/e-acsl-runtime/result/gen_not.out
*/
-void main() {
+int main(void) {
int x = 0;
/*@ assert ! x; */
if (x) /*@ assert x; */ ;
+ return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
index cd7e49c7811302bca21a4466bf86fc21d56c8347..f5299d613e3215ab39503336f464d4ec95178b3a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
@@ -2,13 +2,14 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE.i:121:[value] Assertion got status valid.
+PROJECT_FILE.i:122:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[dominators] computing for function main
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
+ __retres ∈ {0}
x ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
@@ -24,13 +25,15 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
int x;
x = 0;
/*@ assert &x ≡ &x; */ ;
- if (& x != & x) { e_acsl_fail((char *)"(&x == &x)"); }
- return;
+ if (! (& x == & x)) { e_acsl_fail((char *)"(&x == &x)"); }
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index 7e82bcd2f2f0b6ba88aa7993fca1c60d43508105..29c479093c4afd62dae6b494153f1df815a24f58 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -2,30 +2,30 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE.i:123:[value] Assertion got status valid.
+PROJECT_FILE.i:124:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:125.
+ Called from PROJECT_FILE.i:126.
PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:125.
+ Called from PROJECT_FILE.i:126.
PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:126.
+ Called from PROJECT_FILE.i:127.
PROJECT_FILE.i:55:[value] Function mpz_neg: precondition got status valid
PROJECT_FILE.i:56:[value] Function mpz_neg: precondition got status valid
[value] Done for function mpz_neg
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:126.
+ Called from PROJECT_FILE.i:127.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:127.
+ Called from PROJECT_FILE.i:128.
PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:128.
+ Called from PROJECT_FILE.i:129.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -36,33 +36,33 @@ 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:128.
+ Called from PROJECT_FILE.i:130.
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:129.
+ Called from PROJECT_FILE.i:130.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:129.
+ Called from PROJECT_FILE.i:130.
[value] Done for function mpz_clear
-PROJECT_FILE.i:132:[value] Assertion got status valid.
+PROJECT_FILE.i:133:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:134.
+ Called from PROJECT_FILE.i:135.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:134.
+ Called from PROJECT_FILE.i:135.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:135.
+ Called from PROJECT_FILE.i:136.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:135.
+ Called from PROJECT_FILE.i:136.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:136.
+ Called from PROJECT_FILE.i:137.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:137.
+ Called from PROJECT_FILE.i:138.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -72,33 +72,33 @@ PROJECT_FILE.i:132:[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:137.
+ Called from PROJECT_FILE.i:139.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:138.
+ Called from PROJECT_FILE.i:139.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:138.
+ Called from PROJECT_FILE.i:139.
[value] Done for function mpz_clear
-PROJECT_FILE.i:141:[value] Assertion got status valid.
+PROJECT_FILE.i:142:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:143.
+ Called from PROJECT_FILE.i:144.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:143.
+ Called from PROJECT_FILE.i:144.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:144.
+ Called from PROJECT_FILE.i:145.
[value] Done for function mpz_init
[value] computing for function mpz_com <- main.
- Called from PROJECT_FILE.i:144.
+ Called from PROJECT_FILE.i:145.
[kernel] warning: No code for function mpz_com, default assigns generated
[value] Done for function mpz_com
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:145.
+ Called from PROJECT_FILE.i:146.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:146.
+ Called from PROJECT_FILE.i:147.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -108,44 +108,44 @@ PROJECT_FILE.i:141:[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:146.
+ Called from PROJECT_FILE.i:148.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:147.
+ Called from PROJECT_FILE.i:148.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:147.
+ Called from PROJECT_FILE.i:148.
[value] Done for function mpz_clear
-PROJECT_FILE.i:150:[value] Assertion got status valid.
+PROJECT_FILE.i:151:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:152.
+ Called from PROJECT_FILE.i:153.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:153.
+ Called from PROJECT_FILE.i:154.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:153.
+ Called from PROJECT_FILE.i:154.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:154.
+ Called from PROJECT_FILE.i:155.
PROJECT_FILE.i:60:[value] Function mpz_add: precondition got status valid
PROJECT_FILE.i:61:[value] Function mpz_add: precondition got status valid
PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
[value] Done for function mpz_add
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:154.
+ Called from PROJECT_FILE.i:155.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:155.
+ Called from PROJECT_FILE.i:156.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:155.
+ Called from PROJECT_FILE.i:156.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:156.
+ Called from PROJECT_FILE.i:157.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:157.
+ Called from PROJECT_FILE.i:158.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -155,50 +155,50 @@ PROJECT_FILE.i:62:[value] Function mpz_add: precondition 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:157.
+ Called from PROJECT_FILE.i:159.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:158.
+ Called from PROJECT_FILE.i:159.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:158.
+ Called from PROJECT_FILE.i:159.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:158.
+ Called from PROJECT_FILE.i:160.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:159.
+ Called from PROJECT_FILE.i:160.
[value] Done for function mpz_clear
-PROJECT_FILE.i:162:[value] Assertion got status valid.
+PROJECT_FILE.i:163:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:164.
+ Called from PROJECT_FILE.i:165.
[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:166.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:165.
+ Called from PROJECT_FILE.i:166.
[value] Done for function mpz_init
[value] computing for function mpz_sub <- main.
- Called from PROJECT_FILE.i:166.
+ Called from PROJECT_FILE.i:167.
PROJECT_FILE.i:66:[value] Function mpz_sub: precondition got status valid
PROJECT_FILE.i:67:[value] Function mpz_sub: precondition got status valid
PROJECT_FILE.i:68:[value] Function mpz_sub: precondition got status valid
[value] Done for function mpz_sub
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:166.
+ Called from PROJECT_FILE.i:167.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:167.
+ Called from PROJECT_FILE.i:168.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:167.
+ Called from PROJECT_FILE.i:168.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:168.
+ Called from PROJECT_FILE.i:169.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:169.
+ Called from PROJECT_FILE.i:170.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -208,50 +208,50 @@ PROJECT_FILE.i:68:[value] Function mpz_sub: precondition 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:169.
+ Called from PROJECT_FILE.i:171.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:170.
+ Called from PROJECT_FILE.i:171.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:170.
+ Called from PROJECT_FILE.i:171.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:170.
+ Called from PROJECT_FILE.i:172.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:171.
+ Called from PROJECT_FILE.i:172.
[value] Done for function mpz_clear
-PROJECT_FILE.i:174:[value] Assertion got status valid.
+PROJECT_FILE.i:175:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:176.
+ Called from PROJECT_FILE.i:177.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:177.
+ Called from PROJECT_FILE.i:178.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:177.
+ Called from PROJECT_FILE.i:178.
[value] Done for function mpz_init
[value] computing for function mpz_mul <- main.
- Called from PROJECT_FILE.i:178.
+ Called from PROJECT_FILE.i:179.
PROJECT_FILE.i:72:[value] Function mpz_mul: precondition got status valid
PROJECT_FILE.i:73:[value] Function mpz_mul: precondition got status valid
PROJECT_FILE.i:74:[value] Function mpz_mul: precondition got status valid
[value] Done for function mpz_mul
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:178.
+ Called from PROJECT_FILE.i:179.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:179.
+ Called from PROJECT_FILE.i:180.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:179.
+ Called from PROJECT_FILE.i:180.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:180.
+ Called from PROJECT_FILE.i:181.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:181.
+ Called from PROJECT_FILE.i:182.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -261,43 +261,43 @@ PROJECT_FILE.i:74:[value] Function mpz_mul: precondition 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:181.
+ Called from PROJECT_FILE.i:183.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:182.
+ Called from PROJECT_FILE.i:183.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:182.
+ Called from PROJECT_FILE.i:183.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:182.
+ Called from PROJECT_FILE.i:184.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:183.
+ Called from PROJECT_FILE.i:184.
[value] Done for function mpz_clear
-PROJECT_FILE.i:186:[value] Assertion got status valid.
+PROJECT_FILE.i:187:[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:190.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:189.
+ 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:190.
+ Called from PROJECT_FILE.i:191.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_ui <- main.
- Called from PROJECT_FILE.i:190.
+ Called from PROJECT_FILE.i:191.
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:191.
+ Called from PROJECT_FILE.i:192.
[value] Done for function mpz_cmp
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:191.
+ Called from PROJECT_FILE.i:192.
[value] Done for function mpz_init
-PROJECT_FILE.i:192:[value] Assertion got status valid.
+PROJECT_FILE.i:193:[value] Assertion got status valid.
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:193.
+ Called from PROJECT_FILE.i:194.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -307,25 +307,25 @@ PROJECT_FILE.i:192:[value] Assertion got status valid.
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_cdiv_q <- main.
- Called from PROJECT_FILE.i:194.
+ Called from PROJECT_FILE.i:195.
PROJECT_FILE.i:78:[value] Function mpz_cdiv_q: precondition got status valid
PROJECT_FILE.i:79:[value] Function mpz_cdiv_q: precondition got status valid
PROJECT_FILE.i:80:[value] Function mpz_cdiv_q: precondition got status valid
[value] Done for function mpz_cdiv_q
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:194.
+ Called from PROJECT_FILE.i:195.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:195.
+ Called from PROJECT_FILE.i:196.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:195.
+ Called from PROJECT_FILE.i:196.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:196.
+ Called from PROJECT_FILE.i:197.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:197.
+ Called from PROJECT_FILE.i:198.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -335,48 +335,48 @@ PROJECT_FILE.i:80:[value] Function mpz_cdiv_q: precondition 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:197.
+ Called from PROJECT_FILE.i:199.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:198.
+ Called from PROJECT_FILE.i:199.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:198.
+ Called from PROJECT_FILE.i:199.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:198.
+ Called from PROJECT_FILE.i:200.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:199.
+ Called from PROJECT_FILE.i:200.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:199.
+ Called from PROJECT_FILE.i:200.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:199.
+ Called from PROJECT_FILE.i:201.
[value] Done for function mpz_clear
-PROJECT_FILE.i:202:[value] Assertion got status valid.
+PROJECT_FILE.i:204:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:205.
+ Called from PROJECT_FILE.i:207.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:205.
+ Called from PROJECT_FILE.i:207.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:206.
+ Called from PROJECT_FILE.i:208.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_ui <- main.
- Called from PROJECT_FILE.i:206.
+ Called from PROJECT_FILE.i:208.
[value] Done for function mpz_init_set_ui
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:207.
+ Called from PROJECT_FILE.i:209.
[value] Done for function mpz_cmp
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:207.
+ Called from PROJECT_FILE.i:209.
[value] Done for function mpz_init
-PROJECT_FILE.i:208:[value] Assertion got status valid.
+PROJECT_FILE.i:210:[value] Assertion got status valid.
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:209.
+ Called from PROJECT_FILE.i:211.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -385,26 +385,24 @@ PROJECT_FILE.i:208:[value] Assertion got status valid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
-[value] computing for function mpz_mod <- main.
- Called from PROJECT_FILE.i:210.
-PROJECT_FILE.i:84:[value] Function mpz_mod: precondition got status valid
-PROJECT_FILE.i:85:[value] Function mpz_mod: precondition got status valid
-PROJECT_FILE.i:86:[value] Function mpz_mod: precondition got status valid
-[value] Done for function mpz_mod
+[value] computing for function mpz_mod_ui <- main.
+ Called from PROJECT_FILE.i:212.
+[kernel] warning: No code for function mpz_mod_ui, default assigns generated
+[value] Done for function mpz_mod_ui
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:210.
+ Called from PROJECT_FILE.i:212.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:211.
+ Called from PROJECT_FILE.i:213.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:211.
+ Called from PROJECT_FILE.i:213.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:212.
+ Called from PROJECT_FILE.i:214.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:213.
+ Called from PROJECT_FILE.i:215.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -414,98 +412,98 @@ PROJECT_FILE.i:86:[value] Function mpz_mod: precondition 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:213.
+ Called from PROJECT_FILE.i:216.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:214.
+ Called from PROJECT_FILE.i:216.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:214.
+ Called from PROJECT_FILE.i:216.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:214.
+ Called from PROJECT_FILE.i:217.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:215.
+ Called from PROJECT_FILE.i:217.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:215.
+ Called from PROJECT_FILE.i:217.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:215.
+ Called from PROJECT_FILE.i:218.
[value] Done for function mpz_clear
-PROJECT_FILE.i:218:[value] Assertion got status valid.
+PROJECT_FILE.i:221:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:223.
+ Called from PROJECT_FILE.i:226.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:223.
+ Called from PROJECT_FILE.i:226.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:224.
+ Called from PROJECT_FILE.i:227.
[value] Done for function mpz_init
[value] computing for function mpz_mul <- main.
- Called from PROJECT_FILE.i:224.
+ Called from PROJECT_FILE.i:227.
[value] Done for function mpz_mul
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:225.
+ Called from PROJECT_FILE.i:228.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:225.
+ Called from PROJECT_FILE.i:228.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:226.
+ Called from PROJECT_FILE.i:229.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:226.
+ Called from PROJECT_FILE.i:229.
[value] Done for function mpz_add
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:227.
+ Called from PROJECT_FILE.i:230.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:227.
+ Called from PROJECT_FILE.i:230.
[value] Done for function mpz_add
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:228.
+ Called from PROJECT_FILE.i:231.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:228.
+ Called from PROJECT_FILE.i:231.
[value] Done for function mpz_init
[value] computing for function mpz_sub <- main.
- Called from PROJECT_FILE.i:229.
+ Called from PROJECT_FILE.i:232.
[value] Done for function mpz_sub
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:229.
+ Called from PROJECT_FILE.i:232.
[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:233.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:230.
+ Called from PROJECT_FILE.i:233.
[value] Done for function mpz_init
[value] computing for function mpz_sub <- main.
- Called from PROJECT_FILE.i:231.
+ Called from PROJECT_FILE.i:234.
[value] Done for function mpz_sub
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:231.
+ Called from PROJECT_FILE.i:234.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:232.
+ Called from PROJECT_FILE.i:235.
[value] Done for function mpz_add
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:232.
+ Called from PROJECT_FILE.i:235.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:233.
+ Called from PROJECT_FILE.i:236.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:233.
+ Called from PROJECT_FILE.i:236.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:234.
+ Called from PROJECT_FILE.i:237.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:235.
+ Called from PROJECT_FILE.i:238.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -515,71 +513,71 @@ PROJECT_FILE.i:218:[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:236.
+ Called from PROJECT_FILE.i:239.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:236.
+ Called from PROJECT_FILE.i:239.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:236.
+ Called from PROJECT_FILE.i:239.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:237.
+ Called from PROJECT_FILE.i:240.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:237.
+ Called from PROJECT_FILE.i:240.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:237.
+ Called from PROJECT_FILE.i:240.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:238.
+ Called from PROJECT_FILE.i:241.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:238.
+ Called from PROJECT_FILE.i:241.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:238.
+ Called from PROJECT_FILE.i:241.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:239.
+ Called from PROJECT_FILE.i:242.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:239.
+ Called from PROJECT_FILE.i:242.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:239.
+ Called from PROJECT_FILE.i:242.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:240.
+ Called from PROJECT_FILE.i:243.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:240.
+ Called from PROJECT_FILE.i:243.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:240.
+ Called from PROJECT_FILE.i:243.
[value] Done for function mpz_clear
-PROJECT_FILE.i:243:[value] Assertion got status valid.
+PROJECT_FILE.i:246:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:245.
+ Called from PROJECT_FILE.i:248.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:246.
+ Called from PROJECT_FILE.i:249.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:246.
+ Called from PROJECT_FILE.i:249.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:247.
+ Called from PROJECT_FILE.i:250.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:247.
+ Called from PROJECT_FILE.i:250.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:248.
+ Called from PROJECT_FILE.i:251.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:250.
+ 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
@@ -589,44 +587,44 @@ PROJECT_FILE.i:243:[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:251.
+ Called from PROJECT_FILE.i:254.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:251.
+ Called from PROJECT_FILE.i:254.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:251.
+ Called from PROJECT_FILE.i:254.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:252.
+ Called from PROJECT_FILE.i:255.
[value] Done for function mpz_clear
-PROJECT_FILE.i:255:[value] Assertion got status valid.
+PROJECT_FILE.i:258:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:258.
+ 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:258.
+ Called from PROJECT_FILE.i:261.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:259.
+ Called from PROJECT_FILE.i:262.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:259.
+ Called from PROJECT_FILE.i:262.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:260.
+ Called from PROJECT_FILE.i:263.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:260.
+ Called from PROJECT_FILE.i:263.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:261.
+ Called from PROJECT_FILE.i:264.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:261.
+ Called from PROJECT_FILE.i:264.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:263.
+ Called from PROJECT_FILE.i:266.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -636,47 +634,47 @@ PROJECT_FILE.i:255:[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:264.
+ Called from PROJECT_FILE.i:267.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:264.
+ Called from PROJECT_FILE.i:267.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:264.
+ Called from PROJECT_FILE.i:267.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:265.
+ Called from PROJECT_FILE.i:268.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:265.
+ Called from PROJECT_FILE.i:268.
[value] Done for function mpz_clear
-PROJECT_FILE.i:268:[value] Assertion got status valid.
+PROJECT_FILE.i:271:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:271.
+ 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:271.
+ Called from PROJECT_FILE.i:274.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:272.
+ Called from PROJECT_FILE.i:275.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:272.
+ Called from PROJECT_FILE.i:275.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:273.
+ Called from PROJECT_FILE.i:276.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:273.
+ Called from PROJECT_FILE.i:276.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:274.
+ Called from PROJECT_FILE.i:277.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:274.
+ Called from PROJECT_FILE.i:277.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:276.
+ Called from PROJECT_FILE.i:279.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -686,41 +684,41 @@ PROJECT_FILE.i:268:[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:277.
+ Called from PROJECT_FILE.i:280.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:277.
+ Called from PROJECT_FILE.i:280.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:277.
+ Called from PROJECT_FILE.i:280.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:278.
+ Called from PROJECT_FILE.i:281.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:278.
+ Called from PROJECT_FILE.i:281.
[value] Done for function mpz_clear
-PROJECT_FILE.i:281:[value] Assertion got status valid.
+PROJECT_FILE.i:284:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:283.
+ Called from PROJECT_FILE.i:286.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:284.
+ Called from PROJECT_FILE.i:287.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:284.
+ Called from PROJECT_FILE.i:287.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:285.
+ Called from PROJECT_FILE.i:288.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:285.
+ Called from PROJECT_FILE.i:288.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:286.
+ Called from PROJECT_FILE.i:289.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:288.
+ Called from PROJECT_FILE.i:291.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -730,16 +728,16 @@ PROJECT_FILE.i:281:[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:289.
+ Called from PROJECT_FILE.i:292.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:289.
+ Called from PROJECT_FILE.i:292.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:289.
+ Called from PROJECT_FILE.i:292.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:290.
+ Called from PROJECT_FILE.i:293.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
@@ -773,14 +771,15 @@ PROJECT_FILE.i:115:[from] Non terminating function (no dependencies)
[from] Done for function mpz_init_set_ui
[from] Computing for function mpz_cdiv_q
[from] Done for function mpz_cdiv_q
-[from] Computing for function mpz_mod
-[from] Done for function mpz_mod
+[from] Computing for function mpz_mod_ui
+[from] Done for function mpz_mod_ui
[dominators] computing for function main
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
[value] Values for function main:
+ __retres ∈ {0}
x ∈ {-3}
y ∈ {2}
/* Generated by Frama-C */
@@ -845,14 +844,6 @@ extern void mpz_mul(__mpz_struct * /*[1]*/ z1,
extern void mpz_cdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
-/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
- assigns *z1;
-*/
-extern void mpz_mod(__mpz_struct * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2,
- __mpz_struct const * /*[1]*/ z3);
/*@ terminates \false;
ensures \false;
assigns \nothing; */
@@ -869,8 +860,12 @@ void e_acsl_fail(char *msg)
/*@ behavior generated:
assigns \at(\result,Post) \from \nothing; */
extern int ( /* missing proto */ mpz_com)();
-void main(void)
+/*@ behavior generated:
+ assigns \at(\result,Post) \from \nothing; */
+extern int ( /* missing proto */ mpz_mod_ui)();
+int main(void)
{
+ int __retres;
int x;
int y;
x = -3;
@@ -883,7 +878,7 @@ void main(void)
mpz_init_set_si((__mpz_struct *)(e_acsl_3),(long)x);
e_acsl_4 = mpz_cmp((__mpz_struct const *)(e_acsl_2),
(__mpz_struct const *)(e_acsl_3));
- if (e_acsl_4 != 0) { e_acsl_fail((char *)"(-3 == x)"); }
+ if (! (e_acsl_4 == 0)) { e_acsl_fail((char *)"(-3 == x)"); }
mpz_clear((__mpz_struct *)(e_acsl_1));
mpz_clear((__mpz_struct *)(e_acsl_2));
mpz_clear((__mpz_struct *)(e_acsl_3));
@@ -897,7 +892,7 @@ void main(void)
mpz_neg((__mpz_struct *)(e_acsl_7),(__mpz_struct const *)(e_acsl_6));
e_acsl_8 = mpz_cmp((__mpz_struct const *)(e_acsl_5),
(__mpz_struct const *)(e_acsl_7));
- if (e_acsl_8 != 0) { e_acsl_fail((char *)"(x == -3)"); }
+ if (! (e_acsl_8 == 0)) { e_acsl_fail((char *)"(x == -3)"); }
mpz_clear((__mpz_struct *)(e_acsl_5));
mpz_clear((__mpz_struct *)(e_acsl_6));
mpz_clear((__mpz_struct *)(e_acsl_7));
@@ -910,7 +905,7 @@ void main(void)
mpz_init((__mpz_struct *)(e_acsl_11)); mpz_com(e_acsl_11,e_acsl_10);
e_acsl_12 = mpz_cmp((__mpz_struct const *)(e_acsl_9),
(__mpz_struct const *)(e_acsl_11));
- if (e_acsl_12 == 0) { e_acsl_fail((char *)"(0 != ~0)"); }
+ if (! (e_acsl_12 != 0)) { e_acsl_fail((char *)"(0 != ~0)"); }
mpz_clear((__mpz_struct *)(e_acsl_9));
mpz_clear((__mpz_struct *)(e_acsl_10));
mpz_clear((__mpz_struct *)(e_acsl_11));
@@ -929,7 +924,7 @@ void main(void)
mpz_neg((__mpz_struct *)(e_acsl_17),(__mpz_struct const *)(e_acsl_16));
e_acsl_18 = mpz_cmp((__mpz_struct const *)(e_acsl_15),
(__mpz_struct const *)(e_acsl_17));
- if (e_acsl_18 != 0) { e_acsl_fail((char *)"(x+1 == -2)"); }
+ if (! (e_acsl_18 == 0)) { e_acsl_fail((char *)"(x+1 == -2)"); }
mpz_clear((__mpz_struct *)(e_acsl_13));
mpz_clear((__mpz_struct *)(e_acsl_14));
mpz_clear((__mpz_struct *)(e_acsl_15));
@@ -950,7 +945,7 @@ void main(void)
mpz_neg((__mpz_struct *)(e_acsl_23),(__mpz_struct const *)(e_acsl_22));
e_acsl_24 = mpz_cmp((__mpz_struct const *)(e_acsl_21),
(__mpz_struct const *)(e_acsl_23));
- if (e_acsl_24 != 0) { e_acsl_fail((char *)"(x-1 == -4)"); }
+ if (! (e_acsl_24 == 0)) { e_acsl_fail((char *)"(x-1 == -4)"); }
mpz_clear((__mpz_struct *)(e_acsl_19));
mpz_clear((__mpz_struct *)(e_acsl_20));
mpz_clear((__mpz_struct *)(e_acsl_21));
@@ -971,7 +966,7 @@ void main(void)
mpz_neg((__mpz_struct *)(e_acsl_29),(__mpz_struct const *)(e_acsl_28));
e_acsl_30 = mpz_cmp((__mpz_struct const *)(e_acsl_27),
(__mpz_struct const *)(e_acsl_29));
- if (e_acsl_30 != 0) { e_acsl_fail((char *)"(x*3 == -9)"); }
+ if (! (e_acsl_30 == 0)) { e_acsl_fail((char *)"(x*3 == -9)"); }
mpz_clear((__mpz_struct *)(e_acsl_25));
mpz_clear((__mpz_struct *)(e_acsl_26));
mpz_clear((__mpz_struct *)(e_acsl_27));
@@ -997,7 +992,7 @@ void main(void)
mpz_neg((__mpz_struct *)(e_acsl_38),(__mpz_struct const *)(e_acsl_37));
e_acsl_39 = mpz_cmp((__mpz_struct const *)(e_acsl_36),
(__mpz_struct const *)(e_acsl_38));
- if (e_acsl_39 != 0) { e_acsl_fail((char *)"(x/3 == -1)"); }
+ if (! (e_acsl_39 == 0)) { e_acsl_fail((char *)"(x/3 == -1)"); }
mpz_clear((__mpz_struct *)(e_acsl_31));
mpz_clear((__mpz_struct *)(e_acsl_32));
mpz_clear((__mpz_struct *)(e_acsl_33));
@@ -1018,14 +1013,13 @@ void main(void)
(__mpz_struct const *)(e_acsl_43));
mpz_init((__mpz_struct *)(e_acsl_45)); /*@ assert 2 ≢ 0U; */ ;
if (e_acsl_44 == 0) { e_acsl_fail((char *)"(2 == 0U)"); }
- mpz_mod((__mpz_struct *)(e_acsl_45),(__mpz_struct const *)(e_acsl_40),
- (__mpz_struct const *)(e_acsl_41));
+ mpz_mod_ui(e_acsl_45,e_acsl_40,e_acsl_41);
mpz_init_set_si((__mpz_struct *)(e_acsl_46),(long)1);
mpz_init((__mpz_struct *)(e_acsl_47));
mpz_neg((__mpz_struct *)(e_acsl_47),(__mpz_struct const *)(e_acsl_46));
e_acsl_48 = mpz_cmp((__mpz_struct const *)(e_acsl_45),
(__mpz_struct const *)(e_acsl_47));
- if (e_acsl_48 != 0) { e_acsl_fail((char *)"(x%2 == -1)"); }
+ if (! (e_acsl_48 == 0)) { e_acsl_fail((char *)"(x%2 == -1)"); }
mpz_clear((__mpz_struct *)(e_acsl_40));
mpz_clear((__mpz_struct *)(e_acsl_41));
mpz_clear((__mpz_struct *)(e_acsl_42));
@@ -1070,7 +1064,7 @@ void main(void)
mpz_neg((__mpz_struct *)(e_acsl_63),(__mpz_struct const *)(e_acsl_62));
e_acsl_64 = mpz_cmp((__mpz_struct const *)(e_acsl_61),
(__mpz_struct const *)(e_acsl_63));
- if (e_acsl_64 != 0) {
+ if (! (e_acsl_64 == 0)) {
e_acsl_fail((char *)"(((x*2+(3+y))-4)+(x-y) == -10)");
} mpz_clear((__mpz_struct *)(e_acsl_49));
mpz_clear((__mpz_struct *)(e_acsl_50));
@@ -1100,7 +1094,7 @@ void main(void)
mpz_init_set_si((__mpz_struct *)(e_acsl_69),(long)0);
e_acsl_70 = mpz_cmp((__mpz_struct const *)(e_acsl_68),
(__mpz_struct const *)(e_acsl_69));
- if ((e_acsl_67 == 0) != ! (e_acsl_70 == 0)) {
+ if (! ((e_acsl_67 == 0) == ! (e_acsl_70 == 0))) {
e_acsl_fail((char *)"((0==1) == !(0==0))");
} mpz_clear((__mpz_struct *)(e_acsl_65));
mpz_clear((__mpz_struct *)(e_acsl_66));
@@ -1121,7 +1115,7 @@ void main(void)
mpz_init_set_si((__mpz_struct *)(e_acsl_76),(long)0);
e_acsl_77 = mpz_cmp((__mpz_struct const *)(e_acsl_75),
(__mpz_struct const *)(e_acsl_76));
- if ((e_acsl_74 <= 0) != (e_acsl_77 > 0)) {
+ if (! ((e_acsl_74 <= 0) == (e_acsl_77 > 0))) {
e_acsl_fail((char *)"((0<=-1) == (0>0))");
} mpz_clear((__mpz_struct *)(e_acsl_71));
mpz_clear((__mpz_struct *)(e_acsl_72));
@@ -1143,7 +1137,7 @@ void main(void)
mpz_init_set_si((__mpz_struct *)(e_acsl_83),(long)0);
e_acsl_84 = mpz_cmp((__mpz_struct const *)(e_acsl_82),
(__mpz_struct const *)(e_acsl_83));
- if ((e_acsl_81 >= 0) != (e_acsl_84 <= 0)) {
+ if (! ((e_acsl_81 >= 0) == (e_acsl_84 <= 0))) {
e_acsl_fail((char *)"((0>=-1) == (0<=0))");
} mpz_clear((__mpz_struct *)(e_acsl_78));
mpz_clear((__mpz_struct *)(e_acsl_79));
@@ -1163,7 +1157,7 @@ void main(void)
mpz_init_set_si((__mpz_struct *)(e_acsl_89),(long)0);
e_acsl_90 = mpz_cmp((__mpz_struct const *)(e_acsl_88),
(__mpz_struct const *)(e_acsl_89));
- if ((e_acsl_87 != 0) != ! (e_acsl_90 != 0)) {
+ if (! ((e_acsl_87 != 0) == ! (e_acsl_90 != 0))) {
e_acsl_fail((char *)"((0!=1) == !(0!=0))");
} mpz_clear((__mpz_struct *)(e_acsl_85));
mpz_clear((__mpz_struct *)(e_acsl_86));
@@ -1171,7 +1165,8 @@ void main(void)
mpz_clear((__mpz_struct *)(e_acsl_89));
}
- return;
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
index a9df79c33b084bd5d8a3eede2c5ff8e4d7121a6f..56926dd12392cb6357b6be7e201545d163c7f0fc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
@@ -2,14 +2,15 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE.i:123:[value] Assertion got status valid.
-PROJECT_FILE.i:126:[value] Assertion got status valid.
+PROJECT_FILE.i:124:[value] Assertion got status valid.
+PROJECT_FILE.i:127:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[dominators] computing for function main
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
+ __retres ∈ {0}
x ∈ {0}
y ∈ {0}
/* Generated by Frama-C */
@@ -26,17 +27,19 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
long x;
int y;
x = (long)0;
y = 0;
/*@ assert (int)x ≡ y; */ ;
- if ((int)x != y) { e_acsl_fail((char *)"((int)x == y)"); }
+ if (! ((int)x == y)) { e_acsl_fail((char *)"((int)x == y)"); }
/*@ assert x ≡ (long)y; */ ;
- if (x != (long)y) { e_acsl_fail((char *)"(x == (long)y)"); }
- return;
+ if (! (x == (long)y)) { e_acsl_fail((char *)"(x == (long)y)"); }
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index 35578bea611fdf3596f303e499da1ea828e346a4..1dbd4b98860ea4b5c9ff03ff22c36f0ba0883933 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -2,23 +2,23 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE.i:124:[value] Assertion got status valid.
-PROJECT_FILE.i:127:[value] Assertion got status valid.
-PROJECT_FILE.i:130:[value] Assertion got status valid.
+PROJECT_FILE.i:125:[value] Assertion got status valid.
+PROJECT_FILE.i:128:[value] Assertion got status valid.
+PROJECT_FILE.i:131:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:132.
+ Called from PROJECT_FILE.i:133.
PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:132.
+ 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:133.
+ Called from PROJECT_FILE.i:134.
PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:134.
+ Called from PROJECT_FILE.i:135.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -29,24 +29,24 @@ 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:134.
+ 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:135.
+ Called from PROJECT_FILE.i:136.
[value] Done for function mpz_clear
-PROJECT_FILE.i:138:[value] Assertion got status valid.
+PROJECT_FILE.i:139:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:140.
+ Called from PROJECT_FILE.i:141.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:140.
+ Called from PROJECT_FILE.i:141.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:141.
+ Called from PROJECT_FILE.i:142.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:142.
+ Called from PROJECT_FILE.i:143.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -56,25 +56,25 @@ PROJECT_FILE.i:138:[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:142.
+ Called from PROJECT_FILE.i:144.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:143.
+ Called from PROJECT_FILE.i:144.
[value] Done for function mpz_clear
-PROJECT_FILE.i:147:[value] Assertion got status valid.
-PROJECT_FILE.i:150:[value] Assertion got status valid.
-PROJECT_FILE.i:153:[value] Assertion got status valid.
+PROJECT_FILE.i:148:[value] Assertion got status valid.
+PROJECT_FILE.i:151:[value] Assertion got status valid.
+PROJECT_FILE.i:154:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:155.
+ Called from PROJECT_FILE.i:156.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:155.
+ Called from PROJECT_FILE.i:156.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:156.
+ Called from PROJECT_FILE.i:157.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:157.
+ Called from PROJECT_FILE.i:158.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -84,23 +84,23 @@ PROJECT_FILE.i:153:[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:157.
+ Called from PROJECT_FILE.i:158.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:158.
+ Called from PROJECT_FILE.i:159.
[value] Done for function mpz_clear
-PROJECT_FILE.i:161:[value] Assertion got status valid.
+PROJECT_FILE.i:162:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:163.
+ Called from PROJECT_FILE.i:164.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:163.
+ Called from PROJECT_FILE.i:164.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:164.
+ Called from PROJECT_FILE.i:165.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:165.
+ Called from PROJECT_FILE.i:166.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -110,23 +110,23 @@ PROJECT_FILE.i:161:[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:165.
+ Called from PROJECT_FILE.i:166.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:166.
+ Called from PROJECT_FILE.i:167.
[value] Done for function mpz_clear
-PROJECT_FILE.i:169:[value] Assertion got status valid.
+PROJECT_FILE.i:170:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:171.
+ Called from PROJECT_FILE.i:172.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:171.
+ Called from PROJECT_FILE.i:172.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:172.
+ Called from PROJECT_FILE.i:173.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:173.
+ Called from PROJECT_FILE.i:174.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -136,23 +136,23 @@ PROJECT_FILE.i:169:[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:173.
+ Called from PROJECT_FILE.i:175.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:174.
+ Called from PROJECT_FILE.i:175.
[value] Done for function mpz_clear
-PROJECT_FILE.i:177:[value] Assertion got status valid.
+PROJECT_FILE.i:178:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:179.
+ Called from PROJECT_FILE.i:180.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:179.
+ Called from PROJECT_FILE.i:180.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:180.
+ Called from PROJECT_FILE.i:181.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:181.
+ Called from PROJECT_FILE.i:182.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -162,23 +162,23 @@ PROJECT_FILE.i:177:[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:181.
+ Called from PROJECT_FILE.i:183.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:182.
+ Called from PROJECT_FILE.i:183.
[value] Done for function mpz_clear
-PROJECT_FILE.i:185:[value] Assertion got status valid.
+PROJECT_FILE.i:186:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:187.
+ Called from PROJECT_FILE.i:188.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:187.
+ Called from PROJECT_FILE.i:188.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:188.
+ Called from PROJECT_FILE.i:189.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:189.
+ Called from PROJECT_FILE.i:190.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -188,23 +188,23 @@ PROJECT_FILE.i:185:[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:190.
+ Called from PROJECT_FILE.i:191.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:190.
+ Called from PROJECT_FILE.i:191.
[value] Done for function mpz_clear
-PROJECT_FILE.i:193:[value] Assertion got status valid.
+PROJECT_FILE.i:194:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:195.
+ Called from PROJECT_FILE.i:196.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:195.
+ Called from PROJECT_FILE.i:196.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:196.
+ Called from PROJECT_FILE.i:197.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:197.
+ Called from PROJECT_FILE.i:198.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -214,10 +214,10 @@ PROJECT_FILE.i:193:[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:197.
+ Called from PROJECT_FILE.i:199.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:198.
+ Called from PROJECT_FILE.i:199.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
@@ -241,6 +241,7 @@ PROJECT_FILE.i:115:[from] Non terminating function (no dependencies)
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
[value] Values for function main:
+ __retres ∈ {0}
x ∈ {0}
y ∈ {1}
s ∈ {{ &"toto" }}
@@ -276,24 +277,25 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
int x;
int y;
char *s;
x = 0;
y = 1;
/*@ assert x < y; */ ;
- if (x >= y) { e_acsl_fail((char *)"(x < y)"); }
+ if (! (x < y)) { e_acsl_fail((char *)"(x < y)"); }
/*@ assert y > x; */ ;
- if (y <= x) { e_acsl_fail((char *)"(y > x)"); }
+ if (! (y > x)) { e_acsl_fail((char *)"(y > x)"); }
/*@ assert x ≤ 0; */ ;
{ mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3;
mpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)x);
mpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
e_acsl_3 = mpz_cmp((__mpz_struct const *)(e_acsl_1),
(__mpz_struct const *)(e_acsl_2));
- if (e_acsl_3 > 0) { e_acsl_fail((char *)"(x <= 0)"); }
+ if (! (e_acsl_3 <= 0)) { e_acsl_fail((char *)"(x <= 0)"); }
mpz_clear((__mpz_struct *)(e_acsl_1));
mpz_clear((__mpz_struct *)(e_acsl_2));
}
@@ -304,23 +306,24 @@ void main(void)
mpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)1);
e_acsl_6 = mpz_cmp((__mpz_struct const *)(e_acsl_4),
(__mpz_struct const *)(e_acsl_5));
- if (e_acsl_6 < 0) { e_acsl_fail((char *)"(y >= 1)"); }
+ if (! (e_acsl_6 >= 0)) { e_acsl_fail((char *)"(y >= 1)"); }
mpz_clear((__mpz_struct *)(e_acsl_4));
mpz_clear((__mpz_struct *)(e_acsl_5));
}
s = (char *)"toto";
/*@ assert s ≡ s; */ ;
- if (s != s) { e_acsl_fail((char *)"(s == s)"); }
+ if (! (s == s)) { e_acsl_fail((char *)"(s == s)"); }
/*@ assert "toto" ≢ "titi"; */ ;
- if ("toto" == "titi") { e_acsl_fail((char *)"(\"toto\" != \"titi\")"); }
+ if (! ("toto" != "titi")) { e_acsl_fail((char *)"(\"toto\" != \"titi\")");
+ }
/*@ assert 5 < 18; */ ;
{ mpz_t e_acsl_7; mpz_t e_acsl_8; int e_acsl_9;
mpz_init_set_si((__mpz_struct *)(e_acsl_7),(long)5);
mpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)18);
e_acsl_9 = mpz_cmp((__mpz_struct const *)(e_acsl_7),
(__mpz_struct const *)(e_acsl_8));
- if (e_acsl_9 >= 0) { e_acsl_fail((char *)"(5 < 18)"); }
+ if (! (e_acsl_9 < 0)) { e_acsl_fail((char *)"(5 < 18)"); }
mpz_clear((__mpz_struct *)(e_acsl_7));
mpz_clear((__mpz_struct *)(e_acsl_8));
}
@@ -331,7 +334,7 @@ void main(void)
mpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)3);
e_acsl_12 = mpz_cmp((__mpz_struct const *)(e_acsl_10),
(__mpz_struct const *)(e_acsl_11));
- if (e_acsl_12 <= 0) { e_acsl_fail((char *)"(32 > 3)"); }
+ if (! (e_acsl_12 > 0)) { e_acsl_fail((char *)"(32 > 3)"); }
mpz_clear((__mpz_struct *)(e_acsl_10));
mpz_clear((__mpz_struct *)(e_acsl_11));
}
@@ -342,7 +345,7 @@ void main(void)
mpz_init_set_si((__mpz_struct *)(e_acsl_14),(long)13);
e_acsl_15 = mpz_cmp((__mpz_struct const *)(e_acsl_13),
(__mpz_struct const *)(e_acsl_14));
- if (e_acsl_15 > 0) { e_acsl_fail((char *)"(12 <= 13)"); }
+ if (! (e_acsl_15 <= 0)) { e_acsl_fail((char *)"(12 <= 13)"); }
mpz_clear((__mpz_struct *)(e_acsl_13));
mpz_clear((__mpz_struct *)(e_acsl_14));
}
@@ -353,7 +356,7 @@ void main(void)
mpz_init_set_si((__mpz_struct *)(e_acsl_17),(long)12);
e_acsl_18 = mpz_cmp((__mpz_struct const *)(e_acsl_16),
(__mpz_struct const *)(e_acsl_17));
- if (e_acsl_18 < 0) { e_acsl_fail((char *)"(123 >= 12)"); }
+ if (! (e_acsl_18 >= 0)) { e_acsl_fail((char *)"(123 >= 12)"); }
mpz_clear((__mpz_struct *)(e_acsl_16));
mpz_clear((__mpz_struct *)(e_acsl_17));
}
@@ -364,7 +367,7 @@ void main(void)
mpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)0xff);
e_acsl_21 = mpz_cmp((__mpz_struct const *)(e_acsl_19),
(__mpz_struct const *)(e_acsl_20));
- if (e_acsl_21 != 0) { e_acsl_fail((char *)"(0xff == 0xff)"); }
+ if (! (e_acsl_21 == 0)) { e_acsl_fail((char *)"(0xff == 0xff)"); }
mpz_clear((__mpz_struct *)(e_acsl_19));
mpz_clear((__mpz_struct *)(e_acsl_20));
}
@@ -375,12 +378,13 @@ void main(void)
mpz_init_set_si((__mpz_struct *)(e_acsl_23),(long)2);
e_acsl_24 = mpz_cmp((__mpz_struct const *)(e_acsl_22),
(__mpz_struct const *)(e_acsl_23));
- if (e_acsl_24 == 0) { e_acsl_fail((char *)"(1 != 2)"); }
+ if (! (e_acsl_24 != 0)) { e_acsl_fail((char *)"(1 != 2)"); }
mpz_clear((__mpz_struct *)(e_acsl_22));
mpz_clear((__mpz_struct *)(e_acsl_23));
}
- return;
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
index c5f2cb13791a556fc5d0149105fa391335d213cd..b08ec2010033d4ad68c82dc24e3eb38d143497b8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
@@ -8,6 +8,7 @@
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
+ __retres ∈ {0}
x ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
@@ -23,12 +24,14 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
int x;
x = 0;
if (x) { /*@ assert \false; */ ; e_acsl_fail((char *)"(\\false)"); }
- return;
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
index 3c082becf863e1abcfbf59dfffc1f24987e41458..b390c68ee8b09254d1b3d589cf1f84532d3689a6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
@@ -549,13 +549,15 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
int x;
x = 0;
/*@ assert &x ≡ &x; */ ;
- if (& x != & x) { e_acsl_fail((char *)"(&x == &x)"); }
- return;
+ if (! (& x == & x)) { e_acsl_fail((char *)"(&x == &x)"); }
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
index 9b38858edcd80985abc4d3c08e4f20fb92d0b20e..b113dc2a124275384ddaae7f8ef954d14d509355 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
@@ -51,6 +51,7 @@ extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2) __attribute__((
__pure__));
extern void __gmpz_com(mpz_ptr, mpz_srcptr);
+extern unsigned long __gmpz_fdiv_r_ui(mpz_ptr, mpz_srcptr, unsigned long);
__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z) __attribute__((
__pure__));
__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z) __attribute__((
@@ -76,14 +77,6 @@ extern void __gmpz_init_set_ui(__mpz_struct * /*[1]*/ z, unsigned long n);
requires \valid(z3);
assigns *z1;
*/
-extern void __gmpz_mod(__mpz_struct * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2,
- __mpz_struct const * /*[1]*/ z3);
-/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
- assigns *z1;
-*/
extern void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -609,8 +602,9 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
int x;
int y;
x = -3;
@@ -623,7 +617,7 @@ void main(void)
__gmpz_init_set_si((__mpz_struct *)(e_acsl_3),(long)x);
e_acsl_4 = __gmpz_cmp((__mpz_struct const *)(e_acsl_2),
(__mpz_struct const *)(e_acsl_3));
- if (e_acsl_4 != 0) { e_acsl_fail((char *)"(-3 == x)"); }
+ if (! (e_acsl_4 == 0)) { e_acsl_fail((char *)"(-3 == x)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_1));
__gmpz_clear((__mpz_struct *)(e_acsl_2));
__gmpz_clear((__mpz_struct *)(e_acsl_3));
@@ -637,7 +631,7 @@ void main(void)
__gmpz_neg((__mpz_struct *)(e_acsl_7),(__mpz_struct const *)(e_acsl_6));
e_acsl_8 = __gmpz_cmp((__mpz_struct const *)(e_acsl_5),
(__mpz_struct const *)(e_acsl_7));
- if (e_acsl_8 != 0) { e_acsl_fail((char *)"(x == -3)"); }
+ if (! (e_acsl_8 == 0)) { e_acsl_fail((char *)"(x == -3)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_5));
__gmpz_clear((__mpz_struct *)(e_acsl_6));
__gmpz_clear((__mpz_struct *)(e_acsl_7));
@@ -651,7 +645,7 @@ void main(void)
__gmpz_com(e_acsl_11,(__mpz_struct const *)(e_acsl_10));
e_acsl_12 = __gmpz_cmp((__mpz_struct const *)(e_acsl_9),
(__mpz_struct const *)(e_acsl_11));
- if (e_acsl_12 == 0) { e_acsl_fail((char *)"(0 != ~0)"); }
+ if (! (e_acsl_12 != 0)) { e_acsl_fail((char *)"(0 != ~0)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_9));
__gmpz_clear((__mpz_struct *)(e_acsl_10));
__gmpz_clear((__mpz_struct *)(e_acsl_11));
@@ -670,7 +664,7 @@ void main(void)
__gmpz_neg((__mpz_struct *)(e_acsl_17),(__mpz_struct const *)(e_acsl_16));
e_acsl_18 = __gmpz_cmp((__mpz_struct const *)(e_acsl_15),
(__mpz_struct const *)(e_acsl_17));
- if (e_acsl_18 != 0) { e_acsl_fail((char *)"(x+1 == -2)"); }
+ if (! (e_acsl_18 == 0)) { e_acsl_fail((char *)"(x+1 == -2)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_13));
__gmpz_clear((__mpz_struct *)(e_acsl_14));
__gmpz_clear((__mpz_struct *)(e_acsl_15));
@@ -691,7 +685,7 @@ void main(void)
__gmpz_neg((__mpz_struct *)(e_acsl_23),(__mpz_struct const *)(e_acsl_22));
e_acsl_24 = __gmpz_cmp((__mpz_struct const *)(e_acsl_21),
(__mpz_struct const *)(e_acsl_23));
- if (e_acsl_24 != 0) { e_acsl_fail((char *)"(x-1 == -4)"); }
+ if (! (e_acsl_24 == 0)) { e_acsl_fail((char *)"(x-1 == -4)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_19));
__gmpz_clear((__mpz_struct *)(e_acsl_20));
__gmpz_clear((__mpz_struct *)(e_acsl_21));
@@ -712,7 +706,7 @@ void main(void)
__gmpz_neg((__mpz_struct *)(e_acsl_29),(__mpz_struct const *)(e_acsl_28));
e_acsl_30 = __gmpz_cmp((__mpz_struct const *)(e_acsl_27),
(__mpz_struct const *)(e_acsl_29));
- if (e_acsl_30 != 0) { e_acsl_fail((char *)"(x*3 == -9)"); }
+ if (! (e_acsl_30 == 0)) { e_acsl_fail((char *)"(x*3 == -9)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_25));
__gmpz_clear((__mpz_struct *)(e_acsl_26));
__gmpz_clear((__mpz_struct *)(e_acsl_27));
@@ -739,7 +733,7 @@ void main(void)
__gmpz_neg((__mpz_struct *)(e_acsl_38),(__mpz_struct const *)(e_acsl_37));
e_acsl_39 = __gmpz_cmp((__mpz_struct const *)(e_acsl_36),
(__mpz_struct const *)(e_acsl_38));
- if (e_acsl_39 != 0) { e_acsl_fail((char *)"(x/3 == -1)"); }
+ if (! (e_acsl_39 == 0)) { e_acsl_fail((char *)"(x/3 == -1)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_31));
__gmpz_clear((__mpz_struct *)(e_acsl_32));
__gmpz_clear((__mpz_struct *)(e_acsl_33));
@@ -760,14 +754,14 @@ void main(void)
(__mpz_struct const *)(e_acsl_43));
__gmpz_init((__mpz_struct *)(e_acsl_45)); /*@ assert 2 ≢ 0U; */ ;
if (e_acsl_44 == 0) { e_acsl_fail((char *)"(2 == 0U)"); }
- __gmpz_mod((__mpz_struct *)(e_acsl_45),(__mpz_struct const *)(e_acsl_40),
- (__mpz_struct const *)(e_acsl_41));
+ __gmpz_fdiv_r_ui(e_acsl_45,(__mpz_struct const *)(e_acsl_40),
+ (unsigned long)(e_acsl_41));
__gmpz_init_set_si((__mpz_struct *)(e_acsl_46),(long)1);
__gmpz_init((__mpz_struct *)(e_acsl_47));
__gmpz_neg((__mpz_struct *)(e_acsl_47),(__mpz_struct const *)(e_acsl_46));
e_acsl_48 = __gmpz_cmp((__mpz_struct const *)(e_acsl_45),
(__mpz_struct const *)(e_acsl_47));
- if (e_acsl_48 != 0) { e_acsl_fail((char *)"(x%2 == -1)"); }
+ if (! (e_acsl_48 == 0)) { e_acsl_fail((char *)"(x%2 == -1)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_40));
__gmpz_clear((__mpz_struct *)(e_acsl_41));
__gmpz_clear((__mpz_struct *)(e_acsl_42));
@@ -812,7 +806,7 @@ void main(void)
__gmpz_neg((__mpz_struct *)(e_acsl_63),(__mpz_struct const *)(e_acsl_62));
e_acsl_64 = __gmpz_cmp((__mpz_struct const *)(e_acsl_61),
(__mpz_struct const *)(e_acsl_63));
- if (e_acsl_64 != 0) {
+ if (! (e_acsl_64 == 0)) {
e_acsl_fail((char *)"(((x*2+(3+y))-4)+(x-y) == -10)");
} __gmpz_clear((__mpz_struct *)(e_acsl_49));
__gmpz_clear((__mpz_struct *)(e_acsl_50));
@@ -842,7 +836,7 @@ void main(void)
__gmpz_init_set_si((__mpz_struct *)(e_acsl_69),(long)0);
e_acsl_70 = __gmpz_cmp((__mpz_struct const *)(e_acsl_68),
(__mpz_struct const *)(e_acsl_69));
- if ((e_acsl_67 == 0) != ! (e_acsl_70 == 0)) {
+ if (! ((e_acsl_67 == 0) == ! (e_acsl_70 == 0))) {
e_acsl_fail((char *)"((0==1) == !(0==0))");
} __gmpz_clear((__mpz_struct *)(e_acsl_65));
__gmpz_clear((__mpz_struct *)(e_acsl_66));
@@ -863,7 +857,7 @@ void main(void)
__gmpz_init_set_si((__mpz_struct *)(e_acsl_76),(long)0);
e_acsl_77 = __gmpz_cmp((__mpz_struct const *)(e_acsl_75),
(__mpz_struct const *)(e_acsl_76));
- if ((e_acsl_74 <= 0) != (e_acsl_77 > 0)) {
+ if (! ((e_acsl_74 <= 0) == (e_acsl_77 > 0))) {
e_acsl_fail((char *)"((0<=-1) == (0>0))");
} __gmpz_clear((__mpz_struct *)(e_acsl_71));
__gmpz_clear((__mpz_struct *)(e_acsl_72));
@@ -885,7 +879,7 @@ void main(void)
__gmpz_init_set_si((__mpz_struct *)(e_acsl_83),(long)0);
e_acsl_84 = __gmpz_cmp((__mpz_struct const *)(e_acsl_82),
(__mpz_struct const *)(e_acsl_83));
- if ((e_acsl_81 >= 0) != (e_acsl_84 <= 0)) {
+ if (! ((e_acsl_81 >= 0) == (e_acsl_84 <= 0))) {
e_acsl_fail((char *)"((0>=-1) == (0<=0))");
} __gmpz_clear((__mpz_struct *)(e_acsl_78));
__gmpz_clear((__mpz_struct *)(e_acsl_79));
@@ -905,7 +899,7 @@ void main(void)
__gmpz_init_set_si((__mpz_struct *)(e_acsl_89),(long)0);
e_acsl_90 = __gmpz_cmp((__mpz_struct const *)(e_acsl_88),
(__mpz_struct const *)(e_acsl_89));
- if ((e_acsl_87 != 0) != ! (e_acsl_90 != 0)) {
+ if (! ((e_acsl_87 != 0) == ! (e_acsl_90 != 0))) {
e_acsl_fail((char *)"((0!=1) == !(0!=0))");
} __gmpz_clear((__mpz_struct *)(e_acsl_85));
__gmpz_clear((__mpz_struct *)(e_acsl_86));
@@ -913,7 +907,8 @@ void main(void)
__gmpz_clear((__mpz_struct *)(e_acsl_89));
}
- return;
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
index 395ebf5327debe2fcd8b103d8d2d6530104436ee..890d4809614f6e1ce9d0390fa0c057c2cb7349da 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
@@ -549,17 +549,19 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
long x;
int y;
x = (long)0;
y = 0;
/*@ assert (int)x ≡ y; */ ;
- if ((int)x != y) { e_acsl_fail((char *)"((int)x == y)"); }
+ if (! ((int)x == y)) { e_acsl_fail((char *)"((int)x == y)"); }
/*@ assert x ≡ (long)y; */ ;
- if (x != (long)y) { e_acsl_fail((char *)"(x == (long)y)"); }
- return;
+ if (! (x == (long)y)) { e_acsl_fail((char *)"(x == (long)y)"); }
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index 5e05e161569236cfc5f6b03b349e8e15e60047aa..6314572f51163c6b87d06e17e6c26f616e5813eb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -562,24 +562,25 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
int x;
int y;
char *s;
x = 0;
y = 1;
/*@ assert x < y; */ ;
- if (x >= y) { e_acsl_fail((char *)"(x < y)"); }
+ if (! (x < y)) { e_acsl_fail((char *)"(x < y)"); }
/*@ assert y > x; */ ;
- if (y <= x) { e_acsl_fail((char *)"(y > x)"); }
+ if (! (y > x)) { e_acsl_fail((char *)"(y > x)"); }
/*@ assert x ≤ 0; */ ;
{ mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3;
__gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)x);
__gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
(__mpz_struct const *)(e_acsl_2));
- if (e_acsl_3 > 0) { e_acsl_fail((char *)"(x <= 0)"); }
+ if (! (e_acsl_3 <= 0)) { e_acsl_fail((char *)"(x <= 0)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_1));
__gmpz_clear((__mpz_struct *)(e_acsl_2));
}
@@ -590,23 +591,24 @@ void main(void)
__gmpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)1);
e_acsl_6 = __gmpz_cmp((__mpz_struct const *)(e_acsl_4),
(__mpz_struct const *)(e_acsl_5));
- if (e_acsl_6 < 0) { e_acsl_fail((char *)"(y >= 1)"); }
+ if (! (e_acsl_6 >= 0)) { e_acsl_fail((char *)"(y >= 1)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_4));
__gmpz_clear((__mpz_struct *)(e_acsl_5));
}
s = (char *)"toto";
/*@ assert s ≡ s; */ ;
- if (s != s) { e_acsl_fail((char *)"(s == s)"); }
+ if (! (s == s)) { e_acsl_fail((char *)"(s == s)"); }
/*@ assert "toto" ≢ "titi"; */ ;
- if ("toto" == "titi") { e_acsl_fail((char *)"(\"toto\" != \"titi\")"); }
+ if (! ("toto" != "titi")) { e_acsl_fail((char *)"(\"toto\" != \"titi\")");
+ }
/*@ assert 5 < 18; */ ;
{ mpz_t e_acsl_7; mpz_t e_acsl_8; int e_acsl_9;
__gmpz_init_set_si((__mpz_struct *)(e_acsl_7),(long)5);
__gmpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)18);
e_acsl_9 = __gmpz_cmp((__mpz_struct const *)(e_acsl_7),
(__mpz_struct const *)(e_acsl_8));
- if (e_acsl_9 >= 0) { e_acsl_fail((char *)"(5 < 18)"); }
+ if (! (e_acsl_9 < 0)) { e_acsl_fail((char *)"(5 < 18)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_7));
__gmpz_clear((__mpz_struct *)(e_acsl_8));
}
@@ -617,7 +619,7 @@ void main(void)
__gmpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)3);
e_acsl_12 = __gmpz_cmp((__mpz_struct const *)(e_acsl_10),
(__mpz_struct const *)(e_acsl_11));
- if (e_acsl_12 <= 0) { e_acsl_fail((char *)"(32 > 3)"); }
+ if (! (e_acsl_12 > 0)) { e_acsl_fail((char *)"(32 > 3)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_10));
__gmpz_clear((__mpz_struct *)(e_acsl_11));
}
@@ -628,7 +630,7 @@ void main(void)
__gmpz_init_set_si((__mpz_struct *)(e_acsl_14),(long)13);
e_acsl_15 = __gmpz_cmp((__mpz_struct const *)(e_acsl_13),
(__mpz_struct const *)(e_acsl_14));
- if (e_acsl_15 > 0) { e_acsl_fail((char *)"(12 <= 13)"); }
+ if (! (e_acsl_15 <= 0)) { e_acsl_fail((char *)"(12 <= 13)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_13));
__gmpz_clear((__mpz_struct *)(e_acsl_14));
}
@@ -639,7 +641,7 @@ void main(void)
__gmpz_init_set_si((__mpz_struct *)(e_acsl_17),(long)12);
e_acsl_18 = __gmpz_cmp((__mpz_struct const *)(e_acsl_16),
(__mpz_struct const *)(e_acsl_17));
- if (e_acsl_18 < 0) { e_acsl_fail((char *)"(123 >= 12)"); }
+ if (! (e_acsl_18 >= 0)) { e_acsl_fail((char *)"(123 >= 12)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_16));
__gmpz_clear((__mpz_struct *)(e_acsl_17));
}
@@ -650,7 +652,7 @@ void main(void)
__gmpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)0xff);
e_acsl_21 = __gmpz_cmp((__mpz_struct const *)(e_acsl_19),
(__mpz_struct const *)(e_acsl_20));
- if (e_acsl_21 != 0) { e_acsl_fail((char *)"(0xff == 0xff)"); }
+ if (! (e_acsl_21 == 0)) { e_acsl_fail((char *)"(0xff == 0xff)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_19));
__gmpz_clear((__mpz_struct *)(e_acsl_20));
}
@@ -661,12 +663,13 @@ void main(void)
__gmpz_init_set_si((__mpz_struct *)(e_acsl_23),(long)2);
e_acsl_24 = __gmpz_cmp((__mpz_struct const *)(e_acsl_22),
(__mpz_struct const *)(e_acsl_23));
- if (e_acsl_24 == 0) { e_acsl_fail((char *)"(1 != 2)"); }
+ if (! (e_acsl_24 != 0)) { e_acsl_fail((char *)"(1 != 2)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_22));
__gmpz_clear((__mpz_struct *)(e_acsl_23));
}
- return;
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
index b2978110624154691b23051dda7853f608063ca4..c421b9d08fcbfd79cbef993f42392d7575019a0e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
@@ -549,12 +549,14 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
int x;
x = 0;
if (x) { /*@ assert \false; */ ; e_acsl_fail((char *)"(\\false)"); }
- return;
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index fc364dd68c01220b4fa69d33acf4e667c9699237..dc3fe0bba1cbcdb4b6fe2e0f1cfc4bb8be895ff3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -566,26 +566,29 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
+ int x;
/*@ assert 0 ≡ 0; */ ;
{ mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3;
__gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)0);
__gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
(__mpz_struct const *)(e_acsl_2));
- if (e_acsl_3 != 0) { e_acsl_fail((char *)"(0 == 0)"); }
+ if (! (e_acsl_3 == 0)) { e_acsl_fail((char *)"(0 == 0)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_1));
__gmpz_clear((__mpz_struct *)(e_acsl_2));
}
+ x = 0;
/*@ assert 0 ≢ 1; */ ;
{ mpz_t e_acsl_4; mpz_t e_acsl_5; int e_acsl_6;
__gmpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)0);
__gmpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)1);
e_acsl_6 = __gmpz_cmp((__mpz_struct const *)(e_acsl_4),
(__mpz_struct const *)(e_acsl_5));
- if (e_acsl_6 == 0) { e_acsl_fail((char *)"(0 != 1)"); }
+ if (! (e_acsl_6 != 0)) { e_acsl_fail((char *)"(0 != 1)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_4));
__gmpz_clear((__mpz_struct *)(e_acsl_5));
}
@@ -596,13 +599,14 @@ void main(void)
__gmpz_init_set_str((__mpz_struct *)(e_acsl_8),"1152921504606846975",10);
e_acsl_9 = __gmpz_cmp((__mpz_struct const *)(e_acsl_7),
(__mpz_struct const *)(e_acsl_8));
- if (e_acsl_9 != 0) {
+ if (! (e_acsl_9 == 0)) {
e_acsl_fail((char *)"(0xfffffffffffffff == 0xfffffffffffffff)");
} __gmpz_clear((__mpz_struct *)(e_acsl_7));
__gmpz_clear((__mpz_struct *)(e_acsl_8));
}
- return;
+ __retres = 0;
+ return (__retres);
}
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
new file mode 100644
index 0000000000000000000000000000000000000000..bf375629f9222109efc8e7f211c3fc20418c9461
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
@@ -0,0 +1,788 @@
+/* Generated by Frama-C */
+typedef unsigned long size_t;
+typedef unsigned long mp_limb_t;
+struct __anonstruct___mpz_struct_6 {
+ int _mp_alloc ;
+ int _mp_size ;
+ mp_limb_t *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_6 __mpz_struct;
+typedef __mpz_struct mpz_t[1];
+typedef mp_limb_t *mp_ptr;
+typedef mp_limb_t const *mp_srcptr;
+typedef long mp_size_t;
+struct __anonstruct___mpq_struct_7 {
+ __mpz_struct _mp_num ;
+ __mpz_struct _mp_den ;
+};
+typedef struct __anonstruct___mpq_struct_7 __mpq_struct;
+typedef __mpz_struct const *mpz_srcptr;
+typedef __mpz_struct *mpz_ptr;
+typedef __mpq_struct const *mpq_srcptr;
+typedef __mpq_struct *mpq_ptr;
+/* compiler builtin:
+ long __builtin_expect(long, long); */
+/*@ assigns \nothing; */
+extern int printf(char const * __restrict __format , ...);
+__inline static void __gmpz_abs(mpz_ptr __gmp_w, mpz_srcptr __gmp_u);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+*/
+extern void __gmpz_cdiv_q(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2,
+ __mpz_struct const * /*[1]*/ z3);
+/*@ requires \valid(x);
+ assigns *x; */
+extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
+ mp_size_t __gmp_n) __attribute__((
+__pure__));
+/*@ ensures \valid(\old(x));
+ assigns *x; */
+extern void __gmpz_init(__mpz_struct * /*[1]*/ x);
+/*@ ensures \valid(\old(z));
+ assigns *z; */
+extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+/*@ ensures \valid(\old(z));
+ assigns *z; */
+extern void __gmpz_init_set_ui(__mpz_struct * /*[1]*/ z, unsigned long n);
+__inline static void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+__inline static int __gmpz_perfect_square_p(mpz_srcptr __gmp_a) __attribute__((
+__pure__));
+__inline static unsigned long __gmpz_popcount(mpz_srcptr __gmp_u) __attribute__((
+__pure__));
+extern void __gmpz_set(mpz_ptr, mpz_srcptr);
+__inline static void __gmpz_set_q(mpz_ptr __gmp_w, mpq_srcptr __gmp_u);
+__inline static size_t __gmpz_size(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+extern void __gmpz_tdiv_q(mpz_ptr, mpz_srcptr, mpz_srcptr);
+__inline static void __gmpq_abs(mpq_ptr __gmp_w, mpq_srcptr __gmp_u);
+__inline static void __gmpq_neg(mpq_ptr __gmp_w, mpq_srcptr __gmp_u);
+extern void __gmpq_set(mpq_ptr, mpq_srcptr);
+__inline static mp_limb_t __gmpn_add(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
+ mp_size_t __gmp_xsize,
+ mp_srcptr __gmp_yp,
+ mp_size_t __gmp_ysize);
+__inline static mp_limb_t __gmpn_add_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
+ mp_size_t __gmp_size,
+ mp_limb_t __gmp_n);
+extern mp_limb_t __gmpn_add_n(mp_ptr, mp_srcptr, mp_srcptr, mp_size_t);
+__inline static int __gmpn_cmp(mp_srcptr __gmp_xp, mp_srcptr __gmp_yp,
+ mp_size_t __gmp_size) __attribute__((__pure__));
+__inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
+ mp_size_t __gmp_n);
+extern int __gmpn_perfect_square_p(mp_srcptr, mp_size_t) __attribute__((
+__pure__));
+extern unsigned long __gmpn_popcount(mp_srcptr, mp_size_t) __attribute__((
+__pure__));
+__inline static mp_limb_t __gmpn_sub(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
+ mp_size_t __gmp_xsize,
+ mp_srcptr __gmp_yp,
+ mp_size_t __gmp_ysize);
+__inline static mp_limb_t __gmpn_sub_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
+ mp_size_t __gmp_size,
+ mp_limb_t __gmp_n);
+extern mp_limb_t __gmpn_sub_n(mp_ptr, mp_srcptr, mp_srcptr, mp_size_t);
+__inline static void __gmpz_abs(mpz_ptr __gmp_w, mpz_srcptr __gmp_u)
+{
+ if (__gmp_w != __gmp_u) { __gmpz_set(__gmp_w,__gmp_u); }
+ if (__gmp_w->_mp_size >= 0) { __gmp_w->_mp_size = __gmp_w->_mp_size; }
+ else { __gmp_w->_mp_size = - __gmp_w->_mp_size; }
+ return;
+}
+
+__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
+{
+ int __retres;
+ mp_size_t __gmp_n;
+ mp_ptr __gmp_p;
+ int tmp;
+ __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+ __gmp_p = __gmp_z->_mp_d;
+ if (__gmp_n == (mp_size_t)0) { tmp = 1; }
+ else {
+ if (__gmp_n == (mp_size_t)1) {
+ if (*(__gmp_p + 0) <= (mp_limb_t)(~ ((unsigned int)0))) { tmp = 1; }
+ else { tmp = 0; }
+ }
+ else { tmp = 0; }
+ }
+ __retres = tmp;
+ goto return_label;
+ return_label: /* internal */
+ return (__retres);
+}
+
+__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
+{
+ int __retres;
+ mp_size_t __gmp_n;
+ mp_ptr __gmp_p;
+ int tmp;
+ __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+ __gmp_p = __gmp_z->_mp_d;
+ if (__gmp_n == (mp_size_t)0) { tmp = 1; }
+ else {
+ if (__gmp_n == (mp_size_t)1) {
+ if (*(__gmp_p + 0) <= ~ ((unsigned long)0)) { tmp = 1; }
+ else { tmp = 0; }
+ }
+ else { tmp = 0; }
+ }
+ __retres = tmp;
+ goto return_label;
+ return_label: /* internal */
+ return (__retres);
+}
+
+__inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
+{
+ int __retres;
+ mp_size_t __gmp_n;
+ mp_ptr __gmp_p;
+ int tmp;
+ __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+ __gmp_p = __gmp_z->_mp_d;
+ if (__gmp_n == (mp_size_t)0) { tmp = 1; }
+ else {
+ if (__gmp_n == (mp_size_t)1) {
+ if (*(__gmp_p + 0) <= (mp_limb_t)((unsigned short)(~ 0))) { tmp = 1; }
+ else { tmp = 0; }
+ }
+ else { tmp = 0; }
+ }
+ __retres = tmp;
+ goto return_label;
+ return_label: /* internal */
+ return (__retres);
+}
+
+__inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z)
+{
+ mp_ptr __gmp_p;
+ mp_size_t __gmp_n;
+ mp_limb_t __gmp_l;
+ mp_limb_t tmp;
+ __gmp_p = __gmp_z->_mp_d;
+ __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+ __gmp_l = *(__gmp_p + 0);
+ if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
+ else { tmp = (unsigned long)0; }
+ return (tmp);
+}
+
+__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
+ mp_size_t __gmp_n) __attribute__((
+__pure__));
+__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
+ mp_size_t __gmp_n)
+{
+ mp_limb_t __gmp_result;
+ long tmp_1;
+ int tmp_0;
+ __gmp_result = (mp_limb_t)0;
+ { /*undefined sequence*/
+ if (__gmp_n >= (mp_size_t)0) {
+ int tmp;
+ { /*undefined sequence*/
+ if (__gmp_z->_mp_size >= 0) { tmp = __gmp_z->_mp_size; }
+ else { tmp = - __gmp_z->_mp_size; }
+ ;
+ }
+ if (__gmp_n < (mp_size_t)tmp) { tmp_0 = 1; }
+ else { tmp_0 = 0; }
+ }
+ else { tmp_0 = 0; }
+ tmp_1 = __builtin_expect((long)(tmp_0 != 0),(long)1);
+ }
+ if (tmp_1) { __gmp_result = *(__gmp_z->_mp_d + __gmp_n); }
+ return (__gmp_result);
+}
+
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns *z1; */
+__inline static void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2)
+{
+ if (z1 != z2) { __gmpz_set(z1,z2); }
+ z1->_mp_size = - z1->_mp_size;
+ return;
+}
+
+__inline static int __gmpz_perfect_square_p(mpz_srcptr __gmp_a) __attribute__((
+__pure__));
+__inline static int __gmpz_perfect_square_p(mpz_srcptr __gmp_a)
+{
+ mp_size_t __gmp_asize;
+ int __gmp_result;
+ long tmp;
+ __gmp_asize = (long)__gmp_a->_mp_size;
+ __gmp_result = __gmp_asize >= (mp_size_t)0;
+ tmp = __builtin_expect((long)((__gmp_asize > (mp_size_t)0) != 0),(long)1);
+ if (tmp) {
+ __gmp_result = __gmpn_perfect_square_p((mp_limb_t const *)__gmp_a->_mp_d,
+ __gmp_asize);
+ }
+ return (__gmp_result);
+}
+
+__inline static unsigned long __gmpz_popcount(mpz_srcptr __gmp_u) __attribute__((
+__pure__));
+__inline static unsigned long __gmpz_popcount(mpz_srcptr __gmp_u)
+{
+ mp_size_t __gmp_usize;
+ unsigned long __gmp_result;
+ long tmp;
+ __gmp_usize = (long)__gmp_u->_mp_size;
+ if (__gmp_usize < (mp_size_t)0) { __gmp_result = ~ ((unsigned long)0); }
+ else { __gmp_result = (unsigned long)0; }
+ tmp = __builtin_expect((long)((__gmp_usize > (mp_size_t)0) != 0),(long)1);
+ if (tmp) {
+ __gmp_result = __gmpn_popcount((mp_limb_t const *)__gmp_u->_mp_d,
+ __gmp_usize);
+ }
+ return (__gmp_result);
+}
+
+__inline static void __gmpz_set_q(mpz_ptr __gmp_w, mpq_srcptr __gmp_u)
+{
+ __gmpz_tdiv_q(__gmp_w,& __gmp_u->_mp_num,& __gmp_u->_mp_den);
+ return;
+}
+
+__inline static size_t __gmpz_size(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static size_t __gmpz_size(mpz_srcptr __gmp_z)
+{
+ size_t __retres;
+ int tmp;
+ if (__gmp_z->_mp_size >= 0) { tmp = __gmp_z->_mp_size; }
+ else { tmp = - __gmp_z->_mp_size; }
+ __retres = (unsigned long)tmp;
+ return (__retres);
+}
+
+__inline static void __gmpq_abs(mpq_ptr __gmp_w, mpq_srcptr __gmp_u)
+{
+ if (__gmp_w != __gmp_u) { __gmpq_set(__gmp_w,__gmp_u); }
+ if (__gmp_w->_mp_num._mp_size >= 0) {
+ __gmp_w->_mp_num._mp_size = __gmp_w->_mp_num._mp_size;
+ }
+ else { __gmp_w->_mp_num._mp_size = - __gmp_w->_mp_num._mp_size; }
+ return;
+}
+
+__inline static void __gmpq_neg(mpq_ptr __gmp_w, mpq_srcptr __gmp_u)
+{
+ if (__gmp_w != __gmp_u) { __gmpq_set(__gmp_w,__gmp_u); }
+ __gmp_w->_mp_num._mp_size = - __gmp_w->_mp_num._mp_size;
+ return;
+}
+
+__inline static mp_limb_t __gmpn_add(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
+ mp_size_t __gmp_xsize,
+ mp_srcptr __gmp_yp,
+ mp_size_t __gmp_ysize)
+{
+ mp_limb_t __gmp_c;
+ while (1) {
+ { mp_size_t __gmp_i; mp_limb_t __gmp_x; __gmp_i = __gmp_ysize;
+ if (__gmp_i != (mp_size_t)0) {
+ mp_limb_t tmp_1;
+ tmp_1 = __gmpn_add_n(__gmp_wp,__gmp_xp,__gmp_yp,__gmp_i);
+ if (tmp_1) {
+ while (1) {
+ mp_size_t tmp;
+ mp_limb_t tmp_0;
+ if (__gmp_i >= __gmp_xsize) {
+ __gmp_c = (unsigned long)1;
+ goto __gmp_done;
+ }
+ __gmp_x = *(__gmp_xp + __gmp_i);
+ { /*undefined sequence*/
+ tmp = __gmp_i;
+ __gmp_i += (mp_size_t)1;
+ tmp_0 = (__gmp_x + (mp_limb_t)1) & (~ ((unsigned long)0) >> 0);
+ *(__gmp_wp + tmp) = tmp_0;
+ }
+ if (! (tmp_0 == (mp_limb_t)0)) { break; }
+ }
+ }
+ }
+ if (__gmp_wp != __gmp_xp) {
+ while (1) {
+ { mp_size_t __gmp_j; __gmp_j = __gmp_i;
+ while (__gmp_j < __gmp_xsize) {
+ *(__gmp_wp + __gmp_j) = *(__gmp_xp + __gmp_j);
+ __gmp_j += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ } __gmp_c = (unsigned long)0; __gmp_done: ;
+ }
+
+ break;
+ }
+ return (__gmp_c);
+}
+
+__inline static mp_limb_t __gmpn_add_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
+ mp_size_t __gmp_size,
+ mp_limb_t __gmp_n)
+{
+ mp_limb_t __gmp_c;
+ while (1) {
+ { mp_size_t __gmp_i; mp_limb_t __gmp_x; mp_limb_t __gmp_r;
+ __gmp_x = *(__gmp_src + 0); __gmp_r = __gmp_x + __gmp_n;
+ *(__gmp_dst + 0) = __gmp_r;
+ if (__gmp_r < __gmp_n) {
+ __gmp_c = (unsigned long)1;
+ __gmp_i = (long)1;
+ while (__gmp_i < __gmp_size) {
+ __gmp_x = *(__gmp_src + __gmp_i);
+ __gmp_r = __gmp_x + (mp_limb_t)1;
+ *(__gmp_dst + __gmp_i) = __gmp_r;
+ __gmp_i += (mp_size_t)1;
+ if (! (__gmp_r < (mp_limb_t)1)) {
+ if (__gmp_src != __gmp_dst) {
+ while (1) {
+ { mp_size_t __gmp_j; __gmp_j = __gmp_i;
+ while (__gmp_j < __gmp_size) {
+ *(__gmp_dst + __gmp_j) = *(__gmp_src + __gmp_j);
+ __gmp_j += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ break;
+ }
+ }
+ }
+ else {
+ if (__gmp_src != __gmp_dst) {
+ while (1) {
+ { mp_size_t __gmp_j_0; __gmp_j_0 = (long)1;
+ while (__gmp_j_0 < __gmp_size) {
+ *(__gmp_dst + __gmp_j_0) = *(__gmp_src + __gmp_j_0);
+ __gmp_j_0 += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ }
+ }
+
+ break;
+ }
+ return (__gmp_c);
+}
+
+__inline static int __gmpn_cmp(mp_srcptr __gmp_xp, mp_srcptr __gmp_yp,
+ mp_size_t __gmp_size) __attribute__((__pure__));
+__inline static int __gmpn_cmp(mp_srcptr __gmp_xp, mp_srcptr __gmp_yp,
+ mp_size_t __gmp_size)
+{
+ int __gmp_result;
+ while (1) {
+ { mp_size_t __gmp_i; mp_limb_t __gmp_x; mp_limb_t __gmp_y;
+ __gmp_result = 0; __gmp_i = __gmp_size;
+ while (1) {
+ __gmp_i -= (mp_size_t)1;
+ if (! (__gmp_i >= (mp_size_t)0)) { break; }
+ __gmp_x = *(__gmp_xp + __gmp_i);
+ __gmp_y = *(__gmp_yp + __gmp_i);
+ if (__gmp_x != __gmp_y) {
+ if (__gmp_x > __gmp_y) { __gmp_result = 1; }
+ else { __gmp_result = -1; }
+ break;
+ }
+ }
+ }
+
+ break;
+ }
+ return (__gmp_result);
+}
+
+__inline static mp_limb_t __gmpn_sub(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
+ mp_size_t __gmp_xsize,
+ mp_srcptr __gmp_yp,
+ mp_size_t __gmp_ysize)
+{
+ mp_limb_t __gmp_c;
+ while (1) {
+ { mp_size_t __gmp_i; mp_limb_t __gmp_x; __gmp_i = __gmp_ysize;
+ if (__gmp_i != (mp_size_t)0) {
+ mp_limb_t tmp_0;
+ tmp_0 = __gmpn_sub_n(__gmp_wp,__gmp_xp,__gmp_yp,__gmp_i);
+ if (tmp_0) {
+ while (1) {
+ mp_size_t tmp;
+ if (__gmp_i >= __gmp_xsize) {
+ __gmp_c = (unsigned long)1;
+ goto __gmp_done;
+ }
+ __gmp_x = *(__gmp_xp + __gmp_i);
+ { /*undefined sequence*/
+ tmp = __gmp_i;
+ __gmp_i += (mp_size_t)1;
+ *(__gmp_wp + tmp) = (__gmp_x - (mp_limb_t)1) & (~ ((unsigned long)0) >> 0);
+ }
+ if (! (__gmp_x == (mp_limb_t)0)) { break; }
+ }
+ }
+ }
+ if (__gmp_wp != __gmp_xp) {
+ while (1) {
+ { mp_size_t __gmp_j; __gmp_j = __gmp_i;
+ while (__gmp_j < __gmp_xsize) {
+ *(__gmp_wp + __gmp_j) = *(__gmp_xp + __gmp_j);
+ __gmp_j += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ } __gmp_c = (unsigned long)0; __gmp_done: ;
+ }
+
+ break;
+ }
+ return (__gmp_c);
+}
+
+__inline static mp_limb_t __gmpn_sub_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
+ mp_size_t __gmp_size,
+ mp_limb_t __gmp_n)
+{
+ mp_limb_t __gmp_c;
+ while (1) {
+ { mp_size_t __gmp_i; mp_limb_t __gmp_x; mp_limb_t __gmp_r;
+ __gmp_x = *(__gmp_src + 0); __gmp_r = __gmp_x - __gmp_n;
+ *(__gmp_dst + 0) = __gmp_r;
+ if (__gmp_x < __gmp_n) {
+ __gmp_c = (unsigned long)1;
+ __gmp_i = (long)1;
+ while (__gmp_i < __gmp_size) {
+ __gmp_x = *(__gmp_src + __gmp_i);
+ __gmp_r = __gmp_x - (mp_limb_t)1;
+ *(__gmp_dst + __gmp_i) = __gmp_r;
+ __gmp_i += (mp_size_t)1;
+ if (! (__gmp_x < (mp_limb_t)1)) {
+ if (__gmp_src != __gmp_dst) {
+ while (1) {
+ { mp_size_t __gmp_j; __gmp_j = __gmp_i;
+ while (__gmp_j < __gmp_size) {
+ *(__gmp_dst + __gmp_j) = *(__gmp_src + __gmp_j);
+ __gmp_j += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ break;
+ }
+ }
+ }
+ else {
+ if (__gmp_src != __gmp_dst) {
+ while (1) {
+ { mp_size_t __gmp_j_0; __gmp_j_0 = (long)1;
+ while (__gmp_j_0 < __gmp_size) {
+ *(__gmp_dst + __gmp_j_0) = *(__gmp_src + __gmp_j_0);
+ __gmp_j_0 += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ }
+ }
+
+ break;
+ }
+ return (__gmp_c);
+}
+
+__inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
+ mp_size_t __gmp_n)
+{
+ mp_limb_t __gmp_ul;
+ mp_limb_t __gmp_cy;
+ __gmp_cy = (unsigned long)0;
+ while (1) {
+ { mp_srcptr tmp; mp_ptr tmp_0;
+ { /*undefined sequence*/ tmp = __gmp_up; __gmp_up ++; __gmp_ul = *tmp;
+ }
+ { /*undefined sequence*/
+ tmp_0 = __gmp_rp;
+ __gmp_rp ++;
+ *tmp_0 = - __gmp_ul - __gmp_cy;
+ } __gmp_cy |= (unsigned long)(__gmp_ul != (mp_limb_t)0);
+ }
+
+ __gmp_n -= (mp_size_t)1;
+ if (! (__gmp_n != (mp_size_t)0)) { break; }
+ }
+ return (__gmp_cy);
+}
+
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+void e_acsl_fail(char *msg)
+{
+ printf((char const *)"%s\n",msg);
+ exit(1);
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int x;
+ int y;
+ x = 0;
+ y = 1;
+ /*@ assert x ≡ 0 ∧ y ≡ 1; */ ;
+ { mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3; int e_acsl_7;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
+ 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));
+ } else { e_acsl_7 = 0; }
+ if (! e_acsl_7) { e_acsl_fail((char *)"(x == 0 && y == 1)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_1));
+ __gmpz_clear((__mpz_struct *)(e_acsl_2));
+ }
+
+ /*@ 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_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));
+ /*@ 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;
+ __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));
+ }
+
+ /*@ 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; }
+ 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));
+ }
+
+ /*@ 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; }
+ 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);
+ 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));
+ __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));
+ }
+
+ /*@ 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; }
+ else {
+ mpz_t e_acsl_83;
+ mpz_t e_acsl_84;
+ int e_acsl_85;
+ __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_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));
+ }
+
+ __retres = 0;
+ return (__retres);
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
index 8bfae8d97c5c89f4ab74fa678973ebf84cb4a573..073aca9609a4ac9608ea01bec196e68b836b11a7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
@@ -549,17 +549,19 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
int x;
x = 0;
/*@ assert x ≡ 0; */ ;
- if (x != 0) { e_acsl_fail((char *)"(x == 0)"); }
+ if (! (x == 0)) { e_acsl_fail((char *)"(x == 0)"); }
if (x) {
/*@ assert x ≢ 0; */ ;
- if (x == 0) { e_acsl_fail((char *)"(x != 0)"); }
+ if (! (x != 0)) { e_acsl_fail((char *)"(x != 0)"); }
}
- return;
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
index b90669a475ec5c309aa5c362f24d5d4f310df77f..8bce5f3f5d79df32449e28f6c9fe943112a4d4a7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
@@ -554,9 +554,9 @@ void main(void)
int x;
x = 0;
/*@ assert sizeof(int) ≡ sizeof(x); */ ;
- if (4 != 4) { e_acsl_fail((char *)"(sizeof(int) == sizeof(x))"); }
+ if (! (4 == 4)) { e_acsl_fail((char *)"(sizeof(int) == sizeof(x))"); }
/*@ assert sizeof("totototototo") ≡ sizeof(char *); */ ;
- if (4 != 4) {
+ if (! (4 == 4)) {
e_acsl_fail((char *)"(sizeof(\"totototototo\") == sizeof(char *))");
}
return;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_string_literal.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_string_literal.c
index 1409baeea2e4b825072f5e8cdbf0550446886452..d6ef85ef079b4bef6292672ab4273da6e93e48a7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_string_literal.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_string_literal.c
@@ -549,11 +549,14 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
/*@ assert "toto" ≢ "titi"; */ ;
- if ("toto" == "titi") { e_acsl_fail((char *)"(\"toto\" != \"titi\")"); }
- return;
+ if (! ("toto" != "titi")) { e_acsl_fail((char *)"(\"toto\" != \"titi\")");
+ }
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
index e4b6346175b8e7d5f4e128047d79dcf42c3e8c68..6a641969a85926c9f74163171e90b77476f1654c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
@@ -549,12 +549,14 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
int x;
x = 0;
/*@ assert \true; */ ;
- return;
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index c8382f6512eb221a7d3bc7dd5a23e6a98c20421e..ea258f13f9db0799dff835eb95675557af7f4cd8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -2,21 +2,21 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE.i:119:[value] Assertion got status valid.
+PROJECT_FILE.i:121:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:121.
+ Called from PROJECT_FILE.i:123.
PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:121.
+ Called from PROJECT_FILE.i:123.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:122.
+ Called from PROJECT_FILE.i:124.
PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:123.
+ Called from PROJECT_FILE.i:125.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -27,24 +27,24 @@ 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:123.
+ Called from PROJECT_FILE.i:126.
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:124.
+ Called from PROJECT_FILE.i:126.
[value] Done for function mpz_clear
-PROJECT_FILE.i:127:[value] Assertion got status valid.
+PROJECT_FILE.i:130:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:129.
+ 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:129.
+ Called from PROJECT_FILE.i:132.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:130.
+ Called from PROJECT_FILE.i:133.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:131.
+ Called from PROJECT_FILE.i:134.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -54,24 +54,24 @@ PROJECT_FILE.i:127:[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:131.
+ Called from PROJECT_FILE.i:135.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:132.
+ Called from PROJECT_FILE.i:135.
[value] Done for function mpz_clear
-PROJECT_FILE.i:135:[value] Assertion got status valid.
+PROJECT_FILE.i:138:[value] Assertion got status valid.
[value] computing for function mpz_init_set_str <- main.
- Called from PROJECT_FILE.i:137.
+ Called from PROJECT_FILE.i:140.
PROJECT_FILE.i:33:[value] Function mpz_init_set_str: postcondition got status unknown
[value] Done for function mpz_init_set_str
[value] computing for function mpz_init_set_str <- main.
- Called from PROJECT_FILE.i:138.
+ Called from PROJECT_FILE.i:141.
[value] Done for function mpz_init_set_str
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:139.
+ Called from PROJECT_FILE.i:142.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:141.
+ Called from PROJECT_FILE.i:144.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -81,10 +81,10 @@ PROJECT_FILE.i:33:[value] Function mpz_init_set_str: postcondition got status un
[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:142.
+ Called from PROJECT_FILE.i:145.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:142.
+ Called from PROJECT_FILE.i:145.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
@@ -110,6 +110,8 @@ PROJECT_FILE.i:115:[from] Non terminating function (no dependencies)
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
[value] Values for function main:
+ __retres ∈ {0}
+ x ∈ {0}
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
int _mp_alloc ;
@@ -146,26 +148,29 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
+ int x;
/*@ assert 0 ≡ 0; */ ;
{ mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3;
mpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)0);
mpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
e_acsl_3 = mpz_cmp((__mpz_struct const *)(e_acsl_1),
(__mpz_struct const *)(e_acsl_2));
- if (e_acsl_3 != 0) { e_acsl_fail((char *)"(0 == 0)"); }
+ if (! (e_acsl_3 == 0)) { e_acsl_fail((char *)"(0 == 0)"); }
mpz_clear((__mpz_struct *)(e_acsl_1));
mpz_clear((__mpz_struct *)(e_acsl_2));
}
+ x = 0;
/*@ assert 0 ≢ 1; */ ;
{ mpz_t e_acsl_4; mpz_t e_acsl_5; int e_acsl_6;
mpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)0);
mpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)1);
e_acsl_6 = mpz_cmp((__mpz_struct const *)(e_acsl_4),
(__mpz_struct const *)(e_acsl_5));
- if (e_acsl_6 == 0) { e_acsl_fail((char *)"(0 != 1)"); }
+ if (! (e_acsl_6 != 0)) { e_acsl_fail((char *)"(0 != 1)"); }
mpz_clear((__mpz_struct *)(e_acsl_4));
mpz_clear((__mpz_struct *)(e_acsl_5));
}
@@ -176,13 +181,14 @@ void main(void)
mpz_init_set_str((__mpz_struct *)(e_acsl_8),"1152921504606846975",10);
e_acsl_9 = mpz_cmp((__mpz_struct const *)(e_acsl_7),
(__mpz_struct const *)(e_acsl_8));
- if (e_acsl_9 != 0) {
+ if (! (e_acsl_9 == 0)) {
e_acsl_fail((char *)"(0xfffffffffffffff == 0xfffffffffffffff)");
} mpz_clear((__mpz_struct *)(e_acsl_7));
mpz_clear((__mpz_struct *)(e_acsl_8));
}
- return;
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
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
new file mode 100644
index 0000000000000000000000000000000000000000..4e53b06c5e06aeacbfaaed13f449077e8ba2a7c9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
@@ -0,0 +1,534 @@
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+PROJECT_FILE.i:124:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:126.
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:127.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:127.
+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.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:136.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:137.
+[value] Done for function mpz_cmp
+PROJECT_FILE.i:138:[value] assigning non deterministic value for the first time
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:139.
+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.
+[value] Done for function mpz_clear
+[value] computing for function e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:142.
+[value] computing for function printf <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:115.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:115.
+PROJECT_FILE.i:105:[value] Function exit: postcondition got status invalid
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:143.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:143.
+[value] Done for function mpz_clear
+PROJECT_FILE.i:146:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:150.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:150.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:151.
+[value] Done for function mpz_cmp
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:164.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:165.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:166.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:167.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_ui <- main.
+ Called from PROJECT_FILE.i:168.
+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.
+[value] Done for function mpz_cmp
+[value] computing for function mpz_init <- main.
+ Called from PROJECT_FILE.i:170.
+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)..
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:184.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:184.
+[value] Done for function mpz_clear
+PROJECT_FILE.i:187:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:189.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:190.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:190.
+[value] Done for function mpz_cmp
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:199.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:200.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:201.
+[value] Done for function mpz_cmp
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:203.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:204.
+[value] Done for function mpz_clear
+[value] computing for function e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:205.
+[value] computing for function printf <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:115.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:115.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:206.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:206.
+[value] Done for function mpz_clear
+PROJECT_FILE.i:209:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:213.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:213.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:214.
+[value] Done for function mpz_cmp
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:228.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:229.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:230.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:231.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_ui <- main.
+ Called from PROJECT_FILE.i:232.
+[value] Done for function mpz_init_set_ui
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:233.
+[value] Done for function mpz_cmp
+[value] computing for function mpz_init <- main.
+ Called from PROJECT_FILE.i:234.
+[value] Done for function mpz_init
+PROJECT_FILE.i:235:[value] Assertion got status invalid (stopping propagation)..
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:247.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:247.
+[value] Done for function mpz_clear
+PROJECT_FILE.i:250:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:252.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:253.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:253.
+[value] Done for function mpz_cmp
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:262.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:263.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:264.
+[value] Done for function mpz_cmp
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:266.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:267.
+[value] Done for function mpz_clear
+[value] computing for function e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:268.
+[value] computing for function printf <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:115.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:115.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:269.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:269.
+[value] Done for function mpz_clear
+PROJECT_FILE.i:272:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:276.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:276.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:277.
+[value] Done for function mpz_cmp
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:291.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:292.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:293.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:294.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_ui <- main.
+ Called from PROJECT_FILE.i:295.
+[value] Done for function mpz_init_set_ui
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:296.
+[value] Done for function mpz_cmp
+[value] computing for function mpz_init <- main.
+ Called from PROJECT_FILE.i:297.
+[value] Done for function mpz_init
+PROJECT_FILE.i:298:[value] Assertion got status invalid (stopping propagation)..
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:310.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:310.
+[value] Done for function mpz_clear
+[value] Recording results for main
+[value] done for function main
+[from] Computing for function mpz_init_set_si
+[from] Done for function mpz_init_set_si
+[from] Computing for function mpz_cmp
+[from] Done for function mpz_cmp
+[from] Computing for function mpz_clear
+[from] Done for function mpz_clear
+[from] Computing for function e_acsl_fail
+[from] Computing for function printf <-e_acsl_fail
+[from] Done for function printf
+PROJECT_FILE.i:115:[from] warning: variadic call detected. Using only 1 argument(s).
+[from] Computing for function exit <-e_acsl_fail
+[from] Done for function exit
+PROJECT_FILE.i:115:[from] Non terminating function (no dependencies)
+[from] Done for function e_acsl_fail
+[from] Computing for function mpz_init_set_ui
+[from] Done for function mpz_init_set_ui
+[from] Computing for function mpz_init
+[from] Done for function mpz_init
+[dominators] computing for function main
+[dominators] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values for function e_acsl_fail:
+ NON TERMINATING FUNCTION
+[value] Values for function main:
+ __retres ∈ {0}
+ x ∈ {0}
+ y ∈ {1}
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct mpz_t[1];
+/*@ ensures \valid(\old(x));
+ assigns *x; */
+extern void mpz_init(__mpz_struct * /*[1]*/ x);
+/*@ ensures \valid(\old(z));
+ assigns *z; */
+extern void mpz_init_set_ui(__mpz_struct * /*[1]*/ z, unsigned long n);
+/*@ ensures \valid(\old(z));
+ assigns *z; */
+extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+/*@ requires \valid(x);
+ assigns *x; */
+extern void mpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern int mpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+*/
+extern void mpz_cdiv_q(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2,
+ __mpz_struct const * /*[1]*/ z3);
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+/*@ assigns \nothing; */
+extern int printf(char const * , ...);
+void e_acsl_fail(char *msg)
+{
+ printf("%s\n",msg);
+ exit(1);
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int x;
+ int y;
+ x = 0;
+ y = 1;
+ /*@ assert x ≡ 0 ∧ y ≡ 1; */ ;
+ { mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3; int e_acsl_7;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
+ 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));
+ } else { e_acsl_7 = 0; }
+ if (! e_acsl_7) { e_acsl_fail((char *)"(x == 0 && y == 1)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_1));
+ mpz_clear((__mpz_struct *)(e_acsl_2));
+ }
+
+ /*@ 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_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));
+ /*@ 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;
+ 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));
+ }
+
+ /*@ 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; }
+ 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));
+ }
+
+ /*@ 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; }
+ 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);
+ 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));
+ 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));
+ }
+
+ /*@ 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; }
+ else {
+ mpz_t e_acsl_83;
+ mpz_t e_acsl_84;
+ int e_acsl_85;
+ 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_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));
+ }
+
+ __retres = 0;
+ return (__retres);
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
index 949615fa8563f6652b84ea48e80b8231285a53e0..284b88b7f17f480cf648c46434baf59ccc8df55e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
@@ -2,13 +2,14 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE.i:121:[value] Assertion got status valid.
+PROJECT_FILE.i:122:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[dominators] computing for function main
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
+ __retres ∈ {0}
x ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
@@ -24,17 +25,19 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
int x;
x = 0;
/*@ assert x ≡ 0; */ ;
- if (x != 0) { e_acsl_fail((char *)"(x == 0)"); }
+ if (! (x == 0)) { e_acsl_fail((char *)"(x == 0)"); }
if (x) {
/*@ assert x ≢ 0; */ ;
- if (x == 0) { e_acsl_fail((char *)"(x != 0)"); }
+ if (! (x != 0)) { e_acsl_fail((char *)"(x != 0)"); }
}
- return;
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
index 0575aa4d4633432478909611e562497d5e1c20c2..40c2d4ed02de5d21ce1042f0eecc42f0e7d6917b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
@@ -30,9 +30,9 @@ void main(void)
int x;
x = 0;
/*@ assert sizeof(int) ≡ sizeof(x); */ ;
- if (4 != 4) { e_acsl_fail((char *)"(sizeof(int) == sizeof(x))"); }
+ if (! (4 == 4)) { e_acsl_fail((char *)"(sizeof(int) == sizeof(x))"); }
/*@ assert sizeof("totototototo") ≡ sizeof(char *); */ ;
- if (4 != 4) {
+ if (! (4 == 4)) {
e_acsl_fail((char *)"(sizeof(\"totototototo\") == sizeof(char *))");
}
return;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle
index 25b94eba62ee3c1ce36d547ce1b0a74514ee1987..ad4b417cca10295f129d6ef3756158ce62da72c8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle
@@ -2,13 +2,14 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE.i:119:[value] Assertion got status valid.
+PROJECT_FILE.i:120:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[dominators] computing for function main
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
+ __retres ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
ensures \false;
@@ -23,11 +24,14 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
/*@ assert "toto" ≢ "titi"; */ ;
- if ("toto" == "titi") { e_acsl_fail((char *)"(\"toto\" != \"titi\")"); }
- return;
+ if (! ("toto" != "titi")) { e_acsl_fail((char *)"(\"toto\" != \"titi\")");
+ }
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
index 9b549e85bb577ea64d5a856efe854b38c02cf590..33ec1631826643fb4ac9c02105ded5de1ca7cb80 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
@@ -2,13 +2,14 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE.i:121:[value] Assertion got status valid.
+PROJECT_FILE.i:122:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[dominators] computing for function main
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
+ __retres ∈ {0}
x ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
@@ -24,12 +25,14 @@ void e_acsl_fail(char *msg)
return;
}
-void main(void)
+int main(void)
{
+ int __retres;
int x;
x = 0;
/*@ assert \true; */ ;
- return;
+ __retres = 0;
+ return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i b/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i
index cfa24130520d49e2fc6e87bbec366f6bac49a928..2ab8aa953abf78ee8ada641f5bda0b3df5263d93 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i
@@ -1,7 +1,8 @@
/* run.config
COMMENT: string literal
- EXECNOW: LOG gen_string_literal.c BIN gen_string_literal.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/string_literal.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_string_literal.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_string_literal.out ./tests/e-acsl-runtime/result/gen_string_literal.c
+ EXECNOW: LOG gen_string_literal.c BIN gen_string_literal.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/string_literal.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_string_literal.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_string_literal.out ./tests/e-acsl-runtime/result/gen_string_literal.c && ./tests/e-acsl-runtime/result/gen_string_literal.out
*/
-void main() {
+int main(void) {
/*@ assert "toto" != "titi"; */
+ return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/true.i b/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
index 83615a256eddd2be21296f3c67ecf20dcdcda67d..de30c16fa19864578f164842f1ccf8444c28714d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
@@ -1,8 +1,9 @@
/* run.config
COMMENT: assert \true
- EXECNOW: LOG gen_true.c BIN gen_true.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/true.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_true.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_true.out ./tests/e-acsl-runtime/result/gen_true.c
+ EXECNOW: LOG gen_true.c BIN gen_true.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/true.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_true.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_true.out ./tests/e-acsl-runtime/result/gen_true.c && ./tests/e-acsl-runtime/result/gen_true.out
*/
-void main() {
+int main(void) {
int x = 0;
/*@ assert \true; */
+ return 0;
}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 1c94e1b5f5c629cb2d98a27713dba74f19518094..0b4a82831c4f28992977038a5f4e7317f1e26779 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -106,6 +106,24 @@ end
(* ************************************************************************** *)
(* Environments *)
(* ************************************************************************** *)
+(*
+module New_block : sig
+ val is_empty: unit -> bool
+ val push: stmt -> unit
+ val finalize: stmt -> block
+end = struct
+
+ let stmts = ref []
+
+ let push s = stmts := s :: !stmts
+ let is_empty () = !stmts = []
+
+ let finalize s =
+ let l = s :: !stmts in
+ stmts := [];
+ mkBlock (List.rev l)
+
+end
module New_vars: sig
@@ -116,12 +134,11 @@ module New_vars: sig
(varinfo -> exp (* the var as exp *) -> stmt list) -> exp
(* the closure as argument indicates how to initialize the given varinfo *)
- val finalize: unit -> (varinfo * exp * stmt list * bool) list
+ val finalize: unit -> (varinfo * exp * bool) list
(* return the environment and reset it in order to be used again.
Each item of the returned list contains:
- the generated varinfo
- a C expression corresponding to this varinfo
- - a list of stmts initializing the varinfo to the right value
- a boolean which is true iff the generated varinfo is a mpz_t variable. *)
end = struct
@@ -150,7 +167,9 @@ end = struct
ty
in
let e = new_lval v in
- vlist := (v, e, mk_stmts v e, is_t) :: !vlist;
+ let stmts = mk_stmts v e in
+ List.iter New_block.push stmts;
+ vlist := (v, e, is_t) :: !vlist;
e
let push ty mk_stmts = push_list ty (fun v e -> mk_stmts v e)
@@ -166,31 +185,102 @@ end = struct
end
-module New_block : sig
- val is_empty: unit -> bool
- val push: stmt -> unit
- val finalize: stmt -> block
-end = struct
-
- let slist = ref []
-
- let push s = slist := s :: !slist
- let is_empty () = !slist = []
-
- let finalize s =
- let l = !slist @ [ s ] in
- slist := [];
- mkBlock l
-
-end
-
-module New_annotation : sig
+module New_annotations : sig
val push: stmt -> predicate named -> unit
val finalize : (unit -> unit) Queue.t -> unit
end = struct
let q = Queue.create ()
let push s p = Queue.add (fun () -> Annotations.add_assert s [ !self ] p) q
let finalize dest_q = Queue.transfer q dest_q
+end
+ *)
+module Env : sig
+ type t
+ val empty: t
+ val new_var:
+ t -> typ -> (varinfo -> exp (* the var as exp *) -> stmt list) -> exp * t
+ (* the closure as argument indicates how to initialize the given varinfo *)
+ val new_var_and_mpz_init:
+ t -> (varinfo -> exp (* the var as exp *) -> stmt list) -> exp * t
+ val create_from: t -> t
+ val merge: from:t -> t -> t
+ val add_stmt: t -> stmt -> t
+ val add_assert: stmt -> predicate named -> unit
+ val register_actions_queue: (unit -> unit) Queue.t -> unit
+ val generated_variables: t -> varinfo list
+ val block : t -> stmt -> block
+ val is_empty: t -> bool
+end = struct
+
+ let queue = ref (Queue.create ())
+ let register_actions_queue q = queue := q
+
+ type t =
+ { var_cpt: int;
+ vars: varinfo list;
+ beginning_of_block: stmt list;
+ end_of_block: stmt list }
+
+ 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 merge ~from env = { env with var_cpt = from.var_cpt; vars = from.vars }
+
+ let is_empty env =
+ if env.beginning_of_block = [] then begin
+ assert (env.end_of_block = []);
+ true
+ end else
+ false
+
+ let add_stmt env s =
+ { env with beginning_of_block = s :: env.beginning_of_block }
+
+ let add_assert s p =
+ Queue.add (fun () -> Annotations.add_assert s [ !self ] p) !queue
+
+ let new_var env ty mk_stmts =
+ let is_t = Mpz.is_t ty in
+ if is_t then Mpz.is_now_referenced ();
+ let n = succ env.var_cpt in
+ let v =
+ makeVarinfo
+ ~logic:false
+ ~generated:true
+ false (* is a global? *)
+ false (* is a formal? *)
+ ("e_acsl_" ^ string_of_int n)
+ ty
+ in
+ let e = new_lval v in
+ let stmts = mk_stmts v e in
+ e,
+ { var_cpt = n;
+ vars = v :: env.vars;
+ beginning_of_block =
+ List.fold_left (fun l s -> s :: l) env.beginning_of_block stmts;
+ end_of_block =
+ if is_t then Mpz.clear e :: env.end_of_block else env.end_of_block }
+
+ let new_var_and_mpz_init env mk_stmts =
+ new_var env Mpz.t (fun v e -> Mpz.init e :: mk_stmts v e)
+
+ let generated_variables env = List.rev env.vars
+
+ let block env s =
+ let b =
+ mkBlock
+ (List.rev env.beginning_of_block @ [ s ] @ List.rev env.end_of_block)
+ in
+ b.blocals <- b.blocals @ List.rev env.vars;
+ b
+
end
(* ************************************************************************** *)
@@ -215,82 +305,87 @@ let tlval_to_lval = function
| TVar { lv_origin = Some v }, TNoOffset -> Var v, NoOffset
| _ -> not_yet "complex left value"
-let relation_to_revbinop = function
- | Rlt -> Ge
- | Rgt -> Le
- | Rle -> Gt
- | Rge -> Lt
- | Req -> Ne
- | Rneq -> Eq
+let relation_to_binop = function
+ | Rlt -> Lt
+ | Rgt -> Gt
+ | Rle -> Le
+ | Rge -> Ge
+ | Req -> Eq
+ | Rneq -> Ne
let name_of_mpz_arith_bop = function
| PlusA -> "mpz_add"
| MinusA -> "mpz_sub"
| Mult -> "mpz_mul"
| Div -> "mpz_cdiv_q"
- | Mod -> "mpz_mod"
+ | Mod -> "mpz_mod_ui"
| Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
| Shiftlt | Shiftrt | PlusPI | IndexPI | MinusPI | MinusPP -> assert false
-let wrap_leaf e = function
- | Ctype _ -> e
+let wrap_leaf env e = function
+ | Ctype _ -> e, env
| Ltype _ -> not_yet "term from an user defined type"
| Lvar _ -> not_yet "polymorphic term"
- | Linteger -> New_vars.push Mpz.t (fun _ v -> [ Mpz.init_set v e ])
+ | Linteger -> Env.new_var env Mpz.t (fun _ v -> [ Mpz.init_set v e ])
| Lreal -> not_yet "real number"
| Larrow _ -> not_yet "logic function"
-let rec term_to_exp t =
+let rec term_to_exp env t =
let loc = t.term_loc in
match t.term_node with
- | TConst c -> wrap_leaf (constant_to_exp ~loc c) t.term_type
- | TLval lv -> wrap_leaf (new_exp ~loc (Lval (tlval_to_lval lv))) t.term_type
- | TSizeOf ty -> sizeOf ~loc ty
+ | TConst c -> wrap_leaf env (constant_to_exp ~loc c) t.term_type
+ | TLval lv ->
+ wrap_leaf env (new_exp ~loc (Lval (tlval_to_lval lv))) t.term_type
+ | TSizeOf ty -> sizeOf ~loc ty, env
| TSizeOfE t ->
- let e = term_to_exp t in
- sizeOf ~loc (typeOf e)
- | TSizeOfStr s -> new_exp ~loc (SizeOfStr s)
- | TAlignOf ty -> new_exp ~loc (AlignOf ty)
+ let e, env = term_to_exp env t in
+ sizeOf ~loc (typeOf e), env
+ | TSizeOfStr s -> new_exp ~loc (SizeOfStr s), env
+ | TAlignOf ty -> new_exp ~loc (AlignOf ty), env
| TAlignOfE t ->
- let e = term_to_exp t in
- new_exp ~loc (AlignOfE e)
+ let e, env = term_to_exp env t in
+ new_exp ~loc (AlignOfE e), env
| TUnOp(Neg | BNot as op, t) ->
- let e = term_to_exp t in
+ let e, env = term_to_exp env t in
assert (Mpz.e_got_t e);
let name = match op with
| Neg -> "mpz_neg"
| BNot -> "mpz_com"
| LNot -> assert false
in
- New_vars.push_and_mpz_init (fun _ ev -> [ mk_call ~loc name [ ev; e ] ])
+ Env.new_var_and_mpz_init env (fun _ ev -> [ mk_call ~loc name [ ev; e ] ])
| TUnOp(LNot, t) ->
- let e = term_to_exp t in
+ let e, env = term_to_exp env t in
let ty = typeOf e in
assert (not (Mpz.is_t ty));
- new_exp ~loc (UnOp(LNot, e, ty))
+ new_exp ~loc (UnOp(LNot, e, ty)), env
| TBinOp(PlusA | MinusA | Mult | Div | Mod as bop, t1, t2) ->
(* arithmetic binary operator *)
- let e1 = term_to_exp t1 in
- let e2 = term_to_exp t2 in
+ let e1, env = term_to_exp env t1 in
+ let e2, env = term_to_exp env t2 in
assert (Cil_datatype.Typ.equal (typeOf e1) (typeOf e2));
let name = name_of_mpz_arith_bop bop in
(* guarding divisions and modulos *)
+ let zero = Logic_const.tinteger 0 in
+ let guard, env = match bop with
+ | Div | Mod ->
+ comparison_to_exp env Eq t2 zero
+ | _ -> Cil_datatype.Exp.dummy, env
+ in
let mk_stmts _ e =
let call = mk_call ~loc name [ e; e1; e2 ] in
match bop with
| Div | Mod ->
- let z = Logic_const.tinteger 0 in
- let guard = comparison_to_exp Eq t2 z in
- let cond = mk_if guard (Logic_const.prel (Req, t2, z)) in
- New_annotation.push cond (Logic_const.prel (Rneq, t2, z));
+ let cond = mk_if guard (Logic_const.prel (Req, t2, zero)) in
+ Env.add_assert cond (Logic_const.prel (Rneq, t2, zero));
[ cond; call ]
| _ ->
[ call ]
in
- New_vars.push_and_mpz_init mk_stmts
+ Env.new_var_and_mpz_init env mk_stmts
| TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
(* comparison operators *)
- comparison_to_exp ~loc bop t1 t2
+ comparison_to_exp ~loc env bop t1 t2
| TBinOp((Shiftlt | Shiftrt), _, _) ->
(* left/right shift *)
not_yet "left/right shift"
@@ -300,19 +395,19 @@ let rec term_to_exp t =
| TBinOp(PlusPI | IndexPI | MinusPI | MinusPP as bop, t1, t2) ->
(* binary operation over pointers *)
(* [TODO] untested *)
- let e1 = term_to_exp t1 in
- let e2 = term_to_exp t2 in
+ let e1, env = term_to_exp env t1 in
+ let e2, env = term_to_exp env t2 in
Options.warning ~current:true ~once:true
"missing guard for ensuring that %a is a valid pointer"
d_term t;
(* the type of the result is the same than type of the pointer [e1],
whatever is [e2] *)
- new_exp ~loc (BinOp(bop, e1, e2, typeOf e1))
+ new_exp ~loc (BinOp(bop, e1, e2, typeOf e1)), env
| TCastE(ty, t) ->
(* [TODO] missing guard for ensuring no overflow when casting *)
- let e = term_to_exp t in
- mkCast e ty
- | TAddrOf lv -> mkAddrOf ~loc (tlval_to_lval lv)
+ let e, env = term_to_exp env t in
+ mkCast e ty, env
+ | TAddrOf lv -> mkAddrOf ~loc (tlval_to_lval lv), env
| TStartOf _ -> not_yet "beginning of an array"
| Tapp _ -> not_yet "applying logic function"
| Tlambda _ -> not_yet "functional"
@@ -334,39 +429,74 @@ let rec term_to_exp t =
| Trange _ -> not_yet "range"
| Tlet _ -> not_yet "let binding"
-and comparison_to_exp ?(loc=Location.unknown) bop t1 t2 =
- let e1 = term_to_exp t1 in
- let e2 = term_to_exp t2 in
+and comparison_to_exp ?(loc=Location.unknown) env bop t1 t2 =
+ let e1, env = term_to_exp env t1 in
+ let e2, env = term_to_exp env t2 in
(* Options.feedback "ty1=%a; ty2=%a" d_type (typeOf e1) d_type (typeOf e2);*)
assert (Cil_datatype.Typ.equal (typeOf e1) (typeOf e2));
if Mpz.e_got_t e1 then
- let e =
- New_vars.push
+ let e, env =
+ Env.new_var
+ env
intType
(fun v _ -> [ mk_call ~result:(var v) "mpz_cmp" [ e1; e2 ] ])
in
- new_exp ?loc (BinOp(bop, e, zero ?loc, intType))
+ new_exp ?loc (BinOp(bop, e, zero ?loc, intType)), env
else
- new_exp ?loc (BinOp(bop, e1, e2, intType))
+ new_exp ?loc (BinOp(bop, e1, e2, intType)), env
(* convert an ACSL named predicate into the opposite C expression (if any).
E.g. \true is converted into 0. *)
-let rec named_predicate_to_revexp p =
+let rec named_predicate_to_exp env p =
let loc = p.loc in
match p.content with
- | Pfalse -> one ~loc
- | Ptrue -> zero ~loc
+ | Pfalse -> zero ~loc, env
+ | Ptrue -> one ~loc, env
| Papp _ -> not_yet "logic function application"
| Pseparated _ -> not_yet "separated"
- | Prel(rel, t1, t2) -> comparison_to_exp ~loc (relation_to_revbinop rel) t1 t2
- | Pand _ -> not_yet "&&"
- | Por _ -> not_yet "||"
+ | Prel(rel, t1, t2) ->
+ comparison_to_exp ~loc env (relation_to_binop rel) t1 t2
+ | Pand(p1, 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 env = Env.merge ~from:env2 env1 in
+ Env.new_var
+ env
+ intType
+ (fun v _ ->
+ let lv = var v in
+ let then_block =
+ let s = mkStmt ~valid_sid:true (Instr (Set(lv, e2, loc))) in
+ if Env.is_empty env2 then mkBlock [ s ] else Env.block env2 s
+ in
+ let else_block =
+ mkBlock [ mkStmt ~valid_sid:true (Instr (Set(lv, zero loc, loc))) ]
+ in
+ [ mkStmt ~valid_sid:true (If(e1, then_block, else_block, loc)) ])
+ | Por(p1, 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 env = Env.merge ~from:env2 env1 in
+ Env.new_var
+ env
+ intType
+ (fun v _ ->
+ let lv = var v in
+ let then_block =
+ mkBlock [ mkStmt ~valid_sid:true (Instr (Set(lv, one loc, loc))) ]
+ in
+ let else_block =
+ let s = mkStmt ~valid_sid:true (Instr (Set(lv, e2, loc))) in
+ if Env.is_empty env2 then mkBlock [ s ] else Env.block env2 s
+ in
+ [ mkStmt ~valid_sid:true (If(e1, then_block, else_block, loc)) ])
| Pxor _ -> not_yet "xor"
- | Pimplies _ -> not_yet "==>"
+ | Pimplies(p1, p2) ->
+ named_predicate_to_exp env (Logic_const.por ((Logic_const.pnot p1), p2))
| Piff _ -> not_yet "<==>"
| Pnot p ->
- let e = named_predicate_to_revexp p in
- new_exp ~loc (UnOp(Neg, e, TInt(IInt, [])))
+ let e, env = named_predicate_to_exp env p in
+ new_exp ~loc (UnOp(LNot, e, TInt(IInt, []))), env
| Pif _ -> not_yet "_ ? _ : _"
| Plet _ -> not_yet "let _ = _ in _"
| Pforall _ -> not_yet "\\forall"
@@ -383,14 +513,15 @@ let rec named_predicate_to_revexp p =
statement (if any) for runtime assertion checking *)
(* ************************************************************************** *)
-let convert_named_predicate p =
- let e = named_predicate_to_revexp p in
- New_block.push (mk_if e p)
+let convert_named_predicate env p =
+ let e, env = named_predicate_to_exp env p in
+ assert (Typ.equal (typeOf e) intType);
+ Env.add_stmt env (mk_if (new_exp ~loc:e.eloc (UnOp(LNot, e, intType))) p)
-let convert_annotation annot =
+let convert_annotation env annot =
try
match annot.annot_content with
- | AAssert(_l, p) -> convert_named_predicate p
+ | AAssert(_l, p) -> convert_named_predicate env p
| AStmtSpec _ -> not_yet "stmt spec"
| AInvariant _ -> not_yet "invariant"
| AVariant _ -> not_yet "variant"
@@ -399,9 +530,10 @@ let convert_annotation annot =
with Typing_error s ->
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
+ else Options.warning ~current:true "%s@\nignoring annotation." msg;
+ env
-let convert_rooted (User a | AI(_, a)) = convert_annotation a
+let convert_rooted env (User a | AI(_, a)) = convert_annotation env a
(* ************************************************************************** *)
(* Visitor *)
@@ -436,32 +568,24 @@ class e_acsl_visitor prj generate = object (self)
method vstmt_aux stmt =
(* Options.debug ~level:2 "proceeding stmt %d@." stmt.sid;*)
- Annotations.single_iter_stmt (fun ba -> convert_rooted ba) stmt;
- (* new_block and new_vars is set by [convert_rooted] *)
- let is_empty_block = New_block.is_empty () in
- let new_vars = New_vars.finalize () in
- match is_empty_block, new_vars with
- | true, [] -> DoChildren
- | true, _ :: _ -> assert false
- | false, _ ->
+ let env =
+ Annotations.single_fold_stmt
+ (fun ba env -> convert_rooted env ba)
+ stmt
+ Env.empty
+ in
+ if Env.is_empty env then DoChildren
+ else begin
assert generate;
let mk_block stmt =
- let b = New_block.finalize stmt in
- let vars, clears =
- List.fold_left
- (fun (vars, clears) (v, e, stmts, must_clear) ->
- b.blocals <- v :: b.blocals;
- b.bstmts <- stmts @ b.bstmts;
- v :: vars, if must_clear then Mpz.clear e :: clears else clears)
- ([], [])
- new_vars
- in
- gen_vars <- vars;
- b.bstmts <- b.bstmts @ clears;
- New_annotation.finalize self#get_filling_actions;
- mkStmt ~valid_sid:true (Block b)
+ gen_vars <- Env.generated_variables env;
+ mkStmt ~valid_sid:true (Block (Env.block env stmt))
in
ChangeDoChildrenPost(stmt, mk_block)
+ end
+
+ initializer Env.register_actions_queue self#get_filling_actions
+
end