diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index ccec0b43e6f6b4b8f9239cced908d73144d203fd..f2b0831be27079545fc61a38c280f7991a93b844 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -1,7 +1,8 @@
-- relation binaire sur les termes
-- use functions mpz_init_set* (optimization)
- see http://gmplib.org/manual-4.3.2/Simultaneous-Integer-Init-_0026-Assign.html#Simultaneous-Integer-Init-_0026-Assign
+- déboguer opérateurs binaires logiques
+- tester les opérations binaires sur les pointeurs
+
+- amélioration des locs quand possible (genre Prel)
- améliorer test "comparison.i" quand bug fixed #744
- remettre test "cast.i" quand bug fixed #744
diff --git a/src/plugins/e-acsl/share/e_acsl.h b/src/plugins/e-acsl/share/e_acsl.h
index 9969d4680907e05ea66da5e8601bea9608b2a8ac..3adf7bdabf0badcc8e9c130841dff864215b7d87 100644
--- a/src/plugins/e-acsl/share/e_acsl.h
+++ b/src/plugins/e-acsl/share/e_acsl.h
@@ -24,14 +24,12 @@ typedef __mpz_struct mpz_t[1];
/* GMP functions */
/*****************/
+// initilializers
+
/*@ ensures \valid(x);
@ assigns *x; */
extern void mpz_init(mpz_t x);
-/*@ requires \valid(x);
- @ assigns *x; */
-extern void mpz_clear(mpz_t x);
-
/*@ ensures \valid(z);
@ assigns *z; */
extern void mpz_init_set_ui(mpz_t z, unsigned long int n);
@@ -44,11 +42,59 @@ extern void mpz_init_set_si(mpz_t z, signed long int n);
@ assigns *z; */
extern void mpz_init_set_str(mpz_t z, char *str, int base);
+// finalizer
+
+/*@ requires \valid(x);
+ @ assigns *x; */
+extern void mpz_clear(mpz_t x);
+
+// logical and arithmetic operators
+
/*@ requires \valid(z1);
@ requires \valid(z2);
@ assigns \nothing; */
extern int mpz_cmp(mpz_t z1, mpz_t z2);
+/*@ requires \valid(z1);
+ @ requires \valid(z2);
+ @ assigns *z1; */
+extern int mpz_comp(mpz_t z1, mpz_t z2);
+
+/*@ requires \valid(z1);
+ @ requires \valid(z2);
+ @ assigns *z1; */
+extern int mpz_neg(mpz_t z1, mpz_t z2);
+
+/*@ requires \valid(z1);
+ @ requires \valid(z2);
+ @ requires \valid(z3);
+ @ assigns *z1; */
+extern int mpz_add(mpz_t z1, mpz_t z2, mpz_t z3);
+
+/*@ requires \valid(z1);
+ @ requires \valid(z2);
+ @ requires \valid(z3);
+ @ assigns *z1; */
+extern int mpz_sub(mpz_t z1, mpz_t z2, mpz_t z3);
+
+/*@ requires \valid(z1);
+ @ requires \valid(z2);
+ @ requires \valid(z3);
+ @ assigns *z1; */
+extern int mpz_mul(mpz_t z1, mpz_t z2, mpz_t z3);
+
+/*@ requires \valid(z1);
+ @ requires \valid(z2);
+ @ requires \valid(z3);
+ @ assigns *z1; */
+extern int mpz_cdiv_q(mpz_t z1, mpz_t z2, mpz_t z3);
+
+/*@ requires \valid(z1);
+ @ requires \valid(z2);
+ @ requires \valid(z3);
+ @ assigns *z1; */
+extern int mpz_mod(mpz_t z1, mpz_t z2, mpz_t z3);
+
/************************/
/* Standard C functions */
/************************/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i b/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
new file mode 100644
index 0000000000000000000000000000000000000000..10af162d0fdd586ccbf313ce586dda1d046d8551
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
@@ -0,0 +1,25 @@
+/* run.config
+ COMMENT: arithmetic operations */
+
+void main() {
+ int x = -3;
+ int y = 2;
+
+ /*@ assert -3 == x; */ ;
+ /*@ assert x == -3; */ ;
+ /*@ assert 0 != ~0; */ ;
+
+ /*@ assert x+1 == -2; */ ;
+ /*@ assert x-1 == -4; */ ;
+ /*@ assert x*3 == -9; */ ;
+ /*@ assert x/3 == -1; */ ;
+ /*@ assert x % 2 == -1; */ ;
+
+ /*@ assert x * 2 + (3 + y) - 4 + (x - y) == -10; */ ;
+
+ // /*@ assert (0 == 1) == !(0 == 0); */ ;
+
+ // /*@ assert 0 == !1; */ ;
+ /* subtyping relation: 0 should be promoted to boolean below
+ How to handle this? */
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
index d9e881f796ca61d3748d6b994ffd18c8b3c6b673..259d9adf95c3b7e647ecc5b8d8a8683cb498916e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
@@ -2,7 +2,7 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE:75:[value] Assertion got status valid.
+PROJECT_FILE:121:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[dominators] computing for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
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
new file mode 100644
index 0000000000000000000000000000000000000000..02dda29da5bde2d60059e3f57fe741b57235a9a2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -0,0 +1,918 @@
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+PROJECT_FILE:123:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:125.
+PROJECT_FILE:125:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:126.
+PROJECT_FILE:126:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_neg <-main.
+ Called from PROJECT_FILE:126.
+PROJECT_FILE:126:[value] Function mpz_neg: precondition got status valid
+[value] Done for function mpz_neg
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:127.
+PROJECT_FILE:127:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:128.
+PROJECT_FILE:128:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:129.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+PROJECT_FILE:115:[value] Function exit: postcondition got status invalid
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:130.
+PROJECT_FILE:130:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:130.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:131.
+PROJECT_FILE:131:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+PROJECT_FILE:134:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:136.
+PROJECT_FILE:136:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:137.
+PROJECT_FILE:137:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:137.
+PROJECT_FILE:137:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_neg <-main.
+ Called from PROJECT_FILE:138.
+PROJECT_FILE:138:[value] Function mpz_neg: precondition got status valid
+[value] Done for function mpz_neg
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:139.
+PROJECT_FILE:139:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:140.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:141.
+PROJECT_FILE:141:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:141.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:142.
+PROJECT_FILE:142:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+PROJECT_FILE:145:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:147.
+PROJECT_FILE:147:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:148.
+PROJECT_FILE:148:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:148.
+PROJECT_FILE:148:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_com <-main.
+ Called from PROJECT_FILE:149.
+[kernel] No code for function mpz_com, default assigns generated
+[value] Done for function mpz_com
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:150.
+PROJECT_FILE:150:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:151.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:152.
+PROJECT_FILE:152:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:152.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:153.
+PROJECT_FILE:153:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+PROJECT_FILE:156:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:159.
+PROJECT_FILE:159:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:159.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:160.
+PROJECT_FILE:160:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_add <-main.
+ Called from PROJECT_FILE:160.
+PROJECT_FILE:160:[value] Function mpz_add: precondition got status valid
+[value] Done for function mpz_add
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:161.
+PROJECT_FILE:161:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:161.
+PROJECT_FILE:161:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_neg <-main.
+ Called from PROJECT_FILE:162.
+PROJECT_FILE:162:[value] Function mpz_neg: precondition got status valid
+[value] Done for function mpz_neg
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:163.
+PROJECT_FILE:163:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:164.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:165.
+PROJECT_FILE:165:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:165.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:166.
+PROJECT_FILE:166:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:166.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:167.
+PROJECT_FILE:167:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+PROJECT_FILE:170:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:173.
+PROJECT_FILE:173:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:173.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:174.
+PROJECT_FILE:174:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_sub <-main.
+ Called from PROJECT_FILE:174.
+PROJECT_FILE:174:[value] Function mpz_sub: precondition got status valid
+[value] Done for function mpz_sub
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:175.
+PROJECT_FILE:175:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:175.
+PROJECT_FILE:175:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_neg <-main.
+ Called from PROJECT_FILE:176.
+PROJECT_FILE:176:[value] Function mpz_neg: precondition got status valid
+[value] Done for function mpz_neg
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:177.
+PROJECT_FILE:177:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:178.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:179.
+PROJECT_FILE:179:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:179.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:180.
+PROJECT_FILE:180:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:180.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:181.
+PROJECT_FILE:181:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+PROJECT_FILE:184:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:187.
+PROJECT_FILE:187:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:187.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:188.
+PROJECT_FILE:188:[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:188.
+PROJECT_FILE:188:[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:189.
+PROJECT_FILE:189:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:189.
+PROJECT_FILE:189:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_neg <-main.
+ Called from PROJECT_FILE:190.
+PROJECT_FILE:190:[value] Function mpz_neg: precondition got status valid
+[value] Done for function mpz_neg
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:191.
+PROJECT_FILE:191:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:192.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:193.
+PROJECT_FILE:193:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:193.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:194.
+PROJECT_FILE:194:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:194.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:195.
+PROJECT_FILE:195:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+PROJECT_FILE:198:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:201.
+PROJECT_FILE:201:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:201.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:202.
+PROJECT_FILE:202:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_cdiv_q <-main.
+ Called from PROJECT_FILE:203.
+PROJECT_FILE:203:[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:204.
+PROJECT_FILE:204:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:204.
+PROJECT_FILE:204:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_neg <-main.
+ Called from PROJECT_FILE:205.
+PROJECT_FILE:205:[value] Function mpz_neg: precondition got status valid
+[value] Done for function mpz_neg
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:206.
+PROJECT_FILE:206:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:207.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:208.
+PROJECT_FILE:208:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:208.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:209.
+PROJECT_FILE:209:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:209.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:210.
+PROJECT_FILE:210:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+PROJECT_FILE:213:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:216.
+PROJECT_FILE:216:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:216.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:217.
+PROJECT_FILE:217:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_mod <-main.
+ Called from PROJECT_FILE:217.
+PROJECT_FILE:217:[value] Function mpz_mod: precondition got status valid
+[value] Done for function mpz_mod
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:218.
+PROJECT_FILE:218:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:218.
+PROJECT_FILE:218:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_neg <-main.
+ Called from PROJECT_FILE:219.
+PROJECT_FILE:219:[value] Function mpz_neg: precondition got status valid
+[value] Done for function mpz_neg
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:220.
+PROJECT_FILE:220:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:221.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:222.
+PROJECT_FILE:222:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:222.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:223.
+PROJECT_FILE:223:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:223.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:224.
+PROJECT_FILE:224:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+PROJECT_FILE:227:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:233.
+PROJECT_FILE:233:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:234.
+PROJECT_FILE:234:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:234.
+PROJECT_FILE:234:[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:235.
+PROJECT_FILE:235:[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:236.
+PROJECT_FILE:236:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:236.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:237.
+PROJECT_FILE:237:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_add <-main.
+ Called from PROJECT_FILE:237.
+PROJECT_FILE:237:[value] Function mpz_add: precondition got status valid
+[value] Done for function mpz_add
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:238.
+PROJECT_FILE:238:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_add <-main.
+ Called from PROJECT_FILE:238.
+PROJECT_FILE:238:[value] Function mpz_add: precondition got status valid
+[value] Done for function mpz_add
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:239.
+PROJECT_FILE:239:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:239.
+PROJECT_FILE:239:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_sub <-main.
+ Called from PROJECT_FILE:240.
+PROJECT_FILE:240:[value] Function mpz_sub: precondition got status valid
+[value] Done for function mpz_sub
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:241.
+PROJECT_FILE:241:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:241.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:242.
+PROJECT_FILE:242:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_sub <-main.
+ Called from PROJECT_FILE:243.
+PROJECT_FILE:243:[value] Function mpz_sub: precondition got status valid
+[value] Done for function mpz_sub
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:244.
+PROJECT_FILE:244:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_add <-main.
+ Called from PROJECT_FILE:245.
+PROJECT_FILE:245:[value] Function mpz_add: precondition got status valid
+[value] Done for function mpz_add
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:246.
+PROJECT_FILE:246:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:246.
+PROJECT_FILE:246:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_neg <-main.
+ Called from PROJECT_FILE:247.
+PROJECT_FILE:247:[value] Function mpz_neg: precondition got status valid
+[value] Done for function mpz_neg
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:248.
+PROJECT_FILE:248:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:250.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:115.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:251.
+PROJECT_FILE:251:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:251.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:252.
+PROJECT_FILE:252:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:252.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:253.
+PROJECT_FILE:253:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:253.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:254.
+PROJECT_FILE:254:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:254.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:255.
+PROJECT_FILE:255:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:255.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:256.
+PROJECT_FILE:256:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:256.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:257.
+PROJECT_FILE:257:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:257.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:258.
+PROJECT_FILE:258:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] Recording results for main
+[value] done for function main
+[from] Computing for function mpz_init_set_si
+[from] Done for function mpz_init_set_si
+[from] Computing for function mpz_init
+[from] Done for function mpz_init
+[from] Computing for function mpz_neg
+[from] Done for function mpz_neg
+[from] Computing for function mpz_cmp
+[from] Done for function mpz_cmp
+[from] Computing for function e_acsl_fail
+[from] Computing for function eprintf <-e_acsl_fail
+[from] Done for function eprintf
+[from] Computing for function exit <-e_acsl_fail
+[from] Done for function exit
+PROJECT_FILE:115:[from] Non terminating function (no dependencies)
+[from] Done for function e_acsl_fail
+[from] Computing for function mpz_clear
+[from] Done for function mpz_clear
+[from] Computing for function mpz_com
+[from] Done for function mpz_com
+[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_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_mod
+[from] Done for function mpz_mod
+[dominators] computing for function main
+[dominators] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values for function e_acsl_fail:
+ NON TERMINATING FUNCTION
+[value] Values for function main:
+ x ∈ {-3; }
+ y ∈ {2; }
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct mpz_t[1];
+/*@ ensures \valid(\at(x,Old));
+ assigns *x; */
+extern void mpz_init(__mpz_struct * /*[1]*/ x ) ;
+/*@ ensures \valid(\at(z,Old));
+ assigns *z; */
+extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
+/*@ requires \valid(x);
+ assigns *x; */
+extern void mpz_clear(__mpz_struct * /*[1]*/ x ) ;
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern int mpz_cmp(__mpz_struct * /*[1]*/ z1 , __mpz_struct * /*[1]*/ z2 ) ;
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns *z1; */
+extern int mpz_neg(__mpz_struct * /*[1]*/ z1 , __mpz_struct * /*[1]*/ z2 ) ;
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+*/
+extern int mpz_add(__mpz_struct * /*[1]*/ z1 , __mpz_struct * /*[1]*/ z2 ,
+ __mpz_struct * /*[1]*/ z3 ) ;
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+*/
+extern int mpz_sub(__mpz_struct * /*[1]*/ z1 , __mpz_struct * /*[1]*/ z2 ,
+ __mpz_struct * /*[1]*/ z3 ) ;
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+*/
+extern int mpz_mul(__mpz_struct * /*[1]*/ z1 , __mpz_struct * /*[1]*/ z2 ,
+ __mpz_struct * /*[1]*/ z3 ) ;
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+*/
+extern int mpz_cdiv_q(__mpz_struct * /*[1]*/ z1 ,
+ __mpz_struct * /*[1]*/ z2 ,
+ __mpz_struct * /*[1]*/ z3 ) ;
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+*/
+extern int mpz_mod(__mpz_struct * /*[1]*/ z1 , __mpz_struct * /*[1]*/ z2 ,
+ __mpz_struct * /*[1]*/ z3 ) ;
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status ) ;
+/*@ assigns \nothing; */
+extern void eprintf(char * ) ;
+void e_acsl_fail(char *msg )
+{
+ eprintf(msg);
+ exit(1);
+ return;
+}
+
+/*@ behavior generated:
+ assigns \at(\result,Post) \from \nothing; */
+extern int ( /* missing proto */ mpz_com)() ;
+void main(void)
+{
+ int x ;
+ int y ;
+ x = -3;
+ y = 2;
+ /*@ assert (-3 ≡ x); */ ;
+ { mpz_t e_acsl_cst_1 ; mpz_t e_acsl_cst_2 ; mpz_t e_acsl_cst_3 ;
+ int e_acsl_cst_4 ;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_1),(long )3);
+ mpz_init((__mpz_struct *)(e_acsl_cst_2));
+ mpz_neg((__mpz_struct *)(e_acsl_cst_2),(__mpz_struct *)(e_acsl_cst_1));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_3),(long )x);
+ e_acsl_cst_4 = mpz_cmp((__mpz_struct *)(e_acsl_cst_2),
+ (__mpz_struct *)(e_acsl_cst_3));
+ if (e_acsl_cst_4 != 0) { e_acsl_fail((char *)"((-3 == x))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_cst_1));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_2));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_3));
+ }
+
+ /*@ assert (x ≡ -3); */ ;
+ { mpz_t e_acsl_cst_5 ; mpz_t e_acsl_cst_6 ; mpz_t e_acsl_cst_7 ;
+ int e_acsl_cst_8 ;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_5),(long )x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_6),(long )3);
+ mpz_init((__mpz_struct *)(e_acsl_cst_7));
+ mpz_neg((__mpz_struct *)(e_acsl_cst_7),(__mpz_struct *)(e_acsl_cst_6));
+ e_acsl_cst_8 = mpz_cmp((__mpz_struct *)(e_acsl_cst_5),
+ (__mpz_struct *)(e_acsl_cst_7));
+ if (e_acsl_cst_8 != 0) { e_acsl_fail((char *)"((x == -3))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_cst_5));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_6));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_7));
+ }
+
+ /*@ assert (0 ≢ ~0); */ ;
+ { mpz_t e_acsl_cst_9 ; mpz_t e_acsl_cst_10 ; mpz_t e_acsl_cst_11 ;
+ int e_acsl_cst_12 ;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_9),(long )0);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_10),(long )0);
+ mpz_init((__mpz_struct *)(e_acsl_cst_11));
+ mpz_com(e_acsl_cst_11,e_acsl_cst_10);
+ e_acsl_cst_12 = mpz_cmp((__mpz_struct *)(e_acsl_cst_9),
+ (__mpz_struct *)(e_acsl_cst_11));
+ if (e_acsl_cst_12 == 0) { e_acsl_fail((char *)"((0 != ~0))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_cst_9));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_10));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_11));
+ }
+
+ /*@ assert (x+1 ≡ -2); */ ;
+ { mpz_t e_acsl_cst_13 ; mpz_t e_acsl_cst_14 ; mpz_t e_acsl_cst_15 ;
+ mpz_t e_acsl_cst_16 ; mpz_t e_acsl_cst_17 ; int e_acsl_cst_18 ;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_13),(long )x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_14),(long )1);
+ mpz_init((__mpz_struct *)(e_acsl_cst_15));
+ mpz_add((__mpz_struct *)(e_acsl_cst_15),(__mpz_struct *)(e_acsl_cst_13),
+ (__mpz_struct *)(e_acsl_cst_14));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_16),(long )2);
+ mpz_init((__mpz_struct *)(e_acsl_cst_17));
+ mpz_neg((__mpz_struct *)(e_acsl_cst_17),(__mpz_struct *)(e_acsl_cst_16));
+ e_acsl_cst_18 = mpz_cmp((__mpz_struct *)(e_acsl_cst_15),
+ (__mpz_struct *)(e_acsl_cst_17));
+ if (e_acsl_cst_18 != 0) { e_acsl_fail((char *)"((x+1 == -2))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_cst_13));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_14));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_15));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_16));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_17));
+ }
+
+ /*@ assert (x-1 ≡ -4); */ ;
+ { mpz_t e_acsl_cst_19 ; mpz_t e_acsl_cst_20 ; mpz_t e_acsl_cst_21 ;
+ mpz_t e_acsl_cst_22 ; mpz_t e_acsl_cst_23 ; int e_acsl_cst_24 ;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_19),(long )x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_20),(long )1);
+ mpz_init((__mpz_struct *)(e_acsl_cst_21));
+ mpz_sub((__mpz_struct *)(e_acsl_cst_21),(__mpz_struct *)(e_acsl_cst_19),
+ (__mpz_struct *)(e_acsl_cst_20));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_22),(long )4);
+ mpz_init((__mpz_struct *)(e_acsl_cst_23));
+ mpz_neg((__mpz_struct *)(e_acsl_cst_23),(__mpz_struct *)(e_acsl_cst_22));
+ e_acsl_cst_24 = mpz_cmp((__mpz_struct *)(e_acsl_cst_21),
+ (__mpz_struct *)(e_acsl_cst_23));
+ if (e_acsl_cst_24 != 0) { e_acsl_fail((char *)"((x-1 == -4))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_cst_19));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_20));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_21));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_22));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_23));
+ }
+
+ /*@ assert (x*3 ≡ -9); */ ;
+ { mpz_t e_acsl_cst_25 ; mpz_t e_acsl_cst_26 ; mpz_t e_acsl_cst_27 ;
+ mpz_t e_acsl_cst_28 ; mpz_t e_acsl_cst_29 ; int e_acsl_cst_30 ;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_25),(long )x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_26),(long )3);
+ mpz_init((__mpz_struct *)(e_acsl_cst_27));
+ mpz_mul((__mpz_struct *)(e_acsl_cst_27),(__mpz_struct *)(e_acsl_cst_25),
+ (__mpz_struct *)(e_acsl_cst_26));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_28),(long )9);
+ mpz_init((__mpz_struct *)(e_acsl_cst_29));
+ mpz_neg((__mpz_struct *)(e_acsl_cst_29),(__mpz_struct *)(e_acsl_cst_28));
+ e_acsl_cst_30 = mpz_cmp((__mpz_struct *)(e_acsl_cst_27),
+ (__mpz_struct *)(e_acsl_cst_29));
+ if (e_acsl_cst_30 != 0) { e_acsl_fail((char *)"((x*3 == -9))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_cst_25));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_26));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_27));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_28));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_29));
+ }
+
+ /*@ assert (x/3 ≡ -1); */ ;
+ { mpz_t e_acsl_cst_31 ; mpz_t e_acsl_cst_32 ; mpz_t e_acsl_cst_33 ;
+ mpz_t e_acsl_cst_34 ; mpz_t e_acsl_cst_35 ; int e_acsl_cst_36 ;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_31),(long )x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_32),(long )3);
+ mpz_init((__mpz_struct *)(e_acsl_cst_33));
+ mpz_cdiv_q((__mpz_struct *)(e_acsl_cst_33),
+ (__mpz_struct *)(e_acsl_cst_31),
+ (__mpz_struct *)(e_acsl_cst_32));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_34),(long )1);
+ mpz_init((__mpz_struct *)(e_acsl_cst_35));
+ mpz_neg((__mpz_struct *)(e_acsl_cst_35),(__mpz_struct *)(e_acsl_cst_34));
+ e_acsl_cst_36 = mpz_cmp((__mpz_struct *)(e_acsl_cst_33),
+ (__mpz_struct *)(e_acsl_cst_35));
+ if (e_acsl_cst_36 != 0) { e_acsl_fail((char *)"((x/3 == -1))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_cst_31));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_32));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_33));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_34));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_35));
+ }
+
+ /*@ assert (x%2 ≡ -1); */ ;
+ { mpz_t e_acsl_cst_37 ; mpz_t e_acsl_cst_38 ; mpz_t e_acsl_cst_39 ;
+ mpz_t e_acsl_cst_40 ; mpz_t e_acsl_cst_41 ; int e_acsl_cst_42 ;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_37),(long )x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_38),(long )2);
+ mpz_init((__mpz_struct *)(e_acsl_cst_39));
+ mpz_mod((__mpz_struct *)(e_acsl_cst_39),(__mpz_struct *)(e_acsl_cst_37),
+ (__mpz_struct *)(e_acsl_cst_38));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_40),(long )1);
+ mpz_init((__mpz_struct *)(e_acsl_cst_41));
+ mpz_neg((__mpz_struct *)(e_acsl_cst_41),(__mpz_struct *)(e_acsl_cst_40));
+ e_acsl_cst_42 = mpz_cmp((__mpz_struct *)(e_acsl_cst_39),
+ (__mpz_struct *)(e_acsl_cst_41));
+ if (e_acsl_cst_42 != 0) { e_acsl_fail((char *)"((x%2 == -1))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_cst_37));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_38));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_39));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_40));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_41));
+ }
+
+ /*@ assert (((x*2+(3+y))-4)+(x-y) ≡ -10); */ ;
+ { mpz_t e_acsl_cst_43 ; mpz_t e_acsl_cst_44 ; mpz_t e_acsl_cst_45 ;
+ mpz_t e_acsl_cst_46 ; mpz_t e_acsl_cst_47 ; mpz_t e_acsl_cst_48 ;
+ mpz_t e_acsl_cst_49 ; mpz_t e_acsl_cst_50 ; mpz_t e_acsl_cst_51 ;
+ mpz_t e_acsl_cst_52 ; mpz_t e_acsl_cst_53 ; mpz_t e_acsl_cst_54 ;
+ mpz_t e_acsl_cst_55 ; mpz_t e_acsl_cst_56 ; mpz_t e_acsl_cst_57 ;
+ int e_acsl_cst_58 ;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_43),(long )x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_44),(long )2);
+ mpz_init((__mpz_struct *)(e_acsl_cst_45));
+ mpz_mul((__mpz_struct *)(e_acsl_cst_45),(__mpz_struct *)(e_acsl_cst_43),
+ (__mpz_struct *)(e_acsl_cst_44));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_46),(long )3);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_47),(long )y);
+ mpz_init((__mpz_struct *)(e_acsl_cst_48));
+ mpz_add((__mpz_struct *)(e_acsl_cst_48),(__mpz_struct *)(e_acsl_cst_46),
+ (__mpz_struct *)(e_acsl_cst_47));
+ mpz_init((__mpz_struct *)(e_acsl_cst_49));
+ mpz_add((__mpz_struct *)(e_acsl_cst_49),(__mpz_struct *)(e_acsl_cst_45),
+ (__mpz_struct *)(e_acsl_cst_48));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_50),(long )4);
+ mpz_init((__mpz_struct *)(e_acsl_cst_51));
+ mpz_sub((__mpz_struct *)(e_acsl_cst_51),(__mpz_struct *)(e_acsl_cst_49),
+ (__mpz_struct *)(e_acsl_cst_50));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_52),(long )x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_53),(long )y);
+ mpz_init((__mpz_struct *)(e_acsl_cst_54));
+ mpz_sub((__mpz_struct *)(e_acsl_cst_54),(__mpz_struct *)(e_acsl_cst_52),
+ (__mpz_struct *)(e_acsl_cst_53));
+ mpz_init((__mpz_struct *)(e_acsl_cst_55));
+ mpz_add((__mpz_struct *)(e_acsl_cst_55),(__mpz_struct *)(e_acsl_cst_51),
+ (__mpz_struct *)(e_acsl_cst_54));
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_56),(long )10);
+ mpz_init((__mpz_struct *)(e_acsl_cst_57));
+ mpz_neg((__mpz_struct *)(e_acsl_cst_57),(__mpz_struct *)(e_acsl_cst_56));
+ e_acsl_cst_58 = mpz_cmp((__mpz_struct *)(e_acsl_cst_55),
+ (__mpz_struct *)(e_acsl_cst_57));
+ if (e_acsl_cst_58 != 0) {
+ e_acsl_fail((char *)"((((x*2+(3+y))-4)+(x-y) == -10))");
+ } mpz_clear((__mpz_struct *)(e_acsl_cst_43));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_44));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_45));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_46));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_47));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_48));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_49));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_50));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_51));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_52));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_53));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_54));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_55));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_56));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_57));
+ }
+
+ return;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index 2d2ef36e82c14605bf8bc8ab4e9ee5b6ee7da2cc..65e7759f474f9152816eb3690546688c99d95714 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -2,298 +2,298 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE:78:[value] Assertion got status valid.
+PROJECT_FILE:124:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:80.
-PROJECT_FILE:80:[value] Function mpz_init_set_si: postcondition got status unknown
+ Called from PROJECT_FILE:126.
+PROJECT_FILE:126:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:80.
+ Called from PROJECT_FILE:126.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:81.
-PROJECT_FILE:81:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:127.
+PROJECT_FILE:127:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:82.
+ Called from PROJECT_FILE:128.
[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
-PROJECT_FILE:69:[value] Function exit: postcondition got status invalid
+ Called from PROJECT_FILE:115.
+PROJECT_FILE:115:[value] Function exit: postcondition got status invalid
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:83.
-PROJECT_FILE:83:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:129.
+PROJECT_FILE:129:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:83.
+ Called from PROJECT_FILE:129.
[value] Done for function mpz_clear
-PROJECT_FILE:86:[value] Assertion got status valid.
+PROJECT_FILE:132:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:88.
-PROJECT_FILE:88:[value] Function mpz_init_set_si: postcondition got status unknown
+ Called from PROJECT_FILE:134.
+PROJECT_FILE:134:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:88.
+ Called from PROJECT_FILE:134.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:89.
-PROJECT_FILE:89:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:135.
+PROJECT_FILE:135:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:90.
+ Called from PROJECT_FILE:136.
[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:91.
-PROJECT_FILE:91:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:137.
+PROJECT_FILE:137:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:91.
+ Called from PROJECT_FILE:137.
[value] Done for function mpz_clear
-PROJECT_FILE:94:[value] Assertion got status valid.
+PROJECT_FILE:140:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:96.
-PROJECT_FILE:96:[value] Function mpz_init_set_si: postcondition got status unknown
+ Called from PROJECT_FILE:142.
+PROJECT_FILE:142:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:96.
+ Called from PROJECT_FILE:142.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:97.
-PROJECT_FILE:97:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:143.
+PROJECT_FILE:143:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:98.
+ Called from PROJECT_FILE:144.
[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:99.
-PROJECT_FILE:99:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:145.
+PROJECT_FILE:145:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:99.
+ Called from PROJECT_FILE:145.
[value] Done for function mpz_clear
-PROJECT_FILE:102:[value] Assertion got status valid.
+PROJECT_FILE:148:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:104.
-PROJECT_FILE:104:[value] Function mpz_init_set_si: postcondition got status unknown
+ Called from PROJECT_FILE:150.
+PROJECT_FILE:150:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:104.
+ Called from PROJECT_FILE:150.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:105.
-PROJECT_FILE:105:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:151.
+PROJECT_FILE:151:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:106.
+ Called from PROJECT_FILE:152.
[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:107.
-PROJECT_FILE:107:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:153.
+PROJECT_FILE:153:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:107.
+ Called from PROJECT_FILE:153.
[value] Done for function mpz_clear
-PROJECT_FILE:111:[value] Assertion got status valid.
-PROJECT_FILE:114:[value] Assertion got status valid.
-PROJECT_FILE:117:[value] Assertion got status valid.
+PROJECT_FILE:157:[value] Assertion got status valid.
+PROJECT_FILE:160:[value] Assertion got status valid.
+PROJECT_FILE:163:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:119.
-PROJECT_FILE:119:[value] Function mpz_init_set_si: postcondition got status unknown
+ Called from PROJECT_FILE:165.
+PROJECT_FILE:165:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:119.
+ Called from PROJECT_FILE:165.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:120.
-PROJECT_FILE:120:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:166.
+PROJECT_FILE:166:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:121.
+ Called from PROJECT_FILE:167.
[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:122.
-PROJECT_FILE:122:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:168.
+PROJECT_FILE:168:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:122.
+ Called from PROJECT_FILE:168.
[value] Done for function mpz_clear
-PROJECT_FILE:125:[value] Assertion got status valid.
+PROJECT_FILE:171:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:127.
-PROJECT_FILE:127:[value] Function mpz_init_set_si: postcondition got status unknown
+ Called from PROJECT_FILE:173.
+PROJECT_FILE:173:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:127.
+ Called from PROJECT_FILE:173.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:128.
-PROJECT_FILE:128:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:174.
+PROJECT_FILE:174:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:129.
+ Called from PROJECT_FILE:175.
[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:130.
-PROJECT_FILE:130:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:176.
+PROJECT_FILE:176:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:130.
+ Called from PROJECT_FILE:176.
[value] Done for function mpz_clear
-PROJECT_FILE:133:[value] Assertion got status valid.
+PROJECT_FILE:179:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:135.
-PROJECT_FILE:135:[value] Function mpz_init_set_si: postcondition got status unknown
+ Called from PROJECT_FILE:181.
+PROJECT_FILE:181:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:135.
+ Called from PROJECT_FILE:181.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:136.
-PROJECT_FILE:136:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:182.
+PROJECT_FILE:182:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:137.
+ Called from PROJECT_FILE:183.
[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:138.
-PROJECT_FILE:138:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:184.
+PROJECT_FILE:184:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:138.
+ Called from PROJECT_FILE:184.
[value] Done for function mpz_clear
-PROJECT_FILE:141:[value] Assertion got status valid.
+PROJECT_FILE:187:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:143.
-PROJECT_FILE:143:[value] Function mpz_init_set_si: postcondition got status unknown
+ Called from PROJECT_FILE:189.
+PROJECT_FILE:189:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:143.
+ Called from PROJECT_FILE:189.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:144.
-PROJECT_FILE:144:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:190.
+PROJECT_FILE:190:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:145.
+ Called from PROJECT_FILE:191.
[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:146.
-PROJECT_FILE:146:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:192.
+PROJECT_FILE:192:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:146.
+ Called from PROJECT_FILE:192.
[value] Done for function mpz_clear
-PROJECT_FILE:149:[value] Assertion got status valid.
+PROJECT_FILE:195:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:151.
-PROJECT_FILE:151:[value] Function mpz_init_set_si: postcondition got status unknown
+ Called from PROJECT_FILE:197.
+PROJECT_FILE:197:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:151.
+ Called from PROJECT_FILE:197.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:152.
-PROJECT_FILE:152:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:198.
+PROJECT_FILE:198:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:153.
+ Called from PROJECT_FILE:199.
[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:154.
-PROJECT_FILE:154:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:200.
+PROJECT_FILE:200:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:154.
+ Called from PROJECT_FILE:200.
[value] Done for function mpz_clear
-PROJECT_FILE:157:[value] Assertion got status valid.
+PROJECT_FILE:203:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:159.
-PROJECT_FILE:159:[value] Function mpz_init_set_si: postcondition got status unknown
+ Called from PROJECT_FILE:205.
+PROJECT_FILE:205:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:159.
+ Called from PROJECT_FILE:205.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:160.
-PROJECT_FILE:160:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:206.
+PROJECT_FILE:206:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:161.
+ Called from PROJECT_FILE:207.
[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:162.
-PROJECT_FILE:162:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:208.
+PROJECT_FILE:208:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:162.
+ Called from PROJECT_FILE:208.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
@@ -306,7 +306,7 @@ PROJECT_FILE:162:[value] Function mpz_clear: precondition got status valid
[from] Done for function eprintf
[from] Computing for function exit <-e_acsl_fail
[from] Done for function exit
-PROJECT_FILE:69:[from] Non terminating function (no dependencies)
+PROJECT_FILE:115:[from] Non terminating function (no dependencies)
[from] Done for function e_acsl_fail
[from] Computing for function mpz_clear
[from] Done for function mpz_clear
@@ -327,12 +327,12 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct mpz_t[1];
-/*@ requires \valid(x);
- assigns *x; */
-extern void mpz_clear(__mpz_struct * /*[1]*/ x ) ;
/*@ ensures \valid(\at(z,Old));
assigns *z; */
extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
+/*@ requires \valid(x);
+ assigns *x; */
+extern void mpz_clear(__mpz_struct * /*[1]*/ x ) ;
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index 9be9cc4733af9796cdc9829217d545e63c83b0e0..7b331b4436c58589d9a134f3b8982387375cd52a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -2,94 +2,94 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE:73:[value] Assertion got status valid.
+PROJECT_FILE:119:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:75.
-PROJECT_FILE:75:[value] Function mpz_init_set_si: postcondition got status unknown
+ Called from PROJECT_FILE:121.
+PROJECT_FILE:121:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:75.
+ Called from PROJECT_FILE:121.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:76.
-PROJECT_FILE:76:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:122.
+PROJECT_FILE:122:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:77.
+ Called from PROJECT_FILE:123.
[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
-PROJECT_FILE:69:[value] Function exit: postcondition got status invalid
+ Called from PROJECT_FILE:115.
+PROJECT_FILE:115:[value] Function exit: postcondition got status invalid
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:78.
-PROJECT_FILE:78:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:124.
+PROJECT_FILE:124:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:78.
+ Called from PROJECT_FILE:124.
[value] Done for function mpz_clear
-PROJECT_FILE:81:[value] Assertion got status valid.
+PROJECT_FILE:127:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:83.
-PROJECT_FILE:83:[value] Function mpz_init_set_si: postcondition got status unknown
+ Called from PROJECT_FILE:129.
+PROJECT_FILE:129:[value] Function mpz_init_set_si: postcondition got status unknown
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <-main.
- Called from PROJECT_FILE:83.
+ Called from PROJECT_FILE:129.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:84.
-PROJECT_FILE:84:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:130.
+PROJECT_FILE:130:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:85.
+ Called from PROJECT_FILE:131.
[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:86.
-PROJECT_FILE:86:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:132.
+PROJECT_FILE:132:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:86.
+ Called from PROJECT_FILE:132.
[value] Done for function mpz_clear
-PROJECT_FILE:89:[value] Assertion got status valid.
+PROJECT_FILE:135:[value] Assertion got status valid.
[value] computing for function mpz_init_set_str <-main.
- Called from PROJECT_FILE:91.
-PROJECT_FILE:91:[value] Function mpz_init_set_str: postcondition got status unknown
+ Called from PROJECT_FILE:137.
+PROJECT_FILE:137:[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:92.
-PROJECT_FILE:92:[value] Function mpz_init_set_str: postcondition got status unknown
+ Called from PROJECT_FILE:138.
+PROJECT_FILE:138:[value] Function mpz_init_set_str: postcondition got status unknown
[value] Done for function mpz_init_set_str
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:93.
-PROJECT_FILE:93:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:139.
+PROJECT_FILE:139:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:95.
+ Called from PROJECT_FILE:141.
[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
+ Called from PROJECT_FILE:115.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:96.
-PROJECT_FILE:96:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:142.
+PROJECT_FILE:142:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:96.
+ Called from PROJECT_FILE:142.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
@@ -102,7 +102,7 @@ PROJECT_FILE:96:[value] Function mpz_clear: precondition got status valid
[from] Done for function eprintf
[from] Computing for function exit <-e_acsl_fail
[from] Done for function exit
-PROJECT_FILE:69:[from] Non terminating function (no dependencies)
+PROJECT_FILE:115:[from] Non terminating function (no dependencies)
[from] Done for function e_acsl_fail
[from] Computing for function mpz_clear
[from] Done for function mpz_clear
@@ -122,9 +122,6 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct mpz_t[1];
-/*@ requires \valid(x);
- assigns *x; */
-extern void mpz_clear(__mpz_struct * /*[1]*/ x ) ;
/*@ ensures \valid(\at(z,Old));
assigns *z; */
extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
@@ -132,6 +129,9 @@ extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
assigns *z; */
extern void mpz_init_set_str(__mpz_struct * /*[1]*/ z , char *str ,
int base ) ;
+/*@ requires \valid(x);
+ assigns *x; */
+extern void mpz_clear(__mpz_struct * /*[1]*/ x ) ;
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
index f4443a2fb6496db7796ac52e0a2f7325aa7b7a04..9e043b60b5c43c027eec05e44f737ed09f09e34c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
@@ -2,7 +2,7 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE:75:[value] Assertion got status valid.
+PROJECT_FILE:121:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[dominators] computing for function main
@@ -29,10 +29,10 @@ void main(void)
int x ;
x = 0;
/*@ assert (x ≡ 0); */ ;
- if ((long )x != 0L) { e_acsl_fail((char *)"((x == 0))"); }
+ if (x != 0) { e_acsl_fail((char *)"((x == 0))"); }
if (x) {
/*@ assert (x ≢ 0); */ ;
- if ((long )x == 0L) { e_acsl_fail((char *)"((x != 0))"); }
+ if (x == 0) { e_acsl_fail((char *)"((x != 0))"); }
}
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
index 682d6aca84d3478901c3008451fc904ded2e8825..c3a7282e5f759530aa0d110c21be154f1e7c2209 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
@@ -2,8 +2,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE:75:[value] Assertion got status valid.
-PROJECT_FILE:78:[value] Assertion got status valid.
+PROJECT_FILE:121:[value] Assertion got status valid.
+PROJECT_FILE:124:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[dominators] computing for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle
index f0fe2baaa6f816aead3f5c113eed3411dd945009..52f8aa2955b5579a727f30002f65b45e88ecc5cc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle
@@ -2,7 +2,7 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE:73:[value] Assertion got status valid.
+PROJECT_FILE:119:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[dominators] computing for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
index 1e01748f690a73760618a97879de4435aad48f8f..a5a7703d2f488a0a9d11adcf58309831e3839441 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
@@ -2,7 +2,7 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE:75:[value] Assertion got status valid.
+PROJECT_FILE:121:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[dominators] computing for function main
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 306492bd15eb30268f75cad3cf2779d0e715aba8..ab246dd079b16b2f8b20c8614dfc131c00363ea8 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -68,9 +68,10 @@ module Mpz : sig
val t: typ (* type "mpz_t" *)
val is_now_referenced: unit -> unit (* one variable "mpz_t" now exists *)
val is_t: typ -> bool (* is the type equal to "mpz_t"? *)
- val init: varinfo -> stmt (* build stmt "mpz_init(v)" *)
- val clear: varinfo -> stmt (* build stmt "mpz_clear(v)" *)
- val init_set: varinfo -> exp -> stmt
+ val e_got_t: exp -> bool (* is the type of e is equal to "mpz_t"? *)
+ val init: exp -> stmt (* build stmt "mpz_init(v)" *)
+ val clear: exp -> stmt (* build stmt "mpz_clear(v)" *)
+ val init_set: exp -> exp -> stmt
(* build stmt "mpz_init_set_*(v, e)" with the good function 'set' according to
the type of e *)
end = struct
@@ -85,8 +86,9 @@ end = struct
let t = TNamed(t_torig, [])
let is_t ty = Cil_datatype.Typ.equal ty t
+ let e_got_t e = is_t (typeOf e)
- let apply_on_var funname v = mk_call ("mpz_" ^ funname) [ new_lval v ]
+ let apply_on_var funname e = mk_call ("mpz_" ^ funname) [ e ]
let init = apply_on_var "init"
let clear = apply_on_var "clear"
@@ -102,7 +104,7 @@ end = struct
[ e; integer ~loc:unknown_loc 10 ]
| _ -> assert false
in
- mk_call ("mpz_init_set_" ^ fname) (new_lval v :: args)
+ mk_call ("mpz_init_set_" ^ fname) (v :: args)
end
@@ -111,8 +113,9 @@ end
(* ************************************************************************** *)
module New_vars: sig
- val push: typ -> (varinfo -> stmt list) -> varinfo
- val finalize: unit -> (varinfo * stmt list * bool) list
+ val push: typ -> (varinfo -> exp (* the var as exp *) -> stmt) -> exp
+ val push_and_mpz_init: (varinfo -> exp (* the var as exp *) -> stmt) -> exp
+ val finalize: unit -> (varinfo * exp * stmt list * bool) list
end = struct
(* the finalizer resets the counter in order to keep it small. However, Cil
@@ -125,7 +128,7 @@ end = struct
let var_cpt = ref 0
let vlist = ref []
- let push ty mk_stmts =
+ let push_list ty mk_stmts =
incr var_cpt;
let is_t = Mpz.is_t ty in
if is_t then Mpz.is_now_referenced ();
@@ -138,8 +141,14 @@ end = struct
("e_acsl_cst_" ^ string_of_int !var_cpt)
ty
in
- vlist := (v, mk_stmts v, is_t) :: !vlist;
- v
+ let e = new_lval v in
+ vlist := (v, e, mk_stmts v e, is_t) :: !vlist;
+ e
+
+ let push ty mk_stmt = push_list ty (fun v e -> [ mk_stmt v e ])
+
+ let push_and_mpz_init mk_stmt =
+ push_list Mpz.t (fun v e -> [ Mpz.init e; mk_stmt v e ])
let finalize () =
var_cpt := 0;
@@ -180,9 +189,9 @@ let constant_to_exp = function
| CInt64(n, k, s) ->
(match k with
| IBool | IChar | IUChar | IUInt | IUShort | IULong ->
- kinteger64_repr ~loc:unknown_loc IULong n s
+ kinteger64_repr ~loc:unknown_loc k n s
| ISChar | IShort | IInt | ILong ->
- kinteger64_repr ~loc:unknown_loc ILong n s
+ kinteger64_repr ~loc:unknown_loc k n s
| ILongLong | IULongLong ->
mkString ~loc:unknown_loc (Int64.to_string n))
| CStr _ as c -> new_exp unknown_loc (Const c)
@@ -195,13 +204,28 @@ let tlval_to_lval = function
| TVar { lv_origin = Some v }, TNoOffset -> Var v, NoOffset
| _ -> not_yet "complex left value"
+let relation_to_revbinop = function
+ | Rlt -> Ge
+ | Rgt -> Le
+ | Rle -> Gt
+ | Rge -> Lt
+ | Req -> Ne
+ | Rneq -> Eq
+
+let name_of_mpz_arith_bop = function
+ | PlusA -> "mpz_add"
+ | MinusA -> "mpz_sub"
+ | Mult -> "mpz_mul"
+ | Div -> "mpz_cdiv_q"
+ | Mod -> "mpz_mod"
+ | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
+ | Shiftlt | Shiftrt | PlusPI | IndexPI | MinusPI | MinusPP -> assert false
+
let wrap_leaf e = function
| Ctype _ -> e
| Ltype _ -> not_yet "term from an user defined type"
| Lvar _ -> not_yet "polymorphic term"
- | Linteger ->
- let v = New_vars.push Mpz.t (fun v -> [ Mpz.init_set v e ]) in
- new_lval v
+ | Linteger -> New_vars.push Mpz.t (fun _ v -> Mpz.init_set v e)
| Lreal -> not_yet "real number"
| Larrow _ -> not_yet "logic function"
@@ -218,8 +242,45 @@ let rec term_to_exp t = match t.term_node with
| TAlignOfE t ->
let e = term_to_exp t in
new_exp ~loc:unknown_loc (AlignOfE e)
- | TUnOp _ -> not_yet "unary operator"
- | TBinOp _ -> not_yet "binary operator"
+ | TUnOp(Neg | BNot as op, t) ->
+ let e = term_to_exp t in
+ assert (Mpz.e_got_t e);
+ let name = match op with
+ | Neg -> "mpz_neg"
+ | BNot -> "mpz_com"
+ | LNot -> assert false
+ in
+ New_vars.push_and_mpz_init (fun _ ev -> mk_call name [ ev; e ])
+ | TUnOp(LNot, t) ->
+ let e = term_to_exp t in
+ let ty = typeOf e in
+ assert (not (Mpz.is_t ty));
+ new_exp ~loc:unknown_loc (UnOp(LNot, e, ty))
+ | TBinOp(PlusA | MinusA | Mult | Div | Mod as bop, t1, t2) ->
+ (* arithmetic binary operator *)
+ let e1 = term_to_exp t1 in
+ let e2 = term_to_exp t2 in
+ assert (Cil_datatype.Typ.equal (typeOf e1) (typeOf e2));
+ let name = name_of_mpz_arith_bop bop in
+ New_vars.push_and_mpz_init (fun _ e -> mk_call name [ e; e1; e2 ])
+ | TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
+ (* comparison operators *)
+ (* [TODO] don't work; see code comment in arith.i *)
+ comparison_to_exp bop t1 t2
+ | TBinOp((LOr | LAnd | BOr | BXor | BAnd), _, _) ->
+ (* left/right shift *)
+ not_yet "missing binary operator"
+ | TBinOp((Shiftlt | Shiftrt), _, _) ->
+ (* left/right shift *)
+ not_yet "left/right shift"
+ | TBinOp(PlusPI | IndexPI | MinusPI | MinusPP as bop, t1, t2) ->
+ (* binary operation over pointers *)
+ (* [TODO] untested *)
+ let e1 = term_to_exp t1 in
+ let e2 = term_to_exp t2 in
+ (* the type of the result is the same than type of the pointer [e1],
+ whatever is [e2] *)
+ new_exp ~loc:unknown_loc (BinOp(bop, e1, e2, typeOf e1))
| TCastE(ty, t) ->
let e = term_to_exp t in
mkCast e ty
@@ -246,13 +307,20 @@ let rec term_to_exp t = match t.term_node with
| Trange _ -> not_yet "range"
| Tlet _ -> not_yet "let binding"
-let relation_to_revbinop = function
- | Rlt -> Ge
- | Rgt -> Le
- | Rle -> Gt
- | Rge -> Lt
- | Req -> Ne
- | Rneq -> Eq
+and comparison_to_exp bop t1 t2 =
+ let e1 = term_to_exp t1 in
+ let e2 = term_to_exp t2 in
+(* Options.feedback "ty1=%a; ty2=%a" d_type (typeOf e1) d_type (typeOf e2);*)
+ assert (Cil_datatype.Typ.equal (typeOf e1) (typeOf e2));
+ if Mpz.e_got_t e1 then
+ let e =
+ New_vars.push
+ intType
+ (fun v _ -> mk_call ~result:(var v) "mpz_cmp" [ e1; e2 ])
+ in
+ new_exp unknown_loc (BinOp(bop, e, zero unknown_loc, intType))
+ else
+ new_exp unknown_loc (BinOp(bop, e1, e2, intType))
(* convert an ACSL named predicate into the opposite C expression (if any).
E.g. \true is converted into 0. *)
@@ -261,28 +329,7 @@ let rec named_predicate_to_revexp p = match p.content with
| Ptrue -> zero ~loc:unknown_loc
| Papp _ -> not_yet "logic function application"
| Pseparated _ -> not_yet "separated"
- | Prel(rel, t1, t2) ->
- let bop = relation_to_revbinop rel in
- let e1 = term_to_exp t1 in
- let e2 = term_to_exp t2 in
- if Mpz.is_t (typeOf e1) then begin
- assert (Mpz.is_t (typeOf e2));
- let v =
- New_vars.push
- intType
- (fun v ->
- let result = var v in
- [ mk_call ~result "mpz_cmp" [ e1; e2 ] ])
- in
- let bop =
- BinOp(bop,
- new_exp unknown_loc (Lval (var v)),
- zero unknown_loc,
- intType)
- in
- new_exp unknown_loc bop
- end else
- new_exp unknown_loc (BinOp(bop, e1, e2, intType))
+ | Prel(rel, t1, t2) -> comparison_to_exp (relation_to_revbinop rel) t1 t2
| Pand _ -> not_yet "&&"
| Por _ -> not_yet "||"
| Pxor _ -> not_yet "xor"
@@ -374,10 +421,10 @@ class e_acsl_visitor prj generate = object
let b = New_block.finalize stmt in
let vars, clears =
List.fold_left
- (fun (vars, clears) (v, stmts, must_clear) ->
+ (fun (vars, clears) (v, e, stmts, must_clear) ->
b.blocals <- v :: b.blocals;
b.bstmts <- stmts @ b.bstmts;
- v :: vars, if must_clear then Mpz.clear v :: clears else clears)
+ v :: vars, if must_clear then Mpz.clear e :: clears else clears)
([], [])
new_vars
in