[E-ACSL] fix bug when computing RTEs on the EACSL's resulting project

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 #

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.
 
 ###################################

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)
 	      ()

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:

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.

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

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.)

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.)

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

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 ;

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 ;

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.

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

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

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.

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.