diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index a9995b1e776e9dc996e3102060fe0699ac18be08..90583c9f754d08f3fc1d2b898cc13a1c3a4afe6e 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -21,12 +21,10 @@
#########
- stmt_contracts et only_behaviors... pas sur que je fasse ce qu'il faut
-- tester les opérations binaires sur les pointeurs (requiert complex left value)
- tester plusieurs fonctions contenant des annotations
- améliorer test "integer_constant.i" quand bug fixed #745
-- améliorer test "arith.i" quand bug fixed #751
-- améliorer test "ptr.i" quand bug fixed #751
- test sizeof.i devraient être plus précis quand logic_typing plus précis
+- !integer: probably broken (TODO dans le code)
- structs
- unions
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 9232fe25d4cf20db9523acfd04f084020025c1f2..4bb84237ff31592df0626d8400edf0386ea2ef68 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
@@ -16,6 +16,7 @@ int main(void) {
/*@ assert x-1 == -4; */ ;
/*@ assert x*3 == -9; */ ;
/*@ assert x/3 == -1; */ ;
+ /*@ assert 0xfffffffffff/0xfffffffffff == 1; */ ;
/*@ assert x % 2 == -1; */ ;
/*@ assert x * 2 + (3 + y) - 4 + (x - y) == -10; */ ;
@@ -25,9 +26,7 @@ int main(void) {
/*@ assert (0 >= -1) == (0 <= 0); */ ;
/*@ assert (0 != 1) == !(0 != 0); */ ;
- // /*@ assert 0 == !1; */ ;
- /* subtyping relation: 0 should be promoted to boolean below
- How to handle this? See BTS #751 */
+ /*@ assert 0 == !1; */ ;
return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i b/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i
index 7d5b6038a8e3e309da18f0febc2d62661a9fffb9..4c8ebbd755e7ecfafba237c52eef54b9363fd9fb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: predicate using lazy operators
- EXECNOW: LOG gen_lazy.c BIN gen_lazy.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/lazy.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_lazy.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_lazy.out -lgmp ./tests/e-acsl-runtime/result/gen_lazy.c && ./tests/e-acsl-runtime/result/gen_lazy.out
+ EXECNOW: LOG gen_lazy.c BIN gen_lazy.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/lazy.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_lazy.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_lazy.out -lgmp ./tests/e-acsl-runtime/result/gen_lazy.c 2> /dev/null && ./tests/e-acsl-runtime/result/gen_lazy.out
*/
int main(void) {
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 3853a271ca5609c5398c3950729ec3cc573b2bbc..e1823cd42647abb82fd31b77339c8aa95b8870e3 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
@@ -1,3 +1,4 @@
+:0:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
@@ -277,35 +278,49 @@ PROJECT_FILE.i:74:[value] Function mpz_mul: precondition got status valid
[value] Done for function mpz_clear
PROJECT_FILE.i:197:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:199.
+ Called from PROJECT_FILE.i:200.
[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_get_si <- main.
+ Called from PROJECT_FILE.i:201.
+PROJECT_FILE.i:92:[value] Function mpz_get_si: precondition got status valid
+[value] Done for function mpz_get_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:200.
+ Called from PROJECT_FILE.i:201.
[value] Done for function mpz_init
-PROJECT_FILE.i:201:[value] Assertion got status valid.
-[value] computing for function mpz_cdiv_q <- main.
+PROJECT_FILE.i:202:[value] Assertion got status valid.
+[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:203.
+[value] computing for function printf <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:125.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:125.
+[value] Done for function exit
+[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:204.
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:203.
+ Called from PROJECT_FILE.i:204.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:204.
+ Called from PROJECT_FILE.i:205.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:204.
+ Called from PROJECT_FILE.i:205.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:205.
+ Called from PROJECT_FILE.i:206.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:206.
+ Called from PROJECT_FILE.i:207.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -315,49 +330,124 @@ 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:207.
+ Called from PROJECT_FILE.i:208.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:207.
+ Called from PROJECT_FILE.i:208.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:207.
+ Called from PROJECT_FILE.i:208.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:208.
+ Called from PROJECT_FILE.i:209.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:208.
+ Called from PROJECT_FILE.i:209.
+[value] Done for function mpz_clear
+PROJECT_FILE.i:212:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_str <- main.
+ Called from PROJECT_FILE.i:215.
+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:216.
+[value] Done for function mpz_init_set_str
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:217.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:217.
+[value] Done for function mpz_cmp
+[value] computing for function mpz_init <- main.
+ Called from PROJECT_FILE.i:218.
+[value] Done for function mpz_init
+PROJECT_FILE.i:219:[value] Assertion got status valid.
+[value] computing for function e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:220.
+[value] computing for function printf <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:125.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:125.
+[value] Done for function exit
+[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:221.
+[value] Done for function mpz_cdiv_q
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:221.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:222.
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:224.
+[value] computing for function printf <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:125.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:125.
+[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:225.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:225.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:225.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:226.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:226.
[value] Done for function mpz_clear
-PROJECT_FILE.i:211:[value] Assertion got status valid.
+PROJECT_FILE.i:229:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:213.
+ Called from PROJECT_FILE.i:232.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:214.
+ Called from PROJECT_FILE.i:232.
[value] Done for function mpz_init_set_si
+[value] computing for function mpz_get_si <- main.
+ Called from PROJECT_FILE.i:233.
+[value] Done for function mpz_get_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:214.
+ Called from PROJECT_FILE.i:233.
[value] Done for function mpz_init
-PROJECT_FILE.i:215:[value] Assertion got status valid.
+PROJECT_FILE.i:234:[value] Assertion got status valid.
+[value] computing for function e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:235.
+[value] computing for function printf <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:125.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:125.
+[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_ui <- main.
- Called from PROJECT_FILE.i:217.
+ Called from PROJECT_FILE.i:236.
[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:217.
+ Called from PROJECT_FILE.i:236.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:218.
+ Called from PROJECT_FILE.i:237.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:218.
+ Called from PROJECT_FILE.i:237.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:219.
+ Called from PROJECT_FILE.i:238.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:220.
+ Called from PROJECT_FILE.i:239.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -367,92 +457,92 @@ PROJECT_FILE.i:215:[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:221.
+ Called from PROJECT_FILE.i:240.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:221.
+ Called from PROJECT_FILE.i:240.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:221.
+ Called from PROJECT_FILE.i:240.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:222.
+ Called from PROJECT_FILE.i:241.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:222.
+ Called from PROJECT_FILE.i:241.
[value] Done for function mpz_clear
-PROJECT_FILE.i:225:[value] Assertion got status valid.
+PROJECT_FILE.i:244:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:230.
+ Called from PROJECT_FILE.i:249.
[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:249.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:231.
+ Called from PROJECT_FILE.i:250.
[value] Done for function mpz_init
[value] computing for function mpz_mul <- main.
- Called from PROJECT_FILE.i:231.
+ Called from PROJECT_FILE.i:250.
[value] Done for function mpz_mul
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:232.
+ Called from PROJECT_FILE.i:251.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:232.
+ Called from PROJECT_FILE.i:251.
[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:252.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:233.
+ Called from PROJECT_FILE.i:252.
[value] Done for function mpz_add
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:234.
+ Called from PROJECT_FILE.i:253.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:234.
+ Called from PROJECT_FILE.i:253.
[value] Done for function mpz_add
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:235.
+ Called from PROJECT_FILE.i:254.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:235.
+ Called from PROJECT_FILE.i:254.
[value] Done for function mpz_init
[value] computing for function mpz_sub <- main.
- Called from PROJECT_FILE.i:236.
+ Called from PROJECT_FILE.i:255.
[value] Done for function mpz_sub
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:236.
+ Called from PROJECT_FILE.i:255.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:237.
+ Called from PROJECT_FILE.i:256.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:237.
+ Called from PROJECT_FILE.i:256.
[value] Done for function mpz_init
[value] computing for function mpz_sub <- main.
- Called from PROJECT_FILE.i:238.
+ Called from PROJECT_FILE.i:257.
[value] Done for function mpz_sub
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:238.
+ Called from PROJECT_FILE.i:257.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:239.
+ Called from PROJECT_FILE.i:258.
[value] Done for function mpz_add
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:239.
+ Called from PROJECT_FILE.i:258.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:240.
+ Called from PROJECT_FILE.i:259.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:240.
+ Called from PROJECT_FILE.i:259.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:241.
+ Called from PROJECT_FILE.i:260.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:242.
+ Called from PROJECT_FILE.i:261.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -462,69 +552,69 @@ PROJECT_FILE.i:225:[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:243.
+ Called from PROJECT_FILE.i:262.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:243.
+ Called from PROJECT_FILE.i:262.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:243.
+ Called from PROJECT_FILE.i:262.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:244.
+ Called from PROJECT_FILE.i:263.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:244.
+ Called from PROJECT_FILE.i:263.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:244.
+ Called from PROJECT_FILE.i:263.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:245.
+ Called from PROJECT_FILE.i:264.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:245.
+ Called from PROJECT_FILE.i:264.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:245.
+ Called from PROJECT_FILE.i:264.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:246.
+ Called from PROJECT_FILE.i:265.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:246.
+ Called from PROJECT_FILE.i:265.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:246.
+ Called from PROJECT_FILE.i:265.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:247.
+ Called from PROJECT_FILE.i:266.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:247.
+ Called from PROJECT_FILE.i:266.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:247.
+ Called from PROJECT_FILE.i:266.
[value] Done for function mpz_clear
-PROJECT_FILE.i:250:[value] Assertion got status valid.
-PROJECT_FILE.i:253:[value] Assertion got status valid.
+PROJECT_FILE.i:269:[value] Assertion got status valid.
+PROJECT_FILE.i:272:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:255.
+ 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:255.
+ 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:256.
+ Called from PROJECT_FILE.i:275.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:256.
+ Called from PROJECT_FILE.i:275.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:257.
+ Called from PROJECT_FILE.i:276.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:258.
+ Called from PROJECT_FILE.i:277.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -534,32 +624,32 @@ PROJECT_FILE.i:253:[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:259.
+ Called from PROJECT_FILE.i:278.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:259.
+ Called from PROJECT_FILE.i:278.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:259.
+ Called from PROJECT_FILE.i:278.
[value] Done for function mpz_clear
-PROJECT_FILE.i:262:[value] Assertion got status valid.
+PROJECT_FILE.i:281:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:264.
+ Called from PROJECT_FILE.i:283.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:264.
+ Called from PROJECT_FILE.i:283.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:265.
+ Called from PROJECT_FILE.i:284.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
- Called from PROJECT_FILE.i:265.
+ Called from PROJECT_FILE.i:284.
[value] Done for function mpz_neg
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:266.
+ Called from PROJECT_FILE.i:285.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:268.
+ Called from PROJECT_FILE.i:287.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -569,15 +659,16 @@ PROJECT_FILE.i:262:[value] Assertion got status valid.
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:269.
+ Called from PROJECT_FILE.i:288.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:269.
+ Called from PROJECT_FILE.i:288.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:269.
+ Called from PROJECT_FILE.i:288.
[value] Done for function mpz_clear
-PROJECT_FILE.i:272:[value] Assertion got status valid.
+PROJECT_FILE.i:291:[value] Assertion got status valid.
+PROJECT_FILE.i:294:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[from] Computing for function mpz_init_set_si
@@ -606,8 +697,12 @@ PROJECT_FILE.i:125:[from] Non terminating function (no dependencies)
[from] Done for function mpz_sub
[from] Computing for function mpz_mul
[from] Done for function mpz_mul
+[from] Computing for function mpz_get_si
+[from] Done for function mpz_get_si
[from] Computing for function mpz_cdiv_q
[from] Done for function mpz_cdiv_q
+[from] Computing for function mpz_init_set_str
+[from] Done for function mpz_init_set_str
[from] Computing for function mpz_mod_ui
[from] Done for function mpz_mod_ui
[value] ====== VALUES COMPUTED ======
@@ -631,6 +726,10 @@ extern void mpz_init(__mpz_struct * /*[1]*/ x);
/*@ ensures \valid(\old(z));
assigns *z; */
extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+/*@ ensures \valid(\old(z));
+ assigns *z; */
+extern int mpz_init_set_str(__mpz_struct * /*[1]*/ z, char const *str,
+ int base);
/*@ requires \valid(x);
assigns *x; */
extern void mpz_clear(__mpz_struct * /*[1]*/ x);
@@ -676,6 +775,9 @@ 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(z);
+ assigns \nothing; */
+extern long mpz_get_si(__mpz_struct const * /*[1]*/ z);
/*@ terminates \false;
ensures \false;
assigns \nothing; */
@@ -807,100 +909,127 @@ int main(void)
}
/*@ assert x/3 ≡ -1; */ ;
- { mpz_t e_acsl_31; mpz_t e_acsl_32; mpz_t e_acsl_33; mpz_t e_acsl_34;
- mpz_t e_acsl_35; int e_acsl_36;
+ { mpz_t e_acsl_31; mpz_t e_acsl_32; int e_acsl_33; mpz_t e_acsl_34;
+ mpz_t e_acsl_35; mpz_t e_acsl_36; int e_acsl_37;
mpz_init_set_si((__mpz_struct *)(e_acsl_31),(long)x);
mpz_init_set_si((__mpz_struct *)(e_acsl_32),(long)3);
- mpz_init((__mpz_struct *)(e_acsl_33)); /*@ assert 3 ≢ 0; */ ;
- if (3 == 0) { e_acsl_fail((char *)"(3 == 0)"); }
- mpz_cdiv_q((__mpz_struct *)(e_acsl_33),(__mpz_struct const *)(e_acsl_31),
+ e_acsl_33 = (int)mpz_get_si((__mpz_struct const *)(e_acsl_32));
+ mpz_init((__mpz_struct *)(e_acsl_34)); /*@ assert 3 ≢ 0; */ ;
+ if (e_acsl_33 == 0) { e_acsl_fail((char *)"(3 == 0)"); }
+ mpz_cdiv_q((__mpz_struct *)(e_acsl_34),(__mpz_struct const *)(e_acsl_31),
(__mpz_struct const *)(e_acsl_32));
- mpz_init_set_si((__mpz_struct *)(e_acsl_34),(long)1);
- mpz_init((__mpz_struct *)(e_acsl_35));
- mpz_neg((__mpz_struct *)(e_acsl_35),(__mpz_struct const *)(e_acsl_34));
- e_acsl_36 = mpz_cmp((__mpz_struct const *)(e_acsl_33),
- (__mpz_struct const *)(e_acsl_35));
- if (! (e_acsl_36 == 0)) { e_acsl_fail((char *)"(x/3 == -1)"); }
+ mpz_init_set_si((__mpz_struct *)(e_acsl_35),(long)1);
+ mpz_init((__mpz_struct *)(e_acsl_36));
+ mpz_neg((__mpz_struct *)(e_acsl_36),(__mpz_struct const *)(e_acsl_35));
+ e_acsl_37 = mpz_cmp((__mpz_struct const *)(e_acsl_34),
+ (__mpz_struct const *)(e_acsl_36));
+ if (! (e_acsl_37 == 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));
mpz_clear((__mpz_struct *)(e_acsl_34));
mpz_clear((__mpz_struct *)(e_acsl_35));
+ mpz_clear((__mpz_struct *)(e_acsl_36));
}
- /*@ assert x%2 ≡ -1; */ ;
- { mpz_t e_acsl_37; mpz_t e_acsl_38; mpz_t e_acsl_39; mpz_t e_acsl_40;
- mpz_t e_acsl_41; int e_acsl_42;
- mpz_init_set_si((__mpz_struct *)(e_acsl_37),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_38),(long)2);
- mpz_init((__mpz_struct *)(e_acsl_39)); /*@ assert 2 ≢ 0; */ ;
- if (2 == 0) { e_acsl_fail((char *)"(2 == 0)"); }
- mpz_mod_ui(e_acsl_39,e_acsl_37,e_acsl_38);
- mpz_init_set_si((__mpz_struct *)(e_acsl_40),(long)1);
- mpz_init((__mpz_struct *)(e_acsl_41));
- mpz_neg((__mpz_struct *)(e_acsl_41),(__mpz_struct const *)(e_acsl_40));
- e_acsl_42 = mpz_cmp((__mpz_struct const *)(e_acsl_39),
- (__mpz_struct const *)(e_acsl_41));
- if (! (e_acsl_42 == 0)) { e_acsl_fail((char *)"(x%2 == -1)"); }
- mpz_clear((__mpz_struct *)(e_acsl_37));
- mpz_clear((__mpz_struct *)(e_acsl_38));
+ /*@ assert 0xfffffffffff/0xfffffffffff ≡ 1; */ ;
+ { mpz_t e_acsl_38; mpz_t e_acsl_39; mpz_t e_acsl_40; int e_acsl_41;
+ mpz_t e_acsl_42; mpz_t e_acsl_43; int e_acsl_44;
+ mpz_init_set_str((__mpz_struct *)(e_acsl_38),"17592186044415",10);
+ mpz_init_set_str((__mpz_struct *)(e_acsl_39),"17592186044415",10);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_40),(long)0);
+ e_acsl_41 = mpz_cmp((__mpz_struct const *)(e_acsl_39),
+ (__mpz_struct const *)(e_acsl_40));
+ mpz_init((__mpz_struct *)(e_acsl_42));
+ /*@ assert 0xfffffffffff ≢ 0; */ ;
+ if (e_acsl_41 == 0) { e_acsl_fail((char *)"(0xfffffffffff == 0)"); }
+ mpz_cdiv_q((__mpz_struct *)(e_acsl_42),(__mpz_struct const *)(e_acsl_38),
+ (__mpz_struct const *)(e_acsl_39));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_43),(long)1);
+ e_acsl_44 = mpz_cmp((__mpz_struct const *)(e_acsl_42),
+ (__mpz_struct const *)(e_acsl_43));
+ if (! (e_acsl_44 == 0)) {
+ e_acsl_fail((char *)"(0xfffffffffff/0xfffffffffff == 1)");
+ } mpz_clear((__mpz_struct *)(e_acsl_38));
mpz_clear((__mpz_struct *)(e_acsl_39));
mpz_clear((__mpz_struct *)(e_acsl_40));
- mpz_clear((__mpz_struct *)(e_acsl_41));
+ mpz_clear((__mpz_struct *)(e_acsl_42));
+ mpz_clear((__mpz_struct *)(e_acsl_43));
+ }
+
+ /*@ assert x%2 ≡ -1; */ ;
+ { mpz_t e_acsl_45; mpz_t e_acsl_46; int e_acsl_47; mpz_t e_acsl_48;
+ mpz_t e_acsl_49; mpz_t e_acsl_50; int e_acsl_51;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_45),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_46),(long)2);
+ e_acsl_47 = (int)mpz_get_si((__mpz_struct const *)(e_acsl_46));
+ mpz_init((__mpz_struct *)(e_acsl_48)); /*@ assert 2 ≢ 0; */ ;
+ if (e_acsl_47 == 0) { e_acsl_fail((char *)"(2 == 0)"); }
+ mpz_mod_ui(e_acsl_48,e_acsl_45,e_acsl_46);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_49),(long)1);
+ mpz_init((__mpz_struct *)(e_acsl_50));
+ mpz_neg((__mpz_struct *)(e_acsl_50),(__mpz_struct const *)(e_acsl_49));
+ e_acsl_51 = mpz_cmp((__mpz_struct const *)(e_acsl_48),
+ (__mpz_struct const *)(e_acsl_50));
+ if (! (e_acsl_51 == 0)) { e_acsl_fail((char *)"(x%2 == -1)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_45));
+ mpz_clear((__mpz_struct *)(e_acsl_46));
+ mpz_clear((__mpz_struct *)(e_acsl_48));
+ mpz_clear((__mpz_struct *)(e_acsl_49));
+ mpz_clear((__mpz_struct *)(e_acsl_50));
}
/*@ assert ((x*2+(3+y))-4)+(x-y) ≡ -10; */ ;
- { mpz_t e_acsl_43; mpz_t e_acsl_44; mpz_t e_acsl_45; mpz_t e_acsl_46;
- mpz_t e_acsl_47; mpz_t e_acsl_48; mpz_t e_acsl_49; mpz_t e_acsl_50;
- mpz_t e_acsl_51; mpz_t e_acsl_52; mpz_t e_acsl_53; mpz_t e_acsl_54;
- mpz_t e_acsl_55; mpz_t e_acsl_56; mpz_t e_acsl_57; int e_acsl_58;
- mpz_init_set_si((__mpz_struct *)(e_acsl_43),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_44),(long)2);
- mpz_init((__mpz_struct *)(e_acsl_45));
- mpz_mul((__mpz_struct *)(e_acsl_45),(__mpz_struct const *)(e_acsl_43),
- (__mpz_struct const *)(e_acsl_44));
- mpz_init_set_si((__mpz_struct *)(e_acsl_46),(long)3);
- mpz_init_set_si((__mpz_struct *)(e_acsl_47),(long)y);
- mpz_init((__mpz_struct *)(e_acsl_48));
- mpz_add((__mpz_struct *)(e_acsl_48),(__mpz_struct const *)(e_acsl_46),
- (__mpz_struct const *)(e_acsl_47));
- mpz_init((__mpz_struct *)(e_acsl_49));
- mpz_add((__mpz_struct *)(e_acsl_49),(__mpz_struct const *)(e_acsl_45),
- (__mpz_struct const *)(e_acsl_48));
- mpz_init_set_si((__mpz_struct *)(e_acsl_50),(long)4);
- mpz_init((__mpz_struct *)(e_acsl_51));
- mpz_sub((__mpz_struct *)(e_acsl_51),(__mpz_struct const *)(e_acsl_49),
- (__mpz_struct const *)(e_acsl_50));
+ { mpz_t e_acsl_52; mpz_t e_acsl_53; mpz_t e_acsl_54; mpz_t e_acsl_55;
+ mpz_t e_acsl_56; mpz_t e_acsl_57; mpz_t e_acsl_58; mpz_t e_acsl_59;
+ mpz_t e_acsl_60; mpz_t e_acsl_61; mpz_t e_acsl_62; mpz_t e_acsl_63;
+ mpz_t e_acsl_64; mpz_t e_acsl_65; mpz_t e_acsl_66; int e_acsl_67;
mpz_init_set_si((__mpz_struct *)(e_acsl_52),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_53),(long)y);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_53),(long)2);
mpz_init((__mpz_struct *)(e_acsl_54));
- mpz_sub((__mpz_struct *)(e_acsl_54),(__mpz_struct const *)(e_acsl_52),
+ mpz_mul((__mpz_struct *)(e_acsl_54),(__mpz_struct const *)(e_acsl_52),
(__mpz_struct const *)(e_acsl_53));
- mpz_init((__mpz_struct *)(e_acsl_55));
- mpz_add((__mpz_struct *)(e_acsl_55),(__mpz_struct const *)(e_acsl_51),
- (__mpz_struct const *)(e_acsl_54));
- mpz_init_set_si((__mpz_struct *)(e_acsl_56),(long)10);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_55),(long)3);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_56),(long)y);
mpz_init((__mpz_struct *)(e_acsl_57));
- mpz_neg((__mpz_struct *)(e_acsl_57),(__mpz_struct const *)(e_acsl_56));
- e_acsl_58 = mpz_cmp((__mpz_struct const *)(e_acsl_55),
- (__mpz_struct const *)(e_acsl_57));
- if (! (e_acsl_58 == 0)) {
+ mpz_add((__mpz_struct *)(e_acsl_57),(__mpz_struct const *)(e_acsl_55),
+ (__mpz_struct const *)(e_acsl_56));
+ mpz_init((__mpz_struct *)(e_acsl_58));
+ mpz_add((__mpz_struct *)(e_acsl_58),(__mpz_struct const *)(e_acsl_54),
+ (__mpz_struct const *)(e_acsl_57));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_59),(long)4);
+ mpz_init((__mpz_struct *)(e_acsl_60));
+ mpz_sub((__mpz_struct *)(e_acsl_60),(__mpz_struct const *)(e_acsl_58),
+ (__mpz_struct const *)(e_acsl_59));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_61),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_62),(long)y);
+ mpz_init((__mpz_struct *)(e_acsl_63));
+ mpz_sub((__mpz_struct *)(e_acsl_63),(__mpz_struct const *)(e_acsl_61),
+ (__mpz_struct const *)(e_acsl_62));
+ mpz_init((__mpz_struct *)(e_acsl_64));
+ mpz_add((__mpz_struct *)(e_acsl_64),(__mpz_struct const *)(e_acsl_60),
+ (__mpz_struct const *)(e_acsl_63));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_65),(long)10);
+ mpz_init((__mpz_struct *)(e_acsl_66));
+ mpz_neg((__mpz_struct *)(e_acsl_66),(__mpz_struct const *)(e_acsl_65));
+ e_acsl_67 = mpz_cmp((__mpz_struct const *)(e_acsl_64),
+ (__mpz_struct const *)(e_acsl_66));
+ if (! (e_acsl_67 == 0)) {
e_acsl_fail((char *)"(((x*2+(3+y))-4)+(x-y) == -10)");
- } mpz_clear((__mpz_struct *)(e_acsl_43));
- mpz_clear((__mpz_struct *)(e_acsl_44));
- mpz_clear((__mpz_struct *)(e_acsl_45));
- mpz_clear((__mpz_struct *)(e_acsl_46));
- mpz_clear((__mpz_struct *)(e_acsl_47));
- mpz_clear((__mpz_struct *)(e_acsl_48));
- mpz_clear((__mpz_struct *)(e_acsl_49));
- mpz_clear((__mpz_struct *)(e_acsl_50));
- mpz_clear((__mpz_struct *)(e_acsl_51));
- mpz_clear((__mpz_struct *)(e_acsl_52));
+ } mpz_clear((__mpz_struct *)(e_acsl_52));
mpz_clear((__mpz_struct *)(e_acsl_53));
mpz_clear((__mpz_struct *)(e_acsl_54));
mpz_clear((__mpz_struct *)(e_acsl_55));
mpz_clear((__mpz_struct *)(e_acsl_56));
mpz_clear((__mpz_struct *)(e_acsl_57));
+ mpz_clear((__mpz_struct *)(e_acsl_58));
+ mpz_clear((__mpz_struct *)(e_acsl_59));
+ mpz_clear((__mpz_struct *)(e_acsl_60));
+ mpz_clear((__mpz_struct *)(e_acsl_61));
+ mpz_clear((__mpz_struct *)(e_acsl_62));
+ mpz_clear((__mpz_struct *)(e_acsl_63));
+ mpz_clear((__mpz_struct *)(e_acsl_64));
+ mpz_clear((__mpz_struct *)(e_acsl_65));
+ mpz_clear((__mpz_struct *)(e_acsl_66));
}
/*@ assert (0≡1) ≡ !(0≡0); */ ;
@@ -908,39 +1037,43 @@ int main(void)
e_acsl_fail((char *)"((0==1) == !(0==0))");
}
/*@ assert (0≤-1) ≡ (0>0); */ ;
- { mpz_t e_acsl_59; mpz_t e_acsl_60; mpz_t e_acsl_61; int e_acsl_62;
- mpz_init_set_si((__mpz_struct *)(e_acsl_59),(long)0);
- mpz_init_set_si((__mpz_struct *)(e_acsl_60),(long)1);
- mpz_init((__mpz_struct *)(e_acsl_61));
- mpz_neg((__mpz_struct *)(e_acsl_61),(__mpz_struct const *)(e_acsl_60));
- e_acsl_62 = mpz_cmp((__mpz_struct const *)(e_acsl_59),
- (__mpz_struct const *)(e_acsl_61));
- if (! ((e_acsl_62 <= 0) == (0 > 0))) {
+ { mpz_t e_acsl_68; mpz_t e_acsl_69; mpz_t e_acsl_70; int e_acsl_71;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_68),(long)0);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_69),(long)1);
+ mpz_init((__mpz_struct *)(e_acsl_70));
+ mpz_neg((__mpz_struct *)(e_acsl_70),(__mpz_struct const *)(e_acsl_69));
+ e_acsl_71 = mpz_cmp((__mpz_struct const *)(e_acsl_68),
+ (__mpz_struct const *)(e_acsl_70));
+ if (! ((e_acsl_71 <= 0) == (0 > 0))) {
e_acsl_fail((char *)"((0<=-1) == (0>0))");
- } mpz_clear((__mpz_struct *)(e_acsl_59));
- mpz_clear((__mpz_struct *)(e_acsl_60));
- mpz_clear((__mpz_struct *)(e_acsl_61));
+ } mpz_clear((__mpz_struct *)(e_acsl_68));
+ mpz_clear((__mpz_struct *)(e_acsl_69));
+ mpz_clear((__mpz_struct *)(e_acsl_70));
}
/*@ assert (0≥-1) ≡ (0≤0); */ ;
- { mpz_t e_acsl_63; mpz_t e_acsl_64; mpz_t e_acsl_65; int e_acsl_66;
- mpz_init_set_si((__mpz_struct *)(e_acsl_63),(long)0);
- mpz_init_set_si((__mpz_struct *)(e_acsl_64),(long)1);
- mpz_init((__mpz_struct *)(e_acsl_65));
- mpz_neg((__mpz_struct *)(e_acsl_65),(__mpz_struct const *)(e_acsl_64));
- e_acsl_66 = mpz_cmp((__mpz_struct const *)(e_acsl_63),
- (__mpz_struct const *)(e_acsl_65));
- if (! ((e_acsl_66 >= 0) == (0 <= 0))) {
+ { mpz_t e_acsl_72; mpz_t e_acsl_73; mpz_t e_acsl_74; int e_acsl_75;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_72),(long)0);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_73),(long)1);
+ mpz_init((__mpz_struct *)(e_acsl_74));
+ mpz_neg((__mpz_struct *)(e_acsl_74),(__mpz_struct const *)(e_acsl_73));
+ e_acsl_75 = mpz_cmp((__mpz_struct const *)(e_acsl_72),
+ (__mpz_struct const *)(e_acsl_74));
+ if (! ((e_acsl_75 >= 0) == (0 <= 0))) {
e_acsl_fail((char *)"((0>=-1) == (0<=0))");
- } mpz_clear((__mpz_struct *)(e_acsl_63));
- mpz_clear((__mpz_struct *)(e_acsl_64));
- mpz_clear((__mpz_struct *)(e_acsl_65));
+ } mpz_clear((__mpz_struct *)(e_acsl_72));
+ mpz_clear((__mpz_struct *)(e_acsl_73));
+ mpz_clear((__mpz_struct *)(e_acsl_74));
}
/*@ assert (0≢1) ≡ !(0≢0); */ ;
if (! ((0 != 1) == ! (0 != 0))) {
e_acsl_fail((char *)"((0!=1) == !(0!=0))");
}
+ /*@ assert (0≢0) ≡ !(1≢0); */ ;
+ if (! ((0 != 0) == ! (1 != 0))) {
+ e_acsl_fail((char *)"((0!=0) == !(1!=0))");
+ }
__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 fad5da021ca144ce20934d8db1050577975274df..4fc2d516e8e7d8b0dd00033bc5e9347e4c5c291a 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
@@ -58,6 +58,10 @@ __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__));
+/*@ requires \valid(z);
+ assigns \nothing; */
+extern long __gmpz_get_si(__mpz_struct const * /*[1]*/ z) __attribute__((
+__pure__));
__inline static unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z) __attribute__((
__pure__));
__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
@@ -69,6 +73,10 @@ 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 int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z, char const *str,
+ int base);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -714,102 +722,130 @@ int main(void)
}
/*@ assert x/3 ≡ -1; */ ;
- { mpz_t e_acsl_31; mpz_t e_acsl_32; mpz_t e_acsl_33; mpz_t e_acsl_34;
- mpz_t e_acsl_35; int e_acsl_36;
+ { mpz_t e_acsl_31; mpz_t e_acsl_32; int e_acsl_33; mpz_t e_acsl_34;
+ mpz_t e_acsl_35; mpz_t e_acsl_36; int e_acsl_37;
__gmpz_init_set_si((__mpz_struct *)(e_acsl_31),(long)x);
__gmpz_init_set_si((__mpz_struct *)(e_acsl_32),(long)3);
- __gmpz_init((__mpz_struct *)(e_acsl_33)); /*@ assert 3 ≢ 0; */ ;
- if (3 == 0) { e_acsl_fail((char *)"(3 == 0)"); }
- __gmpz_cdiv_q((__mpz_struct *)(e_acsl_33),
+ e_acsl_33 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_32));
+ __gmpz_init((__mpz_struct *)(e_acsl_34)); /*@ assert 3 ≢ 0; */ ;
+ if (e_acsl_33 == 0) { e_acsl_fail((char *)"(3 == 0)"); }
+ __gmpz_cdiv_q((__mpz_struct *)(e_acsl_34),
(__mpz_struct const *)(e_acsl_31),
(__mpz_struct const *)(e_acsl_32));
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_34),(long)1);
- __gmpz_init((__mpz_struct *)(e_acsl_35));
- __gmpz_neg((__mpz_struct *)(e_acsl_35),(__mpz_struct const *)(e_acsl_34));
- e_acsl_36 = __gmpz_cmp((__mpz_struct const *)(e_acsl_33),
- (__mpz_struct const *)(e_acsl_35));
- if (! (e_acsl_36 == 0)) { e_acsl_fail((char *)"(x/3 == -1)"); }
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_35),(long)1);
+ __gmpz_init((__mpz_struct *)(e_acsl_36));
+ __gmpz_neg((__mpz_struct *)(e_acsl_36),(__mpz_struct const *)(e_acsl_35));
+ e_acsl_37 = __gmpz_cmp((__mpz_struct const *)(e_acsl_34),
+ (__mpz_struct const *)(e_acsl_36));
+ if (! (e_acsl_37 == 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));
__gmpz_clear((__mpz_struct *)(e_acsl_34));
__gmpz_clear((__mpz_struct *)(e_acsl_35));
+ __gmpz_clear((__mpz_struct *)(e_acsl_36));
}
- /*@ assert x%2 ≡ -1; */ ;
- { mpz_t e_acsl_37; mpz_t e_acsl_38; mpz_t e_acsl_39; mpz_t e_acsl_40;
- mpz_t e_acsl_41; int e_acsl_42;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_37),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_38),(long)2);
- __gmpz_init((__mpz_struct *)(e_acsl_39)); /*@ assert 2 ≢ 0; */ ;
- if (2 == 0) { e_acsl_fail((char *)"(2 == 0)"); }
- __gmpz_fdiv_r_ui(e_acsl_39,(__mpz_struct const *)(e_acsl_37),
- (unsigned long)(e_acsl_38));
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_40),(long)1);
- __gmpz_init((__mpz_struct *)(e_acsl_41));
- __gmpz_neg((__mpz_struct *)(e_acsl_41),(__mpz_struct const *)(e_acsl_40));
- e_acsl_42 = __gmpz_cmp((__mpz_struct const *)(e_acsl_39),
- (__mpz_struct const *)(e_acsl_41));
- if (! (e_acsl_42 == 0)) { e_acsl_fail((char *)"(x%2 == -1)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_37));
- __gmpz_clear((__mpz_struct *)(e_acsl_38));
+ /*@ assert 0xfffffffffff/0xfffffffffff ≡ 1; */ ;
+ { mpz_t e_acsl_38; mpz_t e_acsl_39; mpz_t e_acsl_40; int e_acsl_41;
+ mpz_t e_acsl_42; mpz_t e_acsl_43; int e_acsl_44;
+ __gmpz_init_set_str((__mpz_struct *)(e_acsl_38),"17592186044415",10);
+ __gmpz_init_set_str((__mpz_struct *)(e_acsl_39),"17592186044415",10);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_40),(long)0);
+ e_acsl_41 = __gmpz_cmp((__mpz_struct const *)(e_acsl_39),
+ (__mpz_struct const *)(e_acsl_40));
+ __gmpz_init((__mpz_struct *)(e_acsl_42));
+ /*@ assert 0xfffffffffff ≢ 0; */ ;
+ if (e_acsl_41 == 0) { e_acsl_fail((char *)"(0xfffffffffff == 0)"); }
+ __gmpz_cdiv_q((__mpz_struct *)(e_acsl_42),
+ (__mpz_struct const *)(e_acsl_38),
+ (__mpz_struct const *)(e_acsl_39));
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_43),(long)1);
+ e_acsl_44 = __gmpz_cmp((__mpz_struct const *)(e_acsl_42),
+ (__mpz_struct const *)(e_acsl_43));
+ if (! (e_acsl_44 == 0)) {
+ e_acsl_fail((char *)"(0xfffffffffff/0xfffffffffff == 1)");
+ } __gmpz_clear((__mpz_struct *)(e_acsl_38));
__gmpz_clear((__mpz_struct *)(e_acsl_39));
__gmpz_clear((__mpz_struct *)(e_acsl_40));
- __gmpz_clear((__mpz_struct *)(e_acsl_41));
+ __gmpz_clear((__mpz_struct *)(e_acsl_42));
+ __gmpz_clear((__mpz_struct *)(e_acsl_43));
+ }
+
+ /*@ assert x%2 ≡ -1; */ ;
+ { mpz_t e_acsl_45; mpz_t e_acsl_46; int e_acsl_47; mpz_t e_acsl_48;
+ mpz_t e_acsl_49; mpz_t e_acsl_50; int e_acsl_51;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_45),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_46),(long)2);
+ e_acsl_47 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_46));
+ __gmpz_init((__mpz_struct *)(e_acsl_48)); /*@ assert 2 ≢ 0; */ ;
+ if (e_acsl_47 == 0) { e_acsl_fail((char *)"(2 == 0)"); }
+ __gmpz_fdiv_r_ui(e_acsl_48,(__mpz_struct const *)(e_acsl_45),
+ (unsigned long)(e_acsl_46));
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_49),(long)1);
+ __gmpz_init((__mpz_struct *)(e_acsl_50));
+ __gmpz_neg((__mpz_struct *)(e_acsl_50),(__mpz_struct const *)(e_acsl_49));
+ e_acsl_51 = __gmpz_cmp((__mpz_struct const *)(e_acsl_48),
+ (__mpz_struct const *)(e_acsl_50));
+ if (! (e_acsl_51 == 0)) { e_acsl_fail((char *)"(x%2 == -1)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_45));
+ __gmpz_clear((__mpz_struct *)(e_acsl_46));
+ __gmpz_clear((__mpz_struct *)(e_acsl_48));
+ __gmpz_clear((__mpz_struct *)(e_acsl_49));
+ __gmpz_clear((__mpz_struct *)(e_acsl_50));
}
/*@ assert ((x*2+(3+y))-4)+(x-y) ≡ -10; */ ;
- { mpz_t e_acsl_43; mpz_t e_acsl_44; mpz_t e_acsl_45; mpz_t e_acsl_46;
- mpz_t e_acsl_47; mpz_t e_acsl_48; mpz_t e_acsl_49; mpz_t e_acsl_50;
- mpz_t e_acsl_51; mpz_t e_acsl_52; mpz_t e_acsl_53; mpz_t e_acsl_54;
- mpz_t e_acsl_55; mpz_t e_acsl_56; mpz_t e_acsl_57; int e_acsl_58;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_43),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_44),(long)2);
- __gmpz_init((__mpz_struct *)(e_acsl_45));
- __gmpz_mul((__mpz_struct *)(e_acsl_45),(__mpz_struct const *)(e_acsl_43),
- (__mpz_struct const *)(e_acsl_44));
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_46),(long)3);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_47),(long)y);
- __gmpz_init((__mpz_struct *)(e_acsl_48));
- __gmpz_add((__mpz_struct *)(e_acsl_48),(__mpz_struct const *)(e_acsl_46),
- (__mpz_struct const *)(e_acsl_47));
- __gmpz_init((__mpz_struct *)(e_acsl_49));
- __gmpz_add((__mpz_struct *)(e_acsl_49),(__mpz_struct const *)(e_acsl_45),
- (__mpz_struct const *)(e_acsl_48));
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_50),(long)4);
- __gmpz_init((__mpz_struct *)(e_acsl_51));
- __gmpz_sub((__mpz_struct *)(e_acsl_51),(__mpz_struct const *)(e_acsl_49),
- (__mpz_struct const *)(e_acsl_50));
+ { mpz_t e_acsl_52; mpz_t e_acsl_53; mpz_t e_acsl_54; mpz_t e_acsl_55;
+ mpz_t e_acsl_56; mpz_t e_acsl_57; mpz_t e_acsl_58; mpz_t e_acsl_59;
+ mpz_t e_acsl_60; mpz_t e_acsl_61; mpz_t e_acsl_62; mpz_t e_acsl_63;
+ mpz_t e_acsl_64; mpz_t e_acsl_65; mpz_t e_acsl_66; int e_acsl_67;
__gmpz_init_set_si((__mpz_struct *)(e_acsl_52),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_53),(long)y);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_53),(long)2);
__gmpz_init((__mpz_struct *)(e_acsl_54));
- __gmpz_sub((__mpz_struct *)(e_acsl_54),(__mpz_struct const *)(e_acsl_52),
+ __gmpz_mul((__mpz_struct *)(e_acsl_54),(__mpz_struct const *)(e_acsl_52),
(__mpz_struct const *)(e_acsl_53));
- __gmpz_init((__mpz_struct *)(e_acsl_55));
- __gmpz_add((__mpz_struct *)(e_acsl_55),(__mpz_struct const *)(e_acsl_51),
- (__mpz_struct const *)(e_acsl_54));
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_56),(long)10);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_55),(long)3);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_56),(long)y);
__gmpz_init((__mpz_struct *)(e_acsl_57));
- __gmpz_neg((__mpz_struct *)(e_acsl_57),(__mpz_struct const *)(e_acsl_56));
- e_acsl_58 = __gmpz_cmp((__mpz_struct const *)(e_acsl_55),
- (__mpz_struct const *)(e_acsl_57));
- if (! (e_acsl_58 == 0)) {
+ __gmpz_add((__mpz_struct *)(e_acsl_57),(__mpz_struct const *)(e_acsl_55),
+ (__mpz_struct const *)(e_acsl_56));
+ __gmpz_init((__mpz_struct *)(e_acsl_58));
+ __gmpz_add((__mpz_struct *)(e_acsl_58),(__mpz_struct const *)(e_acsl_54),
+ (__mpz_struct const *)(e_acsl_57));
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_59),(long)4);
+ __gmpz_init((__mpz_struct *)(e_acsl_60));
+ __gmpz_sub((__mpz_struct *)(e_acsl_60),(__mpz_struct const *)(e_acsl_58),
+ (__mpz_struct const *)(e_acsl_59));
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_61),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_62),(long)y);
+ __gmpz_init((__mpz_struct *)(e_acsl_63));
+ __gmpz_sub((__mpz_struct *)(e_acsl_63),(__mpz_struct const *)(e_acsl_61),
+ (__mpz_struct const *)(e_acsl_62));
+ __gmpz_init((__mpz_struct *)(e_acsl_64));
+ __gmpz_add((__mpz_struct *)(e_acsl_64),(__mpz_struct const *)(e_acsl_60),
+ (__mpz_struct const *)(e_acsl_63));
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_65),(long)10);
+ __gmpz_init((__mpz_struct *)(e_acsl_66));
+ __gmpz_neg((__mpz_struct *)(e_acsl_66),(__mpz_struct const *)(e_acsl_65));
+ e_acsl_67 = __gmpz_cmp((__mpz_struct const *)(e_acsl_64),
+ (__mpz_struct const *)(e_acsl_66));
+ if (! (e_acsl_67 == 0)) {
e_acsl_fail((char *)"(((x*2+(3+y))-4)+(x-y) == -10)");
- } __gmpz_clear((__mpz_struct *)(e_acsl_43));
- __gmpz_clear((__mpz_struct *)(e_acsl_44));
- __gmpz_clear((__mpz_struct *)(e_acsl_45));
- __gmpz_clear((__mpz_struct *)(e_acsl_46));
- __gmpz_clear((__mpz_struct *)(e_acsl_47));
- __gmpz_clear((__mpz_struct *)(e_acsl_48));
- __gmpz_clear((__mpz_struct *)(e_acsl_49));
- __gmpz_clear((__mpz_struct *)(e_acsl_50));
- __gmpz_clear((__mpz_struct *)(e_acsl_51));
- __gmpz_clear((__mpz_struct *)(e_acsl_52));
+ } __gmpz_clear((__mpz_struct *)(e_acsl_52));
__gmpz_clear((__mpz_struct *)(e_acsl_53));
__gmpz_clear((__mpz_struct *)(e_acsl_54));
__gmpz_clear((__mpz_struct *)(e_acsl_55));
__gmpz_clear((__mpz_struct *)(e_acsl_56));
__gmpz_clear((__mpz_struct *)(e_acsl_57));
+ __gmpz_clear((__mpz_struct *)(e_acsl_58));
+ __gmpz_clear((__mpz_struct *)(e_acsl_59));
+ __gmpz_clear((__mpz_struct *)(e_acsl_60));
+ __gmpz_clear((__mpz_struct *)(e_acsl_61));
+ __gmpz_clear((__mpz_struct *)(e_acsl_62));
+ __gmpz_clear((__mpz_struct *)(e_acsl_63));
+ __gmpz_clear((__mpz_struct *)(e_acsl_64));
+ __gmpz_clear((__mpz_struct *)(e_acsl_65));
+ __gmpz_clear((__mpz_struct *)(e_acsl_66));
}
/*@ assert (0≡1) ≡ !(0≡0); */ ;
@@ -817,39 +853,43 @@ int main(void)
e_acsl_fail((char *)"((0==1) == !(0==0))");
}
/*@ assert (0≤-1) ≡ (0>0); */ ;
- { mpz_t e_acsl_59; mpz_t e_acsl_60; mpz_t e_acsl_61; int e_acsl_62;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_59),(long)0);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_60),(long)1);
- __gmpz_init((__mpz_struct *)(e_acsl_61));
- __gmpz_neg((__mpz_struct *)(e_acsl_61),(__mpz_struct const *)(e_acsl_60));
- e_acsl_62 = __gmpz_cmp((__mpz_struct const *)(e_acsl_59),
- (__mpz_struct const *)(e_acsl_61));
- if (! ((e_acsl_62 <= 0) == (0 > 0))) {
+ { mpz_t e_acsl_68; mpz_t e_acsl_69; mpz_t e_acsl_70; int e_acsl_71;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_68),(long)0);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_69),(long)1);
+ __gmpz_init((__mpz_struct *)(e_acsl_70));
+ __gmpz_neg((__mpz_struct *)(e_acsl_70),(__mpz_struct const *)(e_acsl_69));
+ e_acsl_71 = __gmpz_cmp((__mpz_struct const *)(e_acsl_68),
+ (__mpz_struct const *)(e_acsl_70));
+ if (! ((e_acsl_71 <= 0) == (0 > 0))) {
e_acsl_fail((char *)"((0<=-1) == (0>0))");
- } __gmpz_clear((__mpz_struct *)(e_acsl_59));
- __gmpz_clear((__mpz_struct *)(e_acsl_60));
- __gmpz_clear((__mpz_struct *)(e_acsl_61));
+ } __gmpz_clear((__mpz_struct *)(e_acsl_68));
+ __gmpz_clear((__mpz_struct *)(e_acsl_69));
+ __gmpz_clear((__mpz_struct *)(e_acsl_70));
}
/*@ assert (0≥-1) ≡ (0≤0); */ ;
- { mpz_t e_acsl_63; mpz_t e_acsl_64; mpz_t e_acsl_65; int e_acsl_66;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_63),(long)0);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_64),(long)1);
- __gmpz_init((__mpz_struct *)(e_acsl_65));
- __gmpz_neg((__mpz_struct *)(e_acsl_65),(__mpz_struct const *)(e_acsl_64));
- e_acsl_66 = __gmpz_cmp((__mpz_struct const *)(e_acsl_63),
- (__mpz_struct const *)(e_acsl_65));
- if (! ((e_acsl_66 >= 0) == (0 <= 0))) {
+ { mpz_t e_acsl_72; mpz_t e_acsl_73; mpz_t e_acsl_74; int e_acsl_75;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_72),(long)0);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_73),(long)1);
+ __gmpz_init((__mpz_struct *)(e_acsl_74));
+ __gmpz_neg((__mpz_struct *)(e_acsl_74),(__mpz_struct const *)(e_acsl_73));
+ e_acsl_75 = __gmpz_cmp((__mpz_struct const *)(e_acsl_72),
+ (__mpz_struct const *)(e_acsl_74));
+ if (! ((e_acsl_75 >= 0) == (0 <= 0))) {
e_acsl_fail((char *)"((0>=-1) == (0<=0))");
- } __gmpz_clear((__mpz_struct *)(e_acsl_63));
- __gmpz_clear((__mpz_struct *)(e_acsl_64));
- __gmpz_clear((__mpz_struct *)(e_acsl_65));
+ } __gmpz_clear((__mpz_struct *)(e_acsl_72));
+ __gmpz_clear((__mpz_struct *)(e_acsl_73));
+ __gmpz_clear((__mpz_struct *)(e_acsl_74));
}
/*@ assert (0≢1) ≡ !(0≢0); */ ;
if (! ((0 != 1) == ! (0 != 0))) {
e_acsl_fail((char *)"((0!=1) == !(0!=0))");
}
+ /*@ assert (0≢0) ≡ !(1≢0); */ ;
+ if (! ((0 != 0) == ! (1 != 0))) {
+ e_acsl_fail((char *)"((0!=0) == !(1!=0))");
+ }
__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
index 2972764ef069c5e01c0f10e24de4117a1ea36eb0..bee9302fe0a0e28120c3cc646c1d918dba974917 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
@@ -25,14 +25,6 @@ typedef __mpq_struct *mpq_ptr;
/*@ 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);
@@ -53,9 +45,6 @@ __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);
@@ -606,151 +595,130 @@ int main(void)
}
/*@ assert ¬(x ≢ 0 ∧ y ≡ 1/0); */ ;
- { mpz_t e_acsl_16; mpz_t e_acsl_17; int e_acsl_18; int e_acsl_19;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_17),(long)0);
- e_acsl_18 = __gmpz_cmp((__mpz_struct const *)(e_acsl_16),
- (__mpz_struct const *)(e_acsl_17));
- if (e_acsl_18 != 0) {
- mpz_t e_acsl_20;
+ { mpz_t e_acsl_15; mpz_t e_acsl_16; int e_acsl_17; int e_acsl_18;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_15),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)0);
+ e_acsl_17 = __gmpz_cmp((__mpz_struct const *)(e_acsl_15),
+ (__mpz_struct const *)(e_acsl_16));
+ if (e_acsl_17 != 0) {
+ mpz_t e_acsl_19;
+ int e_acsl_20;
mpz_t e_acsl_21;
- mpz_t e_acsl_22;
- mpz_t e_acsl_23;
- int e_acsl_24;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)y);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_21),(long)1);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_22),(long)0);
- __gmpz_init((__mpz_struct *)(e_acsl_23));
+ int e_acsl_22;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_19),(long)y);
/*@ assert 0 ≢ 0; */ ;
if (0 == 0) { e_acsl_fail((char *)"(0 == 0)"); }
- __gmpz_cdiv_q((__mpz_struct *)(e_acsl_23),
- (__mpz_struct const *)(e_acsl_21),
- (__mpz_struct const *)(e_acsl_22));
- e_acsl_24 = __gmpz_cmp((__mpz_struct const *)(e_acsl_20),
- (__mpz_struct const *)(e_acsl_23));
- e_acsl_19 = e_acsl_24 == 0;
- __gmpz_clear((__mpz_struct *)(e_acsl_20));
+ e_acsl_20 = 1 / 0;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_21),(long)e_acsl_20);
+ e_acsl_22 = __gmpz_cmp((__mpz_struct const *)(e_acsl_19),
+ (__mpz_struct const *)(e_acsl_21));
+ e_acsl_18 = e_acsl_22 == 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_19));
__gmpz_clear((__mpz_struct *)(e_acsl_21));
- __gmpz_clear((__mpz_struct *)(e_acsl_22));
- __gmpz_clear((__mpz_struct *)(e_acsl_23));
- } else { e_acsl_19 = 0; }
- if (! (! e_acsl_19)) { e_acsl_fail((char *)"(!(x != 0 && y == 1/0))"); }
+ } else { e_acsl_18 = 0; }
+ if (! (! e_acsl_18)) { e_acsl_fail((char *)"(!(x != 0 && y == 1/0))"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_15));
__gmpz_clear((__mpz_struct *)(e_acsl_16));
- __gmpz_clear((__mpz_struct *)(e_acsl_17));
}
/*@ assert x ≡ 1 ∨ y ≡ 1; */ ;
- { mpz_t e_acsl_28; mpz_t e_acsl_29; int e_acsl_30; int e_acsl_31;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_28),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_29),(long)1);
- e_acsl_30 = __gmpz_cmp((__mpz_struct const *)(e_acsl_28),
- (__mpz_struct const *)(e_acsl_29));
- if (e_acsl_30 == 0) { e_acsl_31 = 1; }
+ { mpz_t e_acsl_26; mpz_t e_acsl_27; int e_acsl_28; int e_acsl_29;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_26),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_27),(long)1);
+ e_acsl_28 = __gmpz_cmp((__mpz_struct const *)(e_acsl_26),
+ (__mpz_struct const *)(e_acsl_27));
+ if (e_acsl_28 == 0) { e_acsl_29 = 1; }
else {
- mpz_t e_acsl_32;
- mpz_t e_acsl_33;
- int e_acsl_34;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_32),(long)y);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_33),(long)1);
- e_acsl_34 = __gmpz_cmp((__mpz_struct const *)(e_acsl_32),
- (__mpz_struct const *)(e_acsl_33));
- e_acsl_31 = e_acsl_34 == 0;
- __gmpz_clear((__mpz_struct *)(e_acsl_32));
- __gmpz_clear((__mpz_struct *)(e_acsl_33));
- } if (! e_acsl_31) { e_acsl_fail((char *)"(x == 1 || y == 1)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_28));
- __gmpz_clear((__mpz_struct *)(e_acsl_29));
+ mpz_t e_acsl_30;
+ mpz_t e_acsl_31;
+ int e_acsl_32;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_30),(long)y);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_31),(long)1);
+ e_acsl_32 = __gmpz_cmp((__mpz_struct const *)(e_acsl_30),
+ (__mpz_struct const *)(e_acsl_31));
+ e_acsl_29 = e_acsl_32 == 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_30));
+ __gmpz_clear((__mpz_struct *)(e_acsl_31));
+ } if (! e_acsl_29) { e_acsl_fail((char *)"(x == 1 || y == 1)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_26));
+ __gmpz_clear((__mpz_struct *)(e_acsl_27));
}
/*@ assert x ≡ 0 ∨ y ≡ 1/0; */ ;
- { mpz_t e_acsl_40; mpz_t e_acsl_41; int e_acsl_42; int e_acsl_43;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_40),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_41),(long)0);
- e_acsl_42 = __gmpz_cmp((__mpz_struct const *)(e_acsl_40),
- (__mpz_struct const *)(e_acsl_41));
- if (e_acsl_42 == 0) { e_acsl_43 = 1; }
+ { mpz_t e_acsl_37; mpz_t e_acsl_38; int e_acsl_39; int e_acsl_40;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_37),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_38),(long)0);
+ e_acsl_39 = __gmpz_cmp((__mpz_struct const *)(e_acsl_37),
+ (__mpz_struct const *)(e_acsl_38));
+ if (e_acsl_39 == 0) { e_acsl_40 = 1; }
else {
- mpz_t e_acsl_44;
- mpz_t e_acsl_45;
- mpz_t e_acsl_46;
- mpz_t e_acsl_47;
- int e_acsl_48;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_44),(long)y);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_45),(long)1);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_46),(long)0);
- __gmpz_init((__mpz_struct *)(e_acsl_47));
+ mpz_t e_acsl_41;
+ int e_acsl_42;
+ mpz_t e_acsl_43;
+ int e_acsl_44;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_41),(long)y);
/*@ assert 0 ≢ 0; */ ;
if (0 == 0) { e_acsl_fail((char *)"(0 == 0)"); }
- __gmpz_cdiv_q((__mpz_struct *)(e_acsl_47),
- (__mpz_struct const *)(e_acsl_45),
- (__mpz_struct const *)(e_acsl_46));
- e_acsl_48 = __gmpz_cmp((__mpz_struct const *)(e_acsl_44),
- (__mpz_struct const *)(e_acsl_47));
- e_acsl_43 = e_acsl_48 == 0;
- __gmpz_clear((__mpz_struct *)(e_acsl_44));
- __gmpz_clear((__mpz_struct *)(e_acsl_45));
- __gmpz_clear((__mpz_struct *)(e_acsl_46));
- __gmpz_clear((__mpz_struct *)(e_acsl_47));
- } if (! e_acsl_43) { e_acsl_fail((char *)"(x == 0 || y == 1/0)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_40));
- __gmpz_clear((__mpz_struct *)(e_acsl_41));
+ e_acsl_42 = 1 / 0;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_43),(long)e_acsl_42);
+ e_acsl_44 = __gmpz_cmp((__mpz_struct const *)(e_acsl_41),
+ (__mpz_struct const *)(e_acsl_43));
+ e_acsl_40 = e_acsl_44 == 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_41));
+ __gmpz_clear((__mpz_struct *)(e_acsl_43));
+ } if (! e_acsl_40) { e_acsl_fail((char *)"(x == 0 || y == 1/0)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_37));
+ __gmpz_clear((__mpz_struct *)(e_acsl_38));
}
/*@ assert x ≡ 0 ⇒ y ≡ 1; */ ;
- { mpz_t e_acsl_52; mpz_t e_acsl_53; int e_acsl_54; int e_acsl_55;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_52),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_53),(long)0);
- e_acsl_54 = __gmpz_cmp((__mpz_struct const *)(e_acsl_52),
- (__mpz_struct const *)(e_acsl_53));
- if (! (e_acsl_54 == 0)) { e_acsl_55 = 1; }
+ { mpz_t e_acsl_48; mpz_t e_acsl_49; int e_acsl_50; int e_acsl_51;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_48),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_49),(long)0);
+ e_acsl_50 = __gmpz_cmp((__mpz_struct const *)(e_acsl_48),
+ (__mpz_struct const *)(e_acsl_49));
+ if (! (e_acsl_50 == 0)) { e_acsl_51 = 1; }
else {
- mpz_t e_acsl_56;
- mpz_t e_acsl_57;
- int e_acsl_58;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_56),(long)y);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_57),(long)1);
- e_acsl_58 = __gmpz_cmp((__mpz_struct const *)(e_acsl_56),
- (__mpz_struct const *)(e_acsl_57));
- e_acsl_55 = e_acsl_58 == 0;
- __gmpz_clear((__mpz_struct *)(e_acsl_56));
- __gmpz_clear((__mpz_struct *)(e_acsl_57));
- } if (! e_acsl_55) { e_acsl_fail((char *)"(x == 0 ==> y == 1)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_52));
- __gmpz_clear((__mpz_struct *)(e_acsl_53));
+ mpz_t e_acsl_52;
+ mpz_t e_acsl_53;
+ int e_acsl_54;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_52),(long)y);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_53),(long)1);
+ e_acsl_54 = __gmpz_cmp((__mpz_struct const *)(e_acsl_52),
+ (__mpz_struct const *)(e_acsl_53));
+ e_acsl_51 = e_acsl_54 == 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_52));
+ __gmpz_clear((__mpz_struct *)(e_acsl_53));
+ } if (! e_acsl_51) { e_acsl_fail((char *)"(x == 0 ==> y == 1)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_48));
+ __gmpz_clear((__mpz_struct *)(e_acsl_49));
}
/*@ assert x ≡ 1 ⇒ y ≡ 1/0; */ ;
- { mpz_t e_acsl_64; mpz_t e_acsl_65; int e_acsl_66; int e_acsl_67;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_64),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_65),(long)1);
- e_acsl_66 = __gmpz_cmp((__mpz_struct const *)(e_acsl_64),
- (__mpz_struct const *)(e_acsl_65));
- if (! (e_acsl_66 == 0)) { e_acsl_67 = 1; }
+ { mpz_t e_acsl_59; mpz_t e_acsl_60; int e_acsl_61; int e_acsl_62;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_59),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_60),(long)1);
+ e_acsl_61 = __gmpz_cmp((__mpz_struct const *)(e_acsl_59),
+ (__mpz_struct const *)(e_acsl_60));
+ if (! (e_acsl_61 == 0)) { e_acsl_62 = 1; }
else {
- mpz_t e_acsl_68;
- mpz_t e_acsl_69;
- mpz_t e_acsl_70;
- mpz_t e_acsl_71;
- int e_acsl_72;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_68),(long)y);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_69),(long)1);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_70),(long)0);
- __gmpz_init((__mpz_struct *)(e_acsl_71));
+ mpz_t e_acsl_63;
+ int e_acsl_64;
+ mpz_t e_acsl_65;
+ int e_acsl_66;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_63),(long)y);
/*@ assert 0 ≢ 0; */ ;
if (0 == 0) { e_acsl_fail((char *)"(0 == 0)"); }
- __gmpz_cdiv_q((__mpz_struct *)(e_acsl_71),
- (__mpz_struct const *)(e_acsl_69),
- (__mpz_struct const *)(e_acsl_70));
- e_acsl_72 = __gmpz_cmp((__mpz_struct const *)(e_acsl_68),
- (__mpz_struct const *)(e_acsl_71));
- e_acsl_67 = e_acsl_72 == 0;
- __gmpz_clear((__mpz_struct *)(e_acsl_68));
- __gmpz_clear((__mpz_struct *)(e_acsl_69));
- __gmpz_clear((__mpz_struct *)(e_acsl_70));
- __gmpz_clear((__mpz_struct *)(e_acsl_71));
- } if (! e_acsl_67) { e_acsl_fail((char *)"(x == 1 ==> y == 1/0)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_64));
- __gmpz_clear((__mpz_struct *)(e_acsl_65));
+ e_acsl_64 = 1 / 0;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_65),(long)e_acsl_64);
+ e_acsl_66 = __gmpz_cmp((__mpz_struct const *)(e_acsl_63),
+ (__mpz_struct const *)(e_acsl_65));
+ e_acsl_62 = e_acsl_66 == 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_63));
+ __gmpz_clear((__mpz_struct *)(e_acsl_65));
+ } if (! e_acsl_62) { e_acsl_fail((char *)"(x == 1 ==> y == 1/0)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_59));
+ __gmpz_clear((__mpz_struct *)(e_acsl_60));
}
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
index 140ce60280c4a129c2fcc803169f76c721617e57..3fa5e559ff282dc250e91bfed85c0c33d52c09e6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
@@ -33,6 +33,14 @@ __inline static void __gmpz_abs(mpz_ptr __gmp_w, mpz_srcptr __gmp_u);
extern void __gmpz_add(__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_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);
@@ -63,6 +71,14 @@ 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);
+/*@ 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);
__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__((
@@ -631,75 +647,111 @@ int main(void)
__gmpz_clear((__mpz_struct *)(e_acsl_8));
}
+ /*@ assert t[(2*sizeof(int))/sizeof((int)0x0)] ≡ 4; */ ;
+ { mpz_t e_acsl_10; mpz_t e_acsl_11; mpz_t e_acsl_12; mpz_t e_acsl_13;
+ mpz_t e_acsl_14; int e_acsl_15; mpz_t e_acsl_16; int e_acsl_17;
+ mpz_t e_acsl_18; mpz_t e_acsl_19; int e_acsl_20;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_10),(long)2);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)4);
+ __gmpz_init((__mpz_struct *)(e_acsl_12));
+ __gmpz_mul((__mpz_struct *)(e_acsl_12),(__mpz_struct const *)(e_acsl_10),
+ (__mpz_struct const *)(e_acsl_11));
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_13),(long)4);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_14),(long)0);
+ e_acsl_15 = __gmpz_cmp((__mpz_struct const *)(e_acsl_13),
+ (__mpz_struct const *)(e_acsl_14));
+ __gmpz_init((__mpz_struct *)(e_acsl_16));
+ /*@ assert sizeof((int)0x0) ≢ 0; */ ;
+ if (e_acsl_15 == 0) { e_acsl_fail((char *)"(sizeof((int)0x0) == 0)"); }
+ __gmpz_cdiv_q((__mpz_struct *)(e_acsl_16),
+ (__mpz_struct const *)(e_acsl_12),
+ (__mpz_struct const *)(e_acsl_13));
+ e_acsl_17 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_16));
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_18),(long)t[e_acsl_17]);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_19),(long)4);
+ e_acsl_20 = __gmpz_cmp((__mpz_struct const *)(e_acsl_18),
+ (__mpz_struct const *)(e_acsl_19));
+ if (! (e_acsl_20 == 0)) {
+ e_acsl_fail((char *)"(t[(2*sizeof(int))/sizeof((int)0x0)] == 4)");
+ } __gmpz_clear((__mpz_struct *)(e_acsl_10));
+ __gmpz_clear((__mpz_struct *)(e_acsl_11));
+ __gmpz_clear((__mpz_struct *)(e_acsl_12));
+ __gmpz_clear((__mpz_struct *)(e_acsl_13));
+ __gmpz_clear((__mpz_struct *)(e_acsl_14));
+ __gmpz_clear((__mpz_struct *)(e_acsl_16));
+ __gmpz_clear((__mpz_struct *)(e_acsl_18));
+ __gmpz_clear((__mpz_struct *)(e_acsl_19));
+ }
+
{ int i; i = 0;
while (1) {
if (! (i < 2)) { break; }
/*@ assert t[i] ≡ i+2; */ ;
- { mpz_t e_acsl_10; mpz_t e_acsl_11; mpz_t e_acsl_12; mpz_t e_acsl_13;
- int e_acsl_14;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_10),(long)t[i]);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)i);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_12),(long)2);
- __gmpz_init((__mpz_struct *)(e_acsl_13));
- __gmpz_add((__mpz_struct *)(e_acsl_13),
- (__mpz_struct const *)(e_acsl_11),
- (__mpz_struct const *)(e_acsl_12));
- e_acsl_14 = __gmpz_cmp((__mpz_struct const *)(e_acsl_10),
- (__mpz_struct const *)(e_acsl_13));
- if (! (e_acsl_14 == 0)) { e_acsl_fail((char *)"(t[i] == i+2)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_10));
- __gmpz_clear((__mpz_struct *)(e_acsl_11));
- __gmpz_clear((__mpz_struct *)(e_acsl_12));
- __gmpz_clear((__mpz_struct *)(e_acsl_13));
- }
-
- /*@ assert t[2-i] ≡ 4-i; */ ;
- { mpz_t e_acsl_15; mpz_t e_acsl_16; mpz_t e_acsl_17; int e_acsl_18;
- mpz_t e_acsl_19; mpz_t e_acsl_20; mpz_t e_acsl_21; mpz_t e_acsl_22;
- int e_acsl_23;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_15),(long)2);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)i);
- __gmpz_init((__mpz_struct *)(e_acsl_17));
- __gmpz_sub((__mpz_struct *)(e_acsl_17),
- (__mpz_struct const *)(e_acsl_15),
- (__mpz_struct const *)(e_acsl_16));
- e_acsl_18 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_17));
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_19),(long)t[e_acsl_18]);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)4);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_21),(long)i);
- __gmpz_init((__mpz_struct *)(e_acsl_22));
- __gmpz_sub((__mpz_struct *)(e_acsl_22),
- (__mpz_struct const *)(e_acsl_20),
- (__mpz_struct const *)(e_acsl_21));
- e_acsl_23 = __gmpz_cmp((__mpz_struct const *)(e_acsl_19),
- (__mpz_struct const *)(e_acsl_22));
- if (! (e_acsl_23 == 0)) { e_acsl_fail((char *)"(t[2-i] == 4-i)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_15));
- __gmpz_clear((__mpz_struct *)(e_acsl_16));
- __gmpz_clear((__mpz_struct *)(e_acsl_17));
- __gmpz_clear((__mpz_struct *)(e_acsl_19));
- __gmpz_clear((__mpz_struct *)(e_acsl_20));
+ { mpz_t e_acsl_21; mpz_t e_acsl_22; mpz_t e_acsl_23; mpz_t e_acsl_24;
+ int e_acsl_25;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_21),(long)t[i]);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_22),(long)i);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_23),(long)2);
+ __gmpz_init((__mpz_struct *)(e_acsl_24));
+ __gmpz_add((__mpz_struct *)(e_acsl_24),
+ (__mpz_struct const *)(e_acsl_22),
+ (__mpz_struct const *)(e_acsl_23));
+ e_acsl_25 = __gmpz_cmp((__mpz_struct const *)(e_acsl_21),
+ (__mpz_struct const *)(e_acsl_24));
+ if (! (e_acsl_25 == 0)) { e_acsl_fail((char *)"(t[i] == i+2)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_21));
__gmpz_clear((__mpz_struct *)(e_acsl_22));
+ __gmpz_clear((__mpz_struct *)(e_acsl_23));
+ __gmpz_clear((__mpz_struct *)(e_acsl_24));
}
- /*@ assert *(&t[2]-i) ≡ 4-i; */ ;
- { mpz_t e_acsl_24; mpz_t e_acsl_25; mpz_t e_acsl_26; mpz_t e_acsl_27;
- int e_acsl_28;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_24),(long)*(& t[2] - i));
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_25),(long)4);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_26),(long)i);
- __gmpz_init((__mpz_struct *)(e_acsl_27));
- __gmpz_sub((__mpz_struct *)(e_acsl_27),
- (__mpz_struct const *)(e_acsl_25),
- (__mpz_struct const *)(e_acsl_26));
- e_acsl_28 = __gmpz_cmp((__mpz_struct const *)(e_acsl_24),
- (__mpz_struct const *)(e_acsl_27));
- if (! (e_acsl_28 == 0)) { e_acsl_fail((char *)"(*(&t[2]-i) == 4-i)");
- } __gmpz_clear((__mpz_struct *)(e_acsl_24));
- __gmpz_clear((__mpz_struct *)(e_acsl_25));
+ /*@ assert t[2-i] ≡ 4-i; */ ;
+ { mpz_t e_acsl_26; mpz_t e_acsl_27; mpz_t e_acsl_28; int 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;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_26),(long)2);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_27),(long)i);
+ __gmpz_init((__mpz_struct *)(e_acsl_28));
+ __gmpz_sub((__mpz_struct *)(e_acsl_28),
+ (__mpz_struct const *)(e_acsl_26),
+ (__mpz_struct const *)(e_acsl_27));
+ e_acsl_29 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_28));
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_30),(long)t[e_acsl_29]);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_31),(long)4);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_32),(long)i);
+ __gmpz_init((__mpz_struct *)(e_acsl_33));
+ __gmpz_sub((__mpz_struct *)(e_acsl_33),
+ (__mpz_struct const *)(e_acsl_31),
+ (__mpz_struct const *)(e_acsl_32));
+ e_acsl_34 = __gmpz_cmp((__mpz_struct const *)(e_acsl_30),
+ (__mpz_struct const *)(e_acsl_33));
+ if (! (e_acsl_34 == 0)) { e_acsl_fail((char *)"(t[2-i] == 4-i)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_26));
__gmpz_clear((__mpz_struct *)(e_acsl_27));
+ __gmpz_clear((__mpz_struct *)(e_acsl_28));
+ __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));
+ }
+
+ /*@ assert *(&t[2]-i) ≡ 4-i; */ ;
+ { mpz_t e_acsl_35; mpz_t e_acsl_36; mpz_t e_acsl_37; mpz_t e_acsl_38;
+ int e_acsl_39;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_35),(long)*(& t[2] - i));
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_36),(long)4);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_37),(long)i);
+ __gmpz_init((__mpz_struct *)(e_acsl_38));
+ __gmpz_sub((__mpz_struct *)(e_acsl_38),
+ (__mpz_struct const *)(e_acsl_36),
+ (__mpz_struct const *)(e_acsl_37));
+ e_acsl_39 = __gmpz_cmp((__mpz_struct const *)(e_acsl_35),
+ (__mpz_struct const *)(e_acsl_38));
+ if (! (e_acsl_39 == 0)) { e_acsl_fail((char *)"(*(&t[2]-i) == 4-i)");
+ } __gmpz_clear((__mpz_struct *)(e_acsl_35));
+ __gmpz_clear((__mpz_struct *)(e_acsl_36));
+ __gmpz_clear((__mpz_struct *)(e_acsl_37));
+ __gmpz_clear((__mpz_struct *)(e_acsl_38));
}
i ++;
@@ -709,14 +761,14 @@ int main(void)
p = & t[2];
t[2] = 5;
/*@ assert *p ≡ 5; */ ;
- { mpz_t e_acsl_29; mpz_t e_acsl_30; int e_acsl_31;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_29),(long)*p);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_30),(long)5);
- e_acsl_31 = __gmpz_cmp((__mpz_struct const *)(e_acsl_29),
- (__mpz_struct const *)(e_acsl_30));
- if (! (e_acsl_31 == 0)) { e_acsl_fail((char *)"(*p == 5)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_29));
- __gmpz_clear((__mpz_struct *)(e_acsl_30));
+ { mpz_t e_acsl_40; mpz_t e_acsl_41; int e_acsl_42;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_40),(long)*p);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_41),(long)5);
+ e_acsl_42 = __gmpz_cmp((__mpz_struct const *)(e_acsl_40),
+ (__mpz_struct const *)(e_acsl_41));
+ if (! (e_acsl_42 == 0)) { e_acsl_fail((char *)"(*p == 5)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_40));
+ __gmpz_clear((__mpz_struct *)(e_acsl_41));
}
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
index 3cfef1101c0a84a8b7d9ea8d957251adefa20634..c8428bb3abe96cba28552c70023b9074e3d08387 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
@@ -60,52 +60,42 @@ PROJECT_FILE.i:153:[value] Assertion got status valid.
Called from PROJECT_FILE.i:157.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:164.
+ Called from PROJECT_FILE.i:163.
[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 <- main.
- Called from PROJECT_FILE.i:167.
-PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-PROJECT_FILE.i:168:[value] Assertion got status invalid (stopping propagation)..
+PROJECT_FILE.i:164:[value] Assertion got status invalid (stopping propagation)..
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:179.
+ Called from PROJECT_FILE.i:174.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:179.
+ Called from PROJECT_FILE.i:174.
[value] Done for function mpz_clear
-PROJECT_FILE.i:182:[value] Assertion got status valid.
+PROJECT_FILE.i:177:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:184.
+ Called from PROJECT_FILE.i:179.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:185.
+ 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:185.
+ Called from PROJECT_FILE.i:180.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:191.
+ Called from PROJECT_FILE.i:186.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:192.
+ Called from PROJECT_FILE.i:187.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:193.
+ Called from PROJECT_FILE.i:188.
[value] Done for function mpz_cmp
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:195.
+ Called from PROJECT_FILE.i:190.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:196.
+ Called from PROJECT_FILE.i:191.
[value] Done for function mpz_clear
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:197.
+ Called from PROJECT_FILE.i:192.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -115,67 +105,58 @@ PROJECT_FILE.i:182:[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:198.
+ Called from PROJECT_FILE.i:193.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:198.
+ Called from PROJECT_FILE.i:193.
[value] Done for function mpz_clear
-PROJECT_FILE.i:201:[value] Assertion got status valid.
+PROJECT_FILE.i:196:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:204.
+ 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:204.
+ Called from PROJECT_FILE.i:199.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:205.
+ Called from PROJECT_FILE.i:200.
[value] Done for function mpz_cmp
[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:214.
-[value] Done for function mpz_init_set_si
-[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:215.
+ Called from PROJECT_FILE.i:207.
[value] Done for function mpz_init_set_si
-[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:216.
-[value] Done for function mpz_init
-PROJECT_FILE.i:217:[value] Assertion got status invalid (stopping propagation)..
+PROJECT_FILE.i:208:[value] Assertion got status invalid (stopping propagation)..
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:227.
+ Called from PROJECT_FILE.i:217.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:227.
+ Called from PROJECT_FILE.i:217.
[value] Done for function mpz_clear
-PROJECT_FILE.i:230:[value] Assertion got status valid.
+PROJECT_FILE.i:220:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:232.
+ Called from PROJECT_FILE.i:222.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:233.
+ Called from PROJECT_FILE.i:223.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:233.
+ Called from PROJECT_FILE.i:223.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:239.
+ 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:240.
+ Called from PROJECT_FILE.i:230.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:241.
+ Called from PROJECT_FILE.i:231.
[value] Done for function mpz_cmp
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:243.
+ Called from PROJECT_FILE.i:233.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:244.
+ Called from PROJECT_FILE.i:234.
[value] Done for function mpz_clear
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:245.
+ Called from PROJECT_FILE.i:235.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -185,39 +166,30 @@ PROJECT_FILE.i:230:[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:246.
+ Called from PROJECT_FILE.i:236.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:246.
+ Called from PROJECT_FILE.i:236.
[value] Done for function mpz_clear
-PROJECT_FILE.i:249:[value] Assertion got status valid.
+PROJECT_FILE.i:239:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:252.
+ Called from PROJECT_FILE.i:242.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:252.
+ Called from PROJECT_FILE.i:242.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:253.
+ Called from PROJECT_FILE.i:243.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:261.
+ 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: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_init <- main.
- Called from PROJECT_FILE.i:264.
-[value] Done for function mpz_init
-PROJECT_FILE.i:265:[value] Assertion got status invalid (stopping propagation)..
+PROJECT_FILE.i:251:[value] Assertion got status invalid (stopping propagation)..
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:275.
+ Called from PROJECT_FILE.i:260.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:275.
+ Called from PROJECT_FILE.i:260.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
@@ -235,8 +207,6 @@ PROJECT_FILE.i:125:[from] warning: variadic call detected. Using only 1 argument
[from] Done for function exit
PROJECT_FILE.i:125:[from] Non terminating function (no dependencies)
[from] Done for function e_acsl_fail
-[from] Computing for function mpz_init
-[from] Done for function mpz_init
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
@@ -252,9 +222,6 @@ struct __anonstruct___mpz_struct_1 {
};
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_si(__mpz_struct * /*[1]*/ z, long n);
@@ -266,14 +233,6 @@ extern void mpz_clear(__mpz_struct * /*[1]*/ x);
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; */
@@ -318,151 +277,130 @@ int main(void)
}
/*@ assert ¬(x ≢ 0 ∧ y ≡ 1/0); */ ;
- { mpz_t e_acsl_16; mpz_t e_acsl_17; int e_acsl_18; int e_acsl_19;
- mpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_17),(long)0);
- e_acsl_18 = mpz_cmp((__mpz_struct const *)(e_acsl_16),
- (__mpz_struct const *)(e_acsl_17));
- if (e_acsl_18 != 0) {
- mpz_t e_acsl_20;
+ { mpz_t e_acsl_15; mpz_t e_acsl_16; int e_acsl_17; int e_acsl_18;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_15),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)0);
+ e_acsl_17 = mpz_cmp((__mpz_struct const *)(e_acsl_15),
+ (__mpz_struct const *)(e_acsl_16));
+ if (e_acsl_17 != 0) {
+ mpz_t e_acsl_19;
+ int e_acsl_20;
mpz_t e_acsl_21;
- mpz_t e_acsl_22;
- mpz_t e_acsl_23;
- int e_acsl_24;
- mpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)y);
- mpz_init_set_si((__mpz_struct *)(e_acsl_21),(long)1);
- mpz_init_set_si((__mpz_struct *)(e_acsl_22),(long)0);
- mpz_init((__mpz_struct *)(e_acsl_23));
+ int e_acsl_22;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_19),(long)y);
/*@ assert 0 ≢ 0; */ ;
if (0 == 0) { e_acsl_fail((char *)"(0 == 0)"); }
- mpz_cdiv_q((__mpz_struct *)(e_acsl_23),
- (__mpz_struct const *)(e_acsl_21),
- (__mpz_struct const *)(e_acsl_22));
- e_acsl_24 = mpz_cmp((__mpz_struct const *)(e_acsl_20),
- (__mpz_struct const *)(e_acsl_23));
- e_acsl_19 = e_acsl_24 == 0;
- mpz_clear((__mpz_struct *)(e_acsl_20));
+ e_acsl_20 = 1 / 0;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_21),(long)e_acsl_20);
+ e_acsl_22 = mpz_cmp((__mpz_struct const *)(e_acsl_19),
+ (__mpz_struct const *)(e_acsl_21));
+ e_acsl_18 = e_acsl_22 == 0;
+ mpz_clear((__mpz_struct *)(e_acsl_19));
mpz_clear((__mpz_struct *)(e_acsl_21));
- mpz_clear((__mpz_struct *)(e_acsl_22));
- mpz_clear((__mpz_struct *)(e_acsl_23));
- } else { e_acsl_19 = 0; }
- if (! (! e_acsl_19)) { e_acsl_fail((char *)"(!(x != 0 && y == 1/0))"); }
+ } else { e_acsl_18 = 0; }
+ if (! (! e_acsl_18)) { e_acsl_fail((char *)"(!(x != 0 && y == 1/0))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_15));
mpz_clear((__mpz_struct *)(e_acsl_16));
- mpz_clear((__mpz_struct *)(e_acsl_17));
}
/*@ assert x ≡ 1 ∨ y ≡ 1; */ ;
- { mpz_t e_acsl_28; mpz_t e_acsl_29; int e_acsl_30; int e_acsl_31;
- mpz_init_set_si((__mpz_struct *)(e_acsl_28),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_29),(long)1);
- e_acsl_30 = mpz_cmp((__mpz_struct const *)(e_acsl_28),
- (__mpz_struct const *)(e_acsl_29));
- if (e_acsl_30 == 0) { e_acsl_31 = 1; }
+ { mpz_t e_acsl_26; mpz_t e_acsl_27; int e_acsl_28; int e_acsl_29;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_26),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_27),(long)1);
+ e_acsl_28 = mpz_cmp((__mpz_struct const *)(e_acsl_26),
+ (__mpz_struct const *)(e_acsl_27));
+ if (e_acsl_28 == 0) { e_acsl_29 = 1; }
else {
- mpz_t e_acsl_32;
- mpz_t e_acsl_33;
- int e_acsl_34;
- mpz_init_set_si((__mpz_struct *)(e_acsl_32),(long)y);
- mpz_init_set_si((__mpz_struct *)(e_acsl_33),(long)1);
- e_acsl_34 = mpz_cmp((__mpz_struct const *)(e_acsl_32),
- (__mpz_struct const *)(e_acsl_33));
- e_acsl_31 = e_acsl_34 == 0;
- mpz_clear((__mpz_struct *)(e_acsl_32));
- mpz_clear((__mpz_struct *)(e_acsl_33));
- } if (! e_acsl_31) { e_acsl_fail((char *)"(x == 1 || y == 1)"); }
- mpz_clear((__mpz_struct *)(e_acsl_28));
- mpz_clear((__mpz_struct *)(e_acsl_29));
+ mpz_t e_acsl_30;
+ mpz_t e_acsl_31;
+ int e_acsl_32;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_30),(long)y);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_31),(long)1);
+ e_acsl_32 = mpz_cmp((__mpz_struct const *)(e_acsl_30),
+ (__mpz_struct const *)(e_acsl_31));
+ e_acsl_29 = e_acsl_32 == 0;
+ mpz_clear((__mpz_struct *)(e_acsl_30));
+ mpz_clear((__mpz_struct *)(e_acsl_31));
+ } if (! e_acsl_29) { e_acsl_fail((char *)"(x == 1 || y == 1)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_26));
+ mpz_clear((__mpz_struct *)(e_acsl_27));
}
/*@ assert x ≡ 0 ∨ y ≡ 1/0; */ ;
- { mpz_t e_acsl_40; mpz_t e_acsl_41; int e_acsl_42; int e_acsl_43;
- mpz_init_set_si((__mpz_struct *)(e_acsl_40),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_41),(long)0);
- e_acsl_42 = mpz_cmp((__mpz_struct const *)(e_acsl_40),
- (__mpz_struct const *)(e_acsl_41));
- if (e_acsl_42 == 0) { e_acsl_43 = 1; }
+ { mpz_t e_acsl_37; mpz_t e_acsl_38; int e_acsl_39; int e_acsl_40;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_37),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_38),(long)0);
+ e_acsl_39 = mpz_cmp((__mpz_struct const *)(e_acsl_37),
+ (__mpz_struct const *)(e_acsl_38));
+ if (e_acsl_39 == 0) { e_acsl_40 = 1; }
else {
- mpz_t e_acsl_44;
- mpz_t e_acsl_45;
- mpz_t e_acsl_46;
- mpz_t e_acsl_47;
- int e_acsl_48;
- mpz_init_set_si((__mpz_struct *)(e_acsl_44),(long)y);
- mpz_init_set_si((__mpz_struct *)(e_acsl_45),(long)1);
- mpz_init_set_si((__mpz_struct *)(e_acsl_46),(long)0);
- mpz_init((__mpz_struct *)(e_acsl_47));
+ mpz_t e_acsl_41;
+ int e_acsl_42;
+ mpz_t e_acsl_43;
+ int e_acsl_44;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_41),(long)y);
/*@ assert 0 ≢ 0; */ ;
if (0 == 0) { e_acsl_fail((char *)"(0 == 0)"); }
- mpz_cdiv_q((__mpz_struct *)(e_acsl_47),
- (__mpz_struct const *)(e_acsl_45),
- (__mpz_struct const *)(e_acsl_46));
- e_acsl_48 = mpz_cmp((__mpz_struct const *)(e_acsl_44),
- (__mpz_struct const *)(e_acsl_47));
- e_acsl_43 = e_acsl_48 == 0;
- mpz_clear((__mpz_struct *)(e_acsl_44));
- mpz_clear((__mpz_struct *)(e_acsl_45));
- mpz_clear((__mpz_struct *)(e_acsl_46));
- mpz_clear((__mpz_struct *)(e_acsl_47));
- } if (! e_acsl_43) { e_acsl_fail((char *)"(x == 0 || y == 1/0)"); }
- mpz_clear((__mpz_struct *)(e_acsl_40));
- mpz_clear((__mpz_struct *)(e_acsl_41));
+ e_acsl_42 = 1 / 0;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_43),(long)e_acsl_42);
+ e_acsl_44 = mpz_cmp((__mpz_struct const *)(e_acsl_41),
+ (__mpz_struct const *)(e_acsl_43));
+ e_acsl_40 = e_acsl_44 == 0;
+ mpz_clear((__mpz_struct *)(e_acsl_41));
+ mpz_clear((__mpz_struct *)(e_acsl_43));
+ } if (! e_acsl_40) { e_acsl_fail((char *)"(x == 0 || y == 1/0)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_37));
+ mpz_clear((__mpz_struct *)(e_acsl_38));
}
/*@ assert x ≡ 0 ⇒ y ≡ 1; */ ;
- { mpz_t e_acsl_52; mpz_t e_acsl_53; int e_acsl_54; int e_acsl_55;
- mpz_init_set_si((__mpz_struct *)(e_acsl_52),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_53),(long)0);
- e_acsl_54 = mpz_cmp((__mpz_struct const *)(e_acsl_52),
- (__mpz_struct const *)(e_acsl_53));
- if (! (e_acsl_54 == 0)) { e_acsl_55 = 1; }
+ { mpz_t e_acsl_48; mpz_t e_acsl_49; int e_acsl_50; int e_acsl_51;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_48),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_49),(long)0);
+ e_acsl_50 = mpz_cmp((__mpz_struct const *)(e_acsl_48),
+ (__mpz_struct const *)(e_acsl_49));
+ if (! (e_acsl_50 == 0)) { e_acsl_51 = 1; }
else {
- mpz_t e_acsl_56;
- mpz_t e_acsl_57;
- int e_acsl_58;
- mpz_init_set_si((__mpz_struct *)(e_acsl_56),(long)y);
- mpz_init_set_si((__mpz_struct *)(e_acsl_57),(long)1);
- e_acsl_58 = mpz_cmp((__mpz_struct const *)(e_acsl_56),
- (__mpz_struct const *)(e_acsl_57));
- e_acsl_55 = e_acsl_58 == 0;
- mpz_clear((__mpz_struct *)(e_acsl_56));
- mpz_clear((__mpz_struct *)(e_acsl_57));
- } if (! e_acsl_55) { e_acsl_fail((char *)"(x == 0 ==> y == 1)"); }
- mpz_clear((__mpz_struct *)(e_acsl_52));
- mpz_clear((__mpz_struct *)(e_acsl_53));
+ mpz_t e_acsl_52;
+ mpz_t e_acsl_53;
+ int e_acsl_54;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_52),(long)y);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_53),(long)1);
+ e_acsl_54 = mpz_cmp((__mpz_struct const *)(e_acsl_52),
+ (__mpz_struct const *)(e_acsl_53));
+ e_acsl_51 = e_acsl_54 == 0;
+ mpz_clear((__mpz_struct *)(e_acsl_52));
+ mpz_clear((__mpz_struct *)(e_acsl_53));
+ } if (! e_acsl_51) { e_acsl_fail((char *)"(x == 0 ==> y == 1)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_48));
+ mpz_clear((__mpz_struct *)(e_acsl_49));
}
/*@ assert x ≡ 1 ⇒ y ≡ 1/0; */ ;
- { mpz_t e_acsl_64; mpz_t e_acsl_65; int e_acsl_66; int e_acsl_67;
- mpz_init_set_si((__mpz_struct *)(e_acsl_64),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_65),(long)1);
- e_acsl_66 = mpz_cmp((__mpz_struct const *)(e_acsl_64),
- (__mpz_struct const *)(e_acsl_65));
- if (! (e_acsl_66 == 0)) { e_acsl_67 = 1; }
+ { mpz_t e_acsl_59; mpz_t e_acsl_60; int e_acsl_61; int e_acsl_62;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_59),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_60),(long)1);
+ e_acsl_61 = mpz_cmp((__mpz_struct const *)(e_acsl_59),
+ (__mpz_struct const *)(e_acsl_60));
+ if (! (e_acsl_61 == 0)) { e_acsl_62 = 1; }
else {
- mpz_t e_acsl_68;
- mpz_t e_acsl_69;
- mpz_t e_acsl_70;
- mpz_t e_acsl_71;
- int e_acsl_72;
- mpz_init_set_si((__mpz_struct *)(e_acsl_68),(long)y);
- mpz_init_set_si((__mpz_struct *)(e_acsl_69),(long)1);
- mpz_init_set_si((__mpz_struct *)(e_acsl_70),(long)0);
- mpz_init((__mpz_struct *)(e_acsl_71));
+ mpz_t e_acsl_63;
+ int e_acsl_64;
+ mpz_t e_acsl_65;
+ int e_acsl_66;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_63),(long)y);
/*@ assert 0 ≢ 0; */ ;
if (0 == 0) { e_acsl_fail((char *)"(0 == 0)"); }
- mpz_cdiv_q((__mpz_struct *)(e_acsl_71),
- (__mpz_struct const *)(e_acsl_69),
- (__mpz_struct const *)(e_acsl_70));
- e_acsl_72 = mpz_cmp((__mpz_struct const *)(e_acsl_68),
- (__mpz_struct const *)(e_acsl_71));
- e_acsl_67 = e_acsl_72 == 0;
- mpz_clear((__mpz_struct *)(e_acsl_68));
- mpz_clear((__mpz_struct *)(e_acsl_69));
- mpz_clear((__mpz_struct *)(e_acsl_70));
- mpz_clear((__mpz_struct *)(e_acsl_71));
- } if (! e_acsl_67) { e_acsl_fail((char *)"(x == 1 ==> y == 1/0)"); }
- mpz_clear((__mpz_struct *)(e_acsl_64));
- mpz_clear((__mpz_struct *)(e_acsl_65));
+ e_acsl_64 = 1 / 0;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_65),(long)e_acsl_64);
+ e_acsl_66 = mpz_cmp((__mpz_struct const *)(e_acsl_63),
+ (__mpz_struct const *)(e_acsl_65));
+ e_acsl_62 = e_acsl_66 == 0;
+ mpz_clear((__mpz_struct *)(e_acsl_63));
+ mpz_clear((__mpz_struct *)(e_acsl_65));
+ } if (! e_acsl_62) { e_acsl_fail((char *)"(x == 1 ==> y == 1/0)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_59));
+ mpz_clear((__mpz_struct *)(e_acsl_60));
}
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
index d495b068a2cbb0f0f5a144e4604439602423977b..612d89375bd59c3ad62cc63a57d674c151abaaf7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
@@ -1,6 +1,8 @@
tests/e-acsl-runtime/ptr.i:12:[e-acsl] warning: missing guard for ensuring that p is a valid memory access
:0:[e-acsl] warning: missing guard for ensuring that 0 is a valid array index
tests/e-acsl-runtime/ptr.i:14:[e-acsl] warning: missing guard for ensuring that 2 is a valid array index
+tests/e-acsl-runtime/ptr.i:15:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
+:0:[e-acsl] warning: missing guard for ensuring that (2*sizeof(int))/sizeof((int)0x0) is a valid array index
tests/e-acsl-runtime/ptr.i:18:[e-acsl] warning: missing guard for ensuring that i is a valid array index
tests/e-acsl-runtime/ptr.i:19:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
:0:[e-acsl] warning: missing guard for ensuring that 2-i is a valid array index
@@ -95,32 +97,126 @@ PROJECT_FILE.i:154:[value] Assertion got status valid.
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:159.
[value] Done for function mpz_clear
-PROJECT_FILE.i:163:[value] entering loop for the first time
-PROJECT_FILE.i:165:[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:167.
+ 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:166.
[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <- main.
+ Called from PROJECT_FILE.i:167.
+PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_mul <- main.
+ Called from PROJECT_FILE.i:167.
+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:168.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:168.
[value] Done for function mpz_init_set_si
+[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:169.
-PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+PROJECT_FILE.i:170:[value] Assertion got status valid.
+[value] computing for function e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:171.
+[value] computing for function printf <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:125.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:125.
+[value] Done for function exit
+[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:172.
+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_get_si <- main.
+ Called from PROJECT_FILE.i:173.
+PROJECT_FILE.i:92:[value] Function mpz_get_si: precondition got status valid
+[value] Done for function mpz_get_si
+PROJECT_FILE.i:174:[kernel] warning: accessing out of bounds index [-2147483648..2147483647].
+ assert 0 ≤ e_acsl_17 ∧ e_acsl_17 < 3;
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:174.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:174.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:175.
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:177.
+[value] computing for function printf <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:125.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:125.
+[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:178.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:178.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:178.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:179.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:179.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:179.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:180.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:180.
+[value] Done for function mpz_clear
+PROJECT_FILE.i:184:[value] entering loop for the first time
+PROJECT_FILE.i:186:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <- main.
+ 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:189.
+[value] Done for function mpz_init_set_si
+[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 <- main.
+ Called from PROJECT_FILE.i:190.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:169.
+ Called from PROJECT_FILE.i:190.
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_cmp <- main.
- Called from PROJECT_FILE.i:170.
+ Called from PROJECT_FILE.i:191.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:171.
+ Called from PROJECT_FILE.i:192.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -130,59 +226,58 @@ 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:172.
+ Called from PROJECT_FILE.i:193.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:172.
+ Called from PROJECT_FILE.i:193.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:172.
+ Called from PROJECT_FILE.i:193.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:173.
+ Called from PROJECT_FILE.i:194.
[value] Done for function mpz_clear
-PROJECT_FILE.i:176:[value] Assertion got status valid.
+PROJECT_FILE.i:197:[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:200.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:180.
+ Called from PROJECT_FILE.i:201.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:180.
+ Called from PROJECT_FILE.i:201.
[value] Done for function mpz_init
[value] computing for function mpz_sub <- main.
- Called from PROJECT_FILE.i:181.
+ Called from PROJECT_FILE.i:202.
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_get_si <- main.
- Called from PROJECT_FILE.i:182.
-PROJECT_FILE.i:92:[value] Function mpz_get_si: precondition got status valid
+ Called from PROJECT_FILE.i:203.
[value] Done for function mpz_get_si
-PROJECT_FILE.i:183:[kernel] warning: accessing out of bounds index [-2147483648..2147483647].
- assert 0 ≤ e_acsl_18 ∧ e_acsl_18 < 3;
+PROJECT_FILE.i:204:[kernel] warning: accessing out of bounds index [-2147483648..2147483647].
+ assert 0 ≤ e_acsl_29 ∧ e_acsl_29 < 3;
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:183.
+ Called from PROJECT_FILE.i:204.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:183.
+ Called from PROJECT_FILE.i:204.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:184.
+ Called from PROJECT_FILE.i:205.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:184.
+ Called from PROJECT_FILE.i:205.
[value] Done for function mpz_init
[value] computing for function mpz_sub <- main.
- Called from PROJECT_FILE.i:185.
+ Called from PROJECT_FILE.i:206.
[value] Done for function mpz_sub
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:186.
+ Called from PROJECT_FILE.i:207.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:187.
+ Called from PROJECT_FILE.i:208.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -192,47 +287,47 @@ PROJECT_FILE.i:183:[kernel] warning: accessing out of bounds index [-2147483648.
[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:188.
+ Called from PROJECT_FILE.i:209.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:188.
+ Called from PROJECT_FILE.i:209.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:188.
+ Called from PROJECT_FILE.i:209.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:189.
+ Called from PROJECT_FILE.i:210.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:189.
+ Called from PROJECT_FILE.i:210.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:189.
+ Called from PROJECT_FILE.i:210.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:190.
+ Called from PROJECT_FILE.i:211.
[value] Done for function mpz_clear
-PROJECT_FILE.i:193:[value] Assertion got status valid.
+PROJECT_FILE.i:214:[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:216.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:196.
+ Called from PROJECT_FILE.i:217.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:196.
+ Called from PROJECT_FILE.i:217.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:197.
+ Called from PROJECT_FILE.i:218.
[value] Done for function mpz_init
[value] computing for function mpz_sub <- main.
- Called from PROJECT_FILE.i:197.
+ Called from PROJECT_FILE.i:218.
[value] Done for function mpz_sub
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:198.
+ Called from PROJECT_FILE.i:219.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:199.
+ Called from PROJECT_FILE.i:220.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -242,38 +337,38 @@ 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:200.
+ Called from PROJECT_FILE.i:221.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:200.
+ Called from PROJECT_FILE.i:221.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:200.
+ Called from PROJECT_FILE.i:221.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:201.
+ Called from PROJECT_FILE.i:222.
[value] Done for function mpz_clear
-PROJECT_FILE.i:165:[value] Assertion got status unknown.
+PROJECT_FILE.i:186:[value] Assertion got status unknown.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:167.
+ 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:168.
+ 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:168.
+ Called from PROJECT_FILE.i:189.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:169.
+ Called from PROJECT_FILE.i:190.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:169.
+ Called from PROJECT_FILE.i:190.
[value] Done for function mpz_add
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:170.
+ Called from PROJECT_FILE.i:191.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:171.
+ Called from PROJECT_FILE.i:192.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -283,53 +378,53 @@ PROJECT_FILE.i:165:[value] Assertion got status unknown.
[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:172.
+ Called from PROJECT_FILE.i:193.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:172.
+ Called from PROJECT_FILE.i:193.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:172.
+ Called from PROJECT_FILE.i:193.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:173.
+ Called from PROJECT_FILE.i:194.
[value] Done for function mpz_clear
-PROJECT_FILE.i:176:[value] Assertion got status unknown.
+PROJECT_FILE.i:197:[value] Assertion got status unknown.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:179.
+ Called from PROJECT_FILE.i:200.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:180.
+ Called from PROJECT_FILE.i:201.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:180.
+ Called from PROJECT_FILE.i:201.
[value] Done for function mpz_init
[value] computing for function mpz_sub <- main.
- Called from PROJECT_FILE.i:181.
+ Called from PROJECT_FILE.i:202.
[value] Done for function mpz_sub
[value] computing for function mpz_get_si <- main.
- Called from PROJECT_FILE.i:182.
+ Called from PROJECT_FILE.i:203.
[value] Done for function mpz_get_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:183.
+ Called from PROJECT_FILE.i:204.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:183.
+ Called from PROJECT_FILE.i:204.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:184.
+ Called from PROJECT_FILE.i:205.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:184.
+ Called from PROJECT_FILE.i:205.
[value] Done for function mpz_init
[value] computing for function mpz_sub <- main.
- Called from PROJECT_FILE.i:185.
+ Called from PROJECT_FILE.i:206.
[value] Done for function mpz_sub
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:186.
+ Called from PROJECT_FILE.i:207.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:187.
+ Called from PROJECT_FILE.i:208.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -339,47 +434,47 @@ PROJECT_FILE.i:176:[value] Assertion got status unknown.
[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:188.
+ Called from PROJECT_FILE.i:209.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:188.
+ Called from PROJECT_FILE.i:209.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:188.
+ Called from PROJECT_FILE.i:209.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:189.
+ Called from PROJECT_FILE.i:210.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:189.
+ Called from PROJECT_FILE.i:210.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:189.
+ Called from PROJECT_FILE.i:210.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:190.
+ Called from PROJECT_FILE.i:211.
[value] Done for function mpz_clear
-PROJECT_FILE.i:193:[value] Assertion got status unknown.
+PROJECT_FILE.i:214:[value] Assertion got status unknown.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:195.
+ Called from PROJECT_FILE.i:216.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:196.
+ Called from PROJECT_FILE.i:217.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:196.
+ Called from PROJECT_FILE.i:217.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:197.
+ Called from PROJECT_FILE.i:218.
[value] Done for function mpz_init
[value] computing for function mpz_sub <- main.
- Called from PROJECT_FILE.i:197.
+ Called from PROJECT_FILE.i:218.
[value] Done for function mpz_sub
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:198.
+ Called from PROJECT_FILE.i:219.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:199.
+ Called from PROJECT_FILE.i:220.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -389,30 +484,30 @@ PROJECT_FILE.i:193:[value] Assertion got status unknown.
[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:200.
+ Called from PROJECT_FILE.i:221.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:200.
+ Called from PROJECT_FILE.i:221.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:200.
+ Called from PROJECT_FILE.i:221.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:201.
+ Called from PROJECT_FILE.i:222.
[value] Done for function mpz_clear
-PROJECT_FILE.i:204:[value] assigning non deterministic value for the first time
-PROJECT_FILE.i:210:[value] Assertion got status valid.
+PROJECT_FILE.i:225:[value] assigning non deterministic value for the first time
+PROJECT_FILE.i:231:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:212.
+ Called from PROJECT_FILE.i:233.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:212.
+ Called from PROJECT_FILE.i:233.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:213.
+ Called from PROJECT_FILE.i:234.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:214.
+ Called from PROJECT_FILE.i:235.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
[value] Done for function printf
@@ -422,10 +517,10 @@ PROJECT_FILE.i:210:[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:215.
+ Called from PROJECT_FILE.i:236.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:215.
+ Called from PROJECT_FILE.i:236.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
@@ -445,12 +540,16 @@ PROJECT_FILE.i:125:[from] Non terminating function (no dependencies)
[from] Done for function mpz_clear
[from] Computing for function mpz_init
[from] Done for function mpz_init
+[from] Computing for function mpz_mul
+[from] Done for function mpz_mul
+[from] Computing for function mpz_cdiv_q
+[from] Done for function mpz_cdiv_q
+[from] Computing for function mpz_get_si
+[from] Done for function mpz_get_si
[from] Computing for function mpz_add
[from] Done for function mpz_add
[from] Computing for function mpz_sub
[from] Done for function mpz_sub
-[from] Computing for function mpz_get_si
-[from] Done for function mpz_get_si
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
@@ -499,6 +598,22 @@ extern void mpz_add(__mpz_struct * /*[1]*/ z1,
extern void mpz_sub(__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_mul(__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_cdiv_q(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2,
+ __mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z);
assigns \nothing; */
extern long mpz_get_si(__mpz_struct const * /*[1]*/ z);
@@ -559,77 +674,115 @@ int main(void)
mpz_clear((__mpz_struct *)(e_acsl_8));
}
+ /*@ assert t[(2*sizeof(int))/sizeof((int)0x0)] ≡ 4; */ ;
+ { mpz_t e_acsl_10; mpz_t e_acsl_11; mpz_t e_acsl_12; mpz_t e_acsl_13;
+ mpz_t e_acsl_14; int e_acsl_15; mpz_t e_acsl_16; int e_acsl_17;
+ mpz_t e_acsl_18; mpz_t e_acsl_19; int e_acsl_20;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_10),(long)2);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)4);
+ mpz_init((__mpz_struct *)(e_acsl_12));
+ mpz_mul((__mpz_struct *)(e_acsl_12),(__mpz_struct const *)(e_acsl_10),
+ (__mpz_struct const *)(e_acsl_11));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_13),(long)4);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_14),(long)0);
+ e_acsl_15 = mpz_cmp((__mpz_struct const *)(e_acsl_13),
+ (__mpz_struct const *)(e_acsl_14));
+ mpz_init((__mpz_struct *)(e_acsl_16));
+ /*@ assert sizeof((int)0x0) ≢ 0; */ ;
+ if (e_acsl_15 == 0) { e_acsl_fail((char *)"(sizeof((int)0x0) == 0)"); }
+ mpz_cdiv_q((__mpz_struct *)(e_acsl_16),(__mpz_struct const *)(e_acsl_12),
+ (__mpz_struct const *)(e_acsl_13));
+ e_acsl_17 = (int)mpz_get_si((__mpz_struct const *)(e_acsl_16));
+ /*@ assert 0 ≤ e_acsl_17 ∧ e_acsl_17 < 3;
+ // synthesized
+ */
+ mpz_init_set_si((__mpz_struct *)(e_acsl_18),(long)t[e_acsl_17]);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_19),(long)4);
+ e_acsl_20 = mpz_cmp((__mpz_struct const *)(e_acsl_18),
+ (__mpz_struct const *)(e_acsl_19));
+ if (! (e_acsl_20 == 0)) {
+ e_acsl_fail((char *)"(t[(2*sizeof(int))/sizeof((int)0x0)] == 4)");
+ } mpz_clear((__mpz_struct *)(e_acsl_10));
+ mpz_clear((__mpz_struct *)(e_acsl_11));
+ mpz_clear((__mpz_struct *)(e_acsl_12));
+ mpz_clear((__mpz_struct *)(e_acsl_13));
+ mpz_clear((__mpz_struct *)(e_acsl_14));
+ mpz_clear((__mpz_struct *)(e_acsl_16));
+ mpz_clear((__mpz_struct *)(e_acsl_18));
+ mpz_clear((__mpz_struct *)(e_acsl_19));
+ }
+
{ int i; i = 0;
while (1) {
if (! (i < 2)) { break; }
/*@ assert t[i] ≡ i+2; */ ;
- { mpz_t e_acsl_10; mpz_t e_acsl_11; mpz_t e_acsl_12; mpz_t e_acsl_13;
- int e_acsl_14;
- mpz_init_set_si((__mpz_struct *)(e_acsl_10),(long)t[i]);
- mpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)i);
- mpz_init_set_si((__mpz_struct *)(e_acsl_12),(long)2);
- mpz_init((__mpz_struct *)(e_acsl_13));
- mpz_add((__mpz_struct *)(e_acsl_13),
- (__mpz_struct const *)(e_acsl_11),
- (__mpz_struct const *)(e_acsl_12));
- e_acsl_14 = mpz_cmp((__mpz_struct const *)(e_acsl_10),
- (__mpz_struct const *)(e_acsl_13));
- if (! (e_acsl_14 == 0)) { e_acsl_fail((char *)"(t[i] == i+2)"); }
- mpz_clear((__mpz_struct *)(e_acsl_10));
- mpz_clear((__mpz_struct *)(e_acsl_11));
- mpz_clear((__mpz_struct *)(e_acsl_12));
- mpz_clear((__mpz_struct *)(e_acsl_13));
+ { mpz_t e_acsl_21; mpz_t e_acsl_22; mpz_t e_acsl_23; mpz_t e_acsl_24;
+ int e_acsl_25;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_21),(long)t[i]);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_22),(long)i);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_23),(long)2);
+ mpz_init((__mpz_struct *)(e_acsl_24));
+ mpz_add((__mpz_struct *)(e_acsl_24),
+ (__mpz_struct const *)(e_acsl_22),
+ (__mpz_struct const *)(e_acsl_23));
+ e_acsl_25 = mpz_cmp((__mpz_struct const *)(e_acsl_21),
+ (__mpz_struct const *)(e_acsl_24));
+ if (! (e_acsl_25 == 0)) { e_acsl_fail((char *)"(t[i] == i+2)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_21));
+ mpz_clear((__mpz_struct *)(e_acsl_22));
+ mpz_clear((__mpz_struct *)(e_acsl_23));
+ mpz_clear((__mpz_struct *)(e_acsl_24));
}
/*@ assert t[2-i] ≡ 4-i; */ ;
- { mpz_t e_acsl_15; mpz_t e_acsl_16; mpz_t e_acsl_17; int e_acsl_18;
- mpz_t e_acsl_19; mpz_t e_acsl_20; mpz_t e_acsl_21; mpz_t e_acsl_22;
- int e_acsl_23; mpz_init_set_si((__mpz_struct *)(e_acsl_15),(long)2);
- mpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)i);
- mpz_init((__mpz_struct *)(e_acsl_17));
- mpz_sub((__mpz_struct *)(e_acsl_17),
- (__mpz_struct const *)(e_acsl_15),
- (__mpz_struct const *)(e_acsl_16));
- e_acsl_18 = (int)mpz_get_si((__mpz_struct const *)(e_acsl_17));
- /*@ assert 0 ≤ e_acsl_18 ∧ e_acsl_18 < 3;
+ { mpz_t e_acsl_26; mpz_t e_acsl_27; mpz_t e_acsl_28; int 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_init_set_si((__mpz_struct *)(e_acsl_26),(long)2);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_27),(long)i);
+ mpz_init((__mpz_struct *)(e_acsl_28));
+ mpz_sub((__mpz_struct *)(e_acsl_28),
+ (__mpz_struct const *)(e_acsl_26),
+ (__mpz_struct const *)(e_acsl_27));
+ e_acsl_29 = (int)mpz_get_si((__mpz_struct const *)(e_acsl_28));
+ /*@ assert 0 ≤ e_acsl_29 ∧ e_acsl_29 < 3;
// synthesized
*/
- mpz_init_set_si((__mpz_struct *)(e_acsl_19),(long)t[e_acsl_18]);
- mpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)4);
- mpz_init_set_si((__mpz_struct *)(e_acsl_21),(long)i);
- mpz_init((__mpz_struct *)(e_acsl_22));
- mpz_sub((__mpz_struct *)(e_acsl_22),
- (__mpz_struct const *)(e_acsl_20),
- (__mpz_struct const *)(e_acsl_21));
- e_acsl_23 = mpz_cmp((__mpz_struct const *)(e_acsl_19),
- (__mpz_struct const *)(e_acsl_22));
- if (! (e_acsl_23 == 0)) { e_acsl_fail((char *)"(t[2-i] == 4-i)"); }
- mpz_clear((__mpz_struct *)(e_acsl_15));
- mpz_clear((__mpz_struct *)(e_acsl_16));
- mpz_clear((__mpz_struct *)(e_acsl_17));
- mpz_clear((__mpz_struct *)(e_acsl_19));
- mpz_clear((__mpz_struct *)(e_acsl_20));
- mpz_clear((__mpz_struct *)(e_acsl_21));
- mpz_clear((__mpz_struct *)(e_acsl_22));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_30),(long)t[e_acsl_29]);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_31),(long)4);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_32),(long)i);
+ mpz_init((__mpz_struct *)(e_acsl_33));
+ mpz_sub((__mpz_struct *)(e_acsl_33),
+ (__mpz_struct const *)(e_acsl_31),
+ (__mpz_struct const *)(e_acsl_32));
+ e_acsl_34 = mpz_cmp((__mpz_struct const *)(e_acsl_30),
+ (__mpz_struct const *)(e_acsl_33));
+ if (! (e_acsl_34 == 0)) { e_acsl_fail((char *)"(t[2-i] == 4-i)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_26));
+ mpz_clear((__mpz_struct *)(e_acsl_27));
+ mpz_clear((__mpz_struct *)(e_acsl_28));
+ 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));
}
/*@ assert *(&t[2]-i) ≡ 4-i; */ ;
- { mpz_t e_acsl_24; mpz_t e_acsl_25; mpz_t e_acsl_26; mpz_t e_acsl_27;
- int e_acsl_28;
- mpz_init_set_si((__mpz_struct *)(e_acsl_24),(long)*(& t[2] - i));
- mpz_init_set_si((__mpz_struct *)(e_acsl_25),(long)4);
- mpz_init_set_si((__mpz_struct *)(e_acsl_26),(long)i);
- mpz_init((__mpz_struct *)(e_acsl_27));
- mpz_sub((__mpz_struct *)(e_acsl_27),
- (__mpz_struct const *)(e_acsl_25),
- (__mpz_struct const *)(e_acsl_26));
- e_acsl_28 = mpz_cmp((__mpz_struct const *)(e_acsl_24),
- (__mpz_struct const *)(e_acsl_27));
- if (! (e_acsl_28 == 0)) { e_acsl_fail((char *)"(*(&t[2]-i) == 4-i)");
- } mpz_clear((__mpz_struct *)(e_acsl_24));
- mpz_clear((__mpz_struct *)(e_acsl_25));
- mpz_clear((__mpz_struct *)(e_acsl_26));
- mpz_clear((__mpz_struct *)(e_acsl_27));
+ { mpz_t e_acsl_35; mpz_t e_acsl_36; mpz_t e_acsl_37; mpz_t e_acsl_38;
+ int e_acsl_39;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_35),(long)*(& t[2] - i));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_36),(long)4);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_37),(long)i);
+ mpz_init((__mpz_struct *)(e_acsl_38));
+ mpz_sub((__mpz_struct *)(e_acsl_38),
+ (__mpz_struct const *)(e_acsl_36),
+ (__mpz_struct const *)(e_acsl_37));
+ e_acsl_39 = mpz_cmp((__mpz_struct const *)(e_acsl_35),
+ (__mpz_struct const *)(e_acsl_38));
+ if (! (e_acsl_39 == 0)) { e_acsl_fail((char *)"(*(&t[2]-i) == 4-i)");
+ } mpz_clear((__mpz_struct *)(e_acsl_35));
+ mpz_clear((__mpz_struct *)(e_acsl_36));
+ mpz_clear((__mpz_struct *)(e_acsl_37));
+ mpz_clear((__mpz_struct *)(e_acsl_38));
}
i ++;
@@ -639,14 +792,14 @@ int main(void)
p = & t[2];
t[2] = 5;
/*@ assert *p ≡ 5; */ ;
- { mpz_t e_acsl_29; mpz_t e_acsl_30; int e_acsl_31;
- mpz_init_set_si((__mpz_struct *)(e_acsl_29),(long)*p);
- mpz_init_set_si((__mpz_struct *)(e_acsl_30),(long)5);
- e_acsl_31 = mpz_cmp((__mpz_struct const *)(e_acsl_29),
- (__mpz_struct const *)(e_acsl_30));
- if (! (e_acsl_31 == 0)) { e_acsl_fail((char *)"(*p == 5)"); }
- mpz_clear((__mpz_struct *)(e_acsl_29));
- mpz_clear((__mpz_struct *)(e_acsl_30));
+ { mpz_t e_acsl_40; mpz_t e_acsl_41; int e_acsl_42;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_40),(long)*p);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_41),(long)5);
+ e_acsl_42 = mpz_cmp((__mpz_struct const *)(e_acsl_40),
+ (__mpz_struct const *)(e_acsl_41));
+ if (! (e_acsl_42 == 0)) { e_acsl_fail((char *)"(*p == 5)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_40));
+ mpz_clear((__mpz_struct *)(e_acsl_41));
}
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i b/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i
index 5c5faa229cf03e1261a841ecb12e2d60b61cfd34..e6864b08f8db15b1589d954569a3c9a5549f86e9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i
@@ -12,7 +12,7 @@ int main(void) {
/*@ assert *p == 1; */
/*@ assert *t == 2; */
/*@ assert *(t+2) == 4; */
- // /*@ assert *(t+2*sizeof(int)) == 4; */ // still this fucking subtyping bug
+ /*@ assert *(t+2*sizeof(int)/sizeof((int)0x0)) == 4; */
for(int i = 0; i < 2; i++) {
/*@ assert (*(t+i) == i+2); */ ;
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 81d795e314e81170e49b4f34660aa977b5ed575d..52fc32115d6ad793cfb20112a5affc7278b3d765 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -214,31 +214,44 @@ and context_insensitive_term_to_exp env t =
Such a case is actually possible. *)
assert (not (Mpz.is_t (typeOf e)));
new_exp ~loc (UnOp(LNot, e, intType)), env, false
- | TBinOp(PlusA | MinusA | Mult | Div | Mod as bop, t1, t2) ->
- (* arithmetic binary operator *)
+ | TBinOp(PlusA | MinusA | Mult as bop, t1, t2) ->
+ (* arithmetic binary operator not safely convertible into C *)
let e1, env = term_to_exp env Linteger t1 in
let e2, env = term_to_exp env Linteger t2 in
assert (Typ.equal (typeOf e1) (typeOf e2));
let name = name_of_mpz_arith_bop bop in
+ let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
+ let e, env = Env.new_var_and_mpz_init env mk_stmts in
+ e, env, false
+ | TBinOp(Div | Mod as bop, t1, t2) ->
+ (* arithmetic binary operator potentially convertible into C *)
+ let ctx = principal_type_from_term t1 t2 in
+ let e1, env = term_to_exp env ctx t1 in
+ let e2, env = term_to_exp env ctx t2 in
(* guarding divisions and modulos *)
let zero = Logic_const.tinteger ~ikind:IInt 0 in
- let guard, env = match bop with
- | Div | Mod -> comparison_to_exp env Eq t2 zero
- | _ -> Exp.dummy, env
+ (* do not generate [e2] from [t2] twice *)
+ let guard, env = comparison_to_exp env ~e1:(e2, ctx) Eq t2 zero in
+ let mk_stmts v e =
+ let name = name_of_mpz_arith_bop bop in
+ let cond =
+ Misc.mk_e_acsl_guard guard (Logic_const.prel (Req, t2, zero))
+ in
+ Env.add_assert cond (Logic_const.prel (Rneq, t2, zero));
+ let instr = match ctx with
+ | Ctype ty when isIntegralType ty ->
+ let e = new_exp ~loc (BinOp(bop, e1, e2, ty)) in
+ mkStmtOneInstr ~valid_sid:true (Set((Var v, NoOffset), e, loc))
+ | Linteger -> Misc.mk_call ~loc name [ e; e1; e2 ]
+ | _ -> assert false
+ in
+ [ cond; instr ]
in
- let mk_stmts _ e =
- let call = Misc.mk_call ~loc name [ e; e1; e2 ] in
- match bop with
- | Div | Mod ->
- let cond =
- Misc.mk_e_acsl_guard guard (Logic_const.prel (Req, t2, zero))
- in
- Env.add_assert cond (Logic_const.prel (Rneq, t2, zero));
- [ cond; call ]
- | _ ->
- [ call ]
+ let e, env = match ctx with
+ | Ctype ty when isIntegralType ty -> Env.new_var env ty mk_stmts
+ | Linteger -> Env.new_var_and_mpz_init env mk_stmts
+ | _ -> assert false
in
- let e, env = Env.new_var_and_mpz_init env mk_stmts in
e, env, false
| TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
(* comparison operators *)
@@ -304,11 +317,20 @@ and term_to_exp env ctx t =
context_sensitive ~loc:t.term_loc env ctx is_mpz_string e
(* generate the C code equivalent to [t1 bop t2]. *)
-and comparison_to_exp ?(loc=Location.unknown) env bop t1 t2 =
- let ctx = principal_type_from_term t1 t2 in
+and comparison_to_exp ?(loc=Location.unknown) ?e1 env bop t1 t2 =
+ let ctx = match e1 with
+ | None -> principal_type_from_term t1 t2
+ | Some(_, ctx) ->
+(* Options.feedback "principality oriented by %a" d_logic_type ctx;*)
+ principal_type_from_term { t1 with term_type = ctx } t2
+ in
(* Options.feedback "principal type of %a and %a is %a"
d_term t1 d_term t2 d_logic_type ctx;*)
- let e1, env = term_to_exp env ctx t1 in
+ let e1, env = match e1 with
+ | None -> term_to_exp env ctx t1
+ | Some(e1, ctx1) when Cil_datatype.Logic_type.equal ctx ctx1 -> e1, env
+ | Some(e1, _) -> context_sensitive ~loc:e1.eloc env ctx false e1
+ in
let e2, env = term_to_exp env ctx t2 in
match ctx with
| Linteger ->