diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 4c64d0ff83c9dff012e99434a467602710d21650..7e86494adaa0b67571a02a0025b4eaf782648974 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -42,6 +42,8 @@
- RTE: potential duplication (e.g. with **p)
- default output of e_acsl_assert in the format of standart error messages
- some calls to __eacsl_memory_debug are missing in debug mode
+- translate only once the assumes clause in presence of a pre- and a
+ post-condition
##############
# KNOWN BUGS #
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 9c90716ad2c6ab6b7483f6f6e7b737ef81bffe52..acf13d03492d005669c9ee1afd15a7b2637e2cfb 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2013/06/18] Fixed bug when generating RTEs on the E-ACSL
+ generated project.
-* E-ACSL [2013/05/30] Fixed -e-acsl-debug n, with n >= 2.
###################################
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index 59f56e3a464c994fc8e0095618b1676c5a5cda71..0250febfdbef6b89b8dad46bee50e635ca1a27ee 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -139,6 +139,13 @@ let generate_code =
Pre_analysis.reset ();
let visit prj = Visit.do_visit ~prj true in
let prj = File.create_project_from_visitor name visit in
+ (* remove the RTE's results computed from E-ACSL: their are
+ partial and associated with the wrong kernel function (the
+ one of the old project). *)
+ Project.clear
+ ~selection:(State_selection.with_dependencies !Db.RteGen.self)
+ ~project:prj
+ ();
Resulting_projects.mark_as_computed ();
prj)
()
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
index 7f4fcbe182cf91f9865aea1a77d3c199e5ed993f..cc8dae96e8fe75088542cd5a9c1c73a0772d5546 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
@@ -53,6 +53,7 @@ share/e-acsl/e_acsl_gmp.h:154:[value] Function __gmpz_mul: precondition got stat
share/e-acsl/e_acsl_gmp.h:155:[value] Function __gmpz_mul: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:156:[value] Function __gmpz_mul: precondition got status valid.
tests/e-acsl-runtime/arith.i:19:[value] Assertion got status valid.
+tests/e-acsl-runtime/arith.i:19:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function __gmpz_tdiv_q
share/e-acsl/e_acsl_gmp.h:161:[value] Function __gmpz_tdiv_q: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:162:[value] Function __gmpz_tdiv_q: precondition got status valid.
@@ -62,13 +63,17 @@ tests/e-acsl-runtime/arith.i:20:[value] Assertion got status valid.
share/e-acsl/e_acsl_gmp.h:71:[value] Function __gmpz_init_set_str: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: postcondition got status valid.
share/e-acsl/e_acsl_gmp.h:74:[value] Function __gmpz_init_set_str: postcondition got status unknown.
+tests/e-acsl-runtime/arith.i:20:[value] Assertion 'E_ACSL' got status valid.
tests/e-acsl-runtime/arith.i:21:[value] Assertion got status valid.
+tests/e-acsl-runtime/arith.i:21:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function __gmpz_tdiv_r
share/e-acsl/e_acsl_gmp.h:168:[value] Function __gmpz_tdiv_r: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:169:[value] Function __gmpz_tdiv_r: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:170:[value] Function __gmpz_tdiv_r: precondition got status valid.
tests/e-acsl-runtime/arith.i:22:[value] Assertion got status valid.
+tests/e-acsl-runtime/arith.i:22:[value] Assertion 'E_ACSL' got status valid.
tests/e-acsl-runtime/arith.i:23:[value] Assertion got status valid.
+tests/e-acsl-runtime/arith.i:23:[value] Assertion 'E_ACSL' got status valid.
tests/e-acsl-runtime/arith.i:25:[value] Assertion got status valid.
tests/e-acsl-runtime/arith.i:27:[value] Assertion got status valid.
tests/e-acsl-runtime/arith.i:28:[value] Assertion got status valid.
@@ -76,6 +81,7 @@ tests/e-acsl-runtime/arith.i:29:[value] Assertion got status valid.
tests/e-acsl-runtime/arith.i:30:[value] Assertion got status valid.
tests/e-acsl-runtime/arith.i:32:[value] Assertion got status valid.
tests/e-acsl-runtime/arith.i:33:[value] Assertion got status valid.
+tests/e-acsl-runtime/arith.i:33:[value] Assertion 'E_ACSL' got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
index 096cbbcc5c7392132a76ba13f8d4e5c0ecfd8f59..b18ecd1204077b486abd8a4bd6f891e64f10715d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
@@ -43,7 +43,7 @@ share/e-acsl/e_acsl_gmp.h:125:[value] Function __gmpz_cmp: precondition got stat
[value] using specification for function __gmpz_init
share/e-acsl/e_acsl_gmp.h:37:[value] Function __gmpz_init: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:38:[value] Function __gmpz_init: postcondition got status valid.
-tests/e-acsl-runtime/bts1307.i:13:[value] Assertion got status valid.
+tests/e-acsl-runtime/bts1307.i:13:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function __gmpz_tdiv_q
share/e-acsl/e_acsl_gmp.h:161:[value] Function __gmpz_tdiv_q: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:162:[value] Function __gmpz_tdiv_q: precondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
index 708749f3f6da0f101fad85acefe558b34b9bbf6a..09ec28c4218d0d341b5b7291ea54ac3026fb2ec2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
@@ -32,7 +32,7 @@ share/e-acsl/e_acsl_gmp.h:142:[value] Function __gmpz_add: precondition got stat
[value] using specification for function __gmpz_cmp
share/e-acsl/e_acsl_gmp.h:124:[value] Function __gmpz_cmp: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:125:[value] Function __gmpz_cmp: precondition got status valid.
-tests/e-acsl-runtime/bts1326.i:11:[value] Assertion got status valid.
+tests/e-acsl-runtime/bts1326.i:11:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_q
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
index 95104abb06b04082946c3278976af5a54e9ccae7..95b2d0a49d8c1c78f46767ad43608ca07790e69b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
@@ -24,12 +24,12 @@
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/bts1390.c:20:[value] entering loop for the first time
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/bts1390.c:13:[value] entering loop for the first time
[value] using specification for function __offset
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
index d61356dd1cec63e994082282527ed56f1a8a53df..7fbf952e57a40065010c8d89d213aa0a8247ab6b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
@@ -51,14 +51,14 @@ share/e-acsl/e_acsl_gmp.h:142:[value] Function __gmpz_add: precondition got stat
tests/e-acsl-runtime/bts1390.c:11:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_i_2);
tests/e-acsl-runtime/bts1390.c:20:[value] entering loop for the first time
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/bts1390.c:13:[value] entering loop for the first time
[value] using specification for function __offset
tests/e-acsl-runtime/bts1390.c:13:[kernel] warning: out of bounds read. assert \valid_read((char *)__e_acsl_at_2+__e_acsl_j_2);
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
index aa490e4d81067549b58c9be9ef298b02995081ad..2ae61370575a804ec92a4b34001934ab76fa7aac 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
@@ -48,7 +48,7 @@ share/e-acsl/e_acsl_gmp.h:125:[value] Function __gmpz_cmp: precondition got stat
[value] using specification for function __gmpz_init
share/e-acsl/e_acsl_gmp.h:37:[value] Function __gmpz_init: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:38:[value] Function __gmpz_init: postcondition got status valid.
-tests/e-acsl-runtime/bts1399.c:24:[value] Assertion got status valid.
+tests/e-acsl-runtime/bts1399.c:24:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_q
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
index 73315d4218615f33c0d4d7a88fe7de0fd2a51f3a..29c1658932c34126045d6f0d32bad0bf0a018115 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
@@ -16,7 +16,7 @@ typedef unsigned int blksize_t;
typedef unsigned int dev_t;
typedef unsigned int mode_t;
typedef unsigned int nlink_t;
-typedef unsigned int off_t;
+typedef long off_t;
struct stat {
dev_t st_dev ;
ino_t st_ino ;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
index 73315d4218615f33c0d4d7a88fe7de0fd2a51f3a..29c1658932c34126045d6f0d32bad0bf0a018115 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
@@ -16,7 +16,7 @@ typedef unsigned int blksize_t;
typedef unsigned int dev_t;
typedef unsigned int mode_t;
typedef unsigned int nlink_t;
-typedef unsigned int off_t;
+typedef long off_t;
struct stat {
dev_t st_dev ;
ino_t st_ino ;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
index 1b5541e3558db4d29690a8647310750365310aa8..f41fe7e4fa6f509ac0de65d02a6b3127e9ba8858 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
@@ -30,14 +30,14 @@ tests/e-acsl-runtime/lazy.i:12:[value] Assertion got status valid.
[value] using specification for function __gmpz_init
share/e-acsl/e_acsl_gmp.h:37:[value] Function __gmpz_init: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:38:[value] Function __gmpz_init: postcondition got status valid.
-tests/e-acsl-runtime/lazy.i:12:[value] Assertion got status invalid (stopping propagation).
+tests/e-acsl-runtime/lazy.i:12:[value] Assertion 'E_ACSL' got status invalid (stopping propagation).
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/lazy.i:13:[value] Assertion got status valid.
tests/e-acsl-runtime/lazy.i:14:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:14:[value] Assertion got status invalid (stopping propagation).
+tests/e-acsl-runtime/lazy.i:14:[value] Assertion 'E_ACSL' got status invalid (stopping propagation).
tests/e-acsl-runtime/lazy.i:15:[value] Assertion got status valid.
tests/e-acsl-runtime/lazy.i:16:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:16:[value] Assertion got status invalid (stopping propagation).
+tests/e-acsl-runtime/lazy.i:16:[value] Assertion 'E_ACSL' got status invalid (stopping propagation).
tests/e-acsl-runtime/lazy.i:17:[value] Assertion got status unknown.
tests/e-acsl-runtime/lazy.i:18:[value] Assertion got status unknown.
tests/e-acsl-runtime/lazy.i:19:[value] Assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
index 2f5824a0c5ed81e5709f12aa4fb3f4c211f12bc2..c4c432cd8c35b71dc3a3020af76e3ea0df29faf0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
@@ -44,6 +44,7 @@ share/e-acsl/e_acsl_gmp.h:142:[value] Function __gmpz_add: precondition got stat
[value] using specification for function __gmpz_cmp
share/e-acsl/e_acsl_gmp.h:124:[value] Function __gmpz_cmp: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:125:[value] Function __gmpz_cmp: precondition got status valid.
+tests/e-acsl-runtime/longlong.i:19:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_r
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle
index 2f5824a0c5ed81e5709f12aa4fb3f4c211f12bc2..c4c432cd8c35b71dc3a3020af76e3ea0df29faf0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle
@@ -44,6 +44,7 @@ share/e-acsl/e_acsl_gmp.h:142:[value] Function __gmpz_add: precondition got stat
[value] using specification for function __gmpz_cmp
share/e-acsl/e_acsl_gmp.h:124:[value] Function __gmpz_cmp: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:125:[value] Function __gmpz_cmp: precondition got status valid.
+tests/e-acsl-runtime/longlong.i:19:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_r
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
index 5e58a22ae00361fe75616a54e3ac4dbe66277d97..5bbb4ab925f9fdea6119fe3e916273e68aa10be0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
@@ -41,7 +41,7 @@ share/e-acsl/e_acsl_gmp.h:38:[value] Function __gmpz_init: postcondition got sta
share/e-acsl/e_acsl_gmp.h:154:[value] Function __gmpz_mul: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:155:[value] Function __gmpz_mul: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:156:[value] Function __gmpz_mul: precondition got status valid.
-tests/e-acsl-runtime/ptr.i:16:[value] Assertion got status valid.
+tests/e-acsl-runtime/ptr.i:16:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function __gmpz_tdiv_q
share/e-acsl/e_acsl_gmp.h:161:[value] Function __gmpz_tdiv_q: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:162:[value] Function __gmpz_tdiv_q: precondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
index f86925f33485d12198c4edcd0d8067681d4a0011..c7bcb94f30ed4660c0c03021bc2d5672d6952f4c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
@@ -49,13 +49,13 @@ tests/e-acsl-runtime/quantif.i:23:[value] Assertion got status unknown.
tests/e-acsl-runtime/quantif.i:23:[value] entering loop for the first time
tests/e-acsl-runtime/quantif.i:27:[value] Assertion got status unknown.
tests/e-acsl-runtime/quantif.i:27:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:28:[value] Assertion got status valid.
+tests/e-acsl-runtime/quantif.i:28:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function __gmpz_tdiv_r
share/e-acsl/e_acsl_gmp.h:168:[value] Function __gmpz_tdiv_r: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:169:[value] Function __gmpz_tdiv_r: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:170:[value] Function __gmpz_tdiv_r: precondition got status valid.
tests/e-acsl-runtime/quantif.i:28:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:28:[value] Assertion got status valid.
+tests/e-acsl-runtime/quantif.i:28:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function __gmpz_tdiv_q
share/e-acsl/e_acsl_gmp.h:161:[value] Function __gmpz_tdiv_q: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:162:[value] Function __gmpz_tdiv_q: precondition got status valid.