From 495b41f040ae6e5c3fafcdcbccd7dbb716bd9ee5 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 18 Jun 2013 13:33:03 +0000
Subject: [PATCH] [E-ACSL] fix bug when computing RTEs on the EACSL's resulting
project
---
src/plugins/e-acsl/TODO | 2 ++
src/plugins/e-acsl/doc/Changelog | 2 ++
src/plugins/e-acsl/main.ml | 7 +++++++
.../e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle | 6 ++++++
.../tests/e-acsl-runtime/oracle/bts1307.1.res.oracle | 2 +-
.../tests/e-acsl-runtime/oracle/bts1326.1.res.oracle | 2 +-
.../tests/e-acsl-runtime/oracle/bts1390.1.res.oracle | 4 ++--
.../e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle | 4 ++--
.../e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle | 6 +++---
.../tests/e-acsl-runtime/oracle/longlong.1.res.oracle | 1 +
.../e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle | 1 +
.../e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle | 2 +-
.../tests/e-acsl-runtime/oracle/quantif.1.res.oracle | 4 ++--
16 files changed, 34 insertions(+), 15 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 4c64d0ff83c..7e86494adaa 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 9c90716ad2c..acf13d03492 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 59f56e3a464..0250febfdbe 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 7f4fcbe182c..cc8dae96e8f 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 096cbbcc5c7..b18ecd12040 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 708749f3f6d..09ec28c4218 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 95104abb06b..95b2d0a49d8 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 d61356dd1ce..7fbf952e57a 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 aa490e4d810..2ae61370575 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 73315d42186..29c1658932c 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 73315d42186..29c1658932c 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 1b5541e3558..f41fe7e4fa6 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 2f5824a0c5e..c4c432cd8c3 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 2f5824a0c5e..c4c432cd8c3 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 5e58a22ae00..5bbb4ab925f 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 f86925f3348..c7bcb94f30e 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.
--
GitLab