diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 701aab53a56219c06906d4010a9195ecd00ca388..ccec0b43e6f6b4b8f9239cced908d73144d203fd 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -4,6 +4,7 @@
see http://gmplib.org/manual-4.3.2/Simultaneous-Integer-Init-_0026-Assign.html#Simultaneous-Integer-Init-_0026-Assign
- améliorer test "comparison.i" quand bug fixed #744
+- remettre test "cast.i" quand bug fixed #744
- améliorer test "integer_constant.i" quand bug fixed #745
en lien avec bts #743:
diff --git a/src/plugins/e-acsl/share/e_acsl.h b/src/plugins/e-acsl/share/e_acsl.h
index 67ccc54b8fe7d803c00e6451c10e03264461ea7f..9969d4680907e05ea66da5e8601bea9608b2a8ac 100644
--- a/src/plugins/e-acsl/share/e_acsl.h
+++ b/src/plugins/e-acsl/share/e_acsl.h
@@ -32,17 +32,17 @@ extern void mpz_init(mpz_t x);
@ assigns *x; */
extern void mpz_clear(mpz_t x);
-/*@ requires \valid(z);
+/*@ ensures \valid(z);
@ assigns *z; */
-extern void mpz_set_ui(mpz_t z, unsigned long int n);
+extern void mpz_init_set_ui(mpz_t z, unsigned long int n);
-/*@ requires \valid(z);
+/*@ ensures \valid(z);
@ assigns *z; */
-extern void mpz_set_si(mpz_t z, signed long int n);
+extern void mpz_init_set_si(mpz_t z, signed long int n);
-/*@ requires \valid(z);
+/*@ ensures \valid(z);
@ assigns *z; */
-extern void mpz_set_str(mpz_t z, char *str, int base);
+extern void mpz_init_set_str(mpz_t z, char *str, int base);
/*@ requires \valid(z1);
@ requires \valid(z2);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i b/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
index 5e70f717119a0db6db67c43c51577dda49024563..08e0908839626e224806fc6e320d924a0b5cc891 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
@@ -1,8 +1,11 @@
/* run.config
- COMMENT: cast */
+ DONTRUN:
+ COMMENT: cast
+ COMMENT: waiting for fixing bts #744 */
void main() {
long x = 0;
int y = 0;
/*@ assert (int)x == y; */ ;
+ /*@ assert x == (long)y; */ ;
}
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 5dcf0a3d4a3048328c908a4101ce850b40e7922c..2d2ef36e82c14605bf8bc8ab4e9ee5b6ee7da2cc 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
@@ -3,28 +3,19 @@
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE:78:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
+[value] computing for function mpz_init_set_si <-main.
Called from PROJECT_FILE:80.
-PROJECT_FILE:80:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
+PROJECT_FILE:80:[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.
-PROJECT_FILE:80:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:81.
-PROJECT_FILE:81:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:81.
-PROJECT_FILE:81:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
+[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:82.
-PROJECT_FILE:82:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:81.
+PROJECT_FILE:81:[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:83.
+ Called from PROJECT_FILE:82.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -35,35 +26,26 @@ PROJECT_FILE:69:[value] Function exit: postcondition got status invalid
[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:84.
-PROJECT_FILE:84:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:83.
+PROJECT_FILE:83:[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:84.
+ Called from PROJECT_FILE:83.
[value] Done for function mpz_clear
-PROJECT_FILE:87:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:89.
-PROJECT_FILE:89:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:89.
-PROJECT_FILE:89:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:90.
-PROJECT_FILE:90:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:90.
-PROJECT_FILE:90:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
+PROJECT_FILE:86:[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
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:88.
+[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:91.
-PROJECT_FILE:91:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:89.
+PROJECT_FILE:89:[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:92.
+ Called from PROJECT_FILE:90.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -73,35 +55,26 @@ PROJECT_FILE:91:[value] Function mpz_cmp: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:93.
-PROJECT_FILE:93:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:91.
+PROJECT_FILE:91:[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:93.
+ Called from PROJECT_FILE:91.
[value] Done for function mpz_clear
-PROJECT_FILE:96:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:98.
-PROJECT_FILE:98:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:98.
-PROJECT_FILE:98:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:99.
-PROJECT_FILE:99:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:99.
-PROJECT_FILE:99:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
+PROJECT_FILE:94:[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
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:96.
+[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:100.
-PROJECT_FILE:100:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:97.
+PROJECT_FILE:97:[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:101.
+ Called from PROJECT_FILE:98.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -111,35 +84,26 @@ PROJECT_FILE:100:[value] Function mpz_cmp: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:102.
-PROJECT_FILE:102:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:99.
+PROJECT_FILE:99:[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:102.
+ Called from PROJECT_FILE:99.
[value] Done for function mpz_clear
-PROJECT_FILE:105:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:107.
-PROJECT_FILE:107:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:107.
-PROJECT_FILE:107:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:108.
-PROJECT_FILE:108:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:108.
-PROJECT_FILE:108:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
+PROJECT_FILE:102:[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
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:104.
+[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:109.
-PROJECT_FILE:109:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:105.
+PROJECT_FILE:105:[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:110.
+ Called from PROJECT_FILE:106.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -149,37 +113,28 @@ PROJECT_FILE:109:[value] Function mpz_cmp: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:111.
-PROJECT_FILE:111:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:107.
+PROJECT_FILE:107:[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:111.
+ Called from PROJECT_FILE:107.
[value] Done for function mpz_clear
-PROJECT_FILE:115:[value] Assertion got status valid.
-PROJECT_FILE:118:[value] Assertion got status valid.
-PROJECT_FILE:121:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:123.
-PROJECT_FILE:123:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:123.
-PROJECT_FILE:123:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:124.
-PROJECT_FILE:124:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:124.
-PROJECT_FILE:124:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
+PROJECT_FILE:111:[value] Assertion got status valid.
+PROJECT_FILE:114:[value] Assertion got status valid.
+PROJECT_FILE:117:[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
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:119.
+[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:125.
-PROJECT_FILE:125:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:120.
+PROJECT_FILE:120:[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:126.
+ Called from PROJECT_FILE:121.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -189,35 +144,26 @@ PROJECT_FILE:125:[value] Function mpz_cmp: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:127.
-PROJECT_FILE:127:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:122.
+PROJECT_FILE:122:[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:127.
+ Called from PROJECT_FILE:122.
[value] Done for function mpz_clear
-PROJECT_FILE:130:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:132.
-PROJECT_FILE:132:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:132.
-PROJECT_FILE:132:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:133.
-PROJECT_FILE:133:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:133.
-PROJECT_FILE:133:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
+PROJECT_FILE:125:[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
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:127.
+[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:134.
-PROJECT_FILE:134:[value] Function mpz_cmp: precondition got status valid
+ 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:135.
+ Called from PROJECT_FILE:129.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -227,35 +173,26 @@ PROJECT_FILE:134:[value] Function mpz_cmp: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:136.
-PROJECT_FILE:136:[value] Function mpz_clear: precondition got status valid
+ 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:136.
+ Called from PROJECT_FILE:130.
[value] Done for function mpz_clear
-PROJECT_FILE:139:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:141.
-PROJECT_FILE:141:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:141.
-PROJECT_FILE:141:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:142.
-PROJECT_FILE:142:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:142.
-PROJECT_FILE:142:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
+PROJECT_FILE:133:[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
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:135.
+[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:143.
-PROJECT_FILE:143:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:136.
+PROJECT_FILE:136:[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:144.
+ Called from PROJECT_FILE:137.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -265,35 +202,26 @@ PROJECT_FILE:143:[value] Function mpz_cmp: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:145.
-PROJECT_FILE:145:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:138.
+PROJECT_FILE:138:[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:145.
+ Called from PROJECT_FILE:138.
[value] Done for function mpz_clear
-PROJECT_FILE:148:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:150.
-PROJECT_FILE:150:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:150.
-PROJECT_FILE:150:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:151.
-PROJECT_FILE:151:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:151.
-PROJECT_FILE:151:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
+PROJECT_FILE:141:[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
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:143.
+[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:144.
+PROJECT_FILE:144:[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:145.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -303,35 +231,26 @@ PROJECT_FILE:152:[value] Function mpz_cmp: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:154.
-PROJECT_FILE:154:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:146.
+PROJECT_FILE:146:[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:146.
[value] Done for function mpz_clear
-PROJECT_FILE:157:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:159.
-PROJECT_FILE:159:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:159.
-PROJECT_FILE:159:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_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_set_si <-main.
- Called from PROJECT_FILE:160.
-PROJECT_FILE:160:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
+PROJECT_FILE:149:[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
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:151.
+[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:161.
-PROJECT_FILE:161:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:152.
+PROJECT_FILE:152:[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:162.
+ Called from PROJECT_FILE:153.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -341,35 +260,26 @@ PROJECT_FILE:161:[value] Function mpz_cmp: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:163.
-PROJECT_FILE:163:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:154.
+PROJECT_FILE:154:[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:163.
+ Called from PROJECT_FILE:154.
[value] Done for function mpz_clear
-PROJECT_FILE:166:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:168.
-PROJECT_FILE:168:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:168.
-PROJECT_FILE:168:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:169.
-PROJECT_FILE:169:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:169.
-PROJECT_FILE:169:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
+PROJECT_FILE:157:[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_cmp <-main.
- Called from PROJECT_FILE:170.
-PROJECT_FILE:170:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:160.
+PROJECT_FILE:160:[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:171.
+ Called from PROJECT_FILE:161.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -379,18 +289,16 @@ PROJECT_FILE:170:[value] Function mpz_cmp: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:172.
-PROJECT_FILE:172:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:162.
+PROJECT_FILE:162:[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:172.
+ Called from PROJECT_FILE:162.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
-[from] Computing for function mpz_init
-[from] Done for function mpz_init
-[from] Computing for function mpz_set_si
-[from] Done for function mpz_set_si
+[from] Computing for function mpz_init_set_si
+[from] Done for function mpz_init_set_si
[from] Computing for function mpz_cmp
[from] Done for function mpz_cmp
[from] Computing for function e_acsl_fail
@@ -419,15 +327,12 @@ struct __anonstruct___mpz_struct_1 {
};
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 ) ;
/*@ requires \valid(x);
assigns *x; */
extern void mpz_clear(__mpz_struct * /*[1]*/ x ) ;
-/*@ requires \valid(z);
+/*@ ensures \valid(\at(z,Old));
assigns *z; */
-extern void mpz_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
+extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
@@ -454,54 +359,46 @@ void main(void)
y = 1;
/*@ assert (x < y); */ ;
{ mpz_t e_acsl_cst_1 ; mpz_t e_acsl_cst_2 ; int e_acsl_cst_3 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_1));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_1),(long )x);
- mpz_init((__mpz_struct *)(e_acsl_cst_2));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_2),(long )y);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_1),(long )x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_2),(long )y);
e_acsl_cst_3 = mpz_cmp((__mpz_struct *)(e_acsl_cst_1),
(__mpz_struct *)(e_acsl_cst_2));
if (e_acsl_cst_3 >= 0) { e_acsl_fail((char *)"((x < y))"); }
- mpz_clear((__mpz_struct *)(e_acsl_cst_2));
mpz_clear((__mpz_struct *)(e_acsl_cst_1));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_2));
}
/*@ assert (y > x); */ ;
{ mpz_t e_acsl_cst_4 ; mpz_t e_acsl_cst_5 ; int e_acsl_cst_6 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_4));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_4),(long )y);
- mpz_init((__mpz_struct *)(e_acsl_cst_5));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_5),(long )x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_4),(long )y);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_5),(long )x);
e_acsl_cst_6 = mpz_cmp((__mpz_struct *)(e_acsl_cst_4),
(__mpz_struct *)(e_acsl_cst_5));
if (e_acsl_cst_6 <= 0) { e_acsl_fail((char *)"((y > x))"); }
- mpz_clear((__mpz_struct *)(e_acsl_cst_5));
mpz_clear((__mpz_struct *)(e_acsl_cst_4));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_5));
}
/*@ assert (x ≤ 0); */ ;
{ mpz_t e_acsl_cst_7 ; mpz_t e_acsl_cst_8 ; int e_acsl_cst_9 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_7));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_7),(long )x);
- mpz_init((__mpz_struct *)(e_acsl_cst_8));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_8),(long )0);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_7),(long )x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_8),(long )0);
e_acsl_cst_9 = mpz_cmp((__mpz_struct *)(e_acsl_cst_7),
(__mpz_struct *)(e_acsl_cst_8));
if (e_acsl_cst_9 > 0) { e_acsl_fail((char *)"((x <= 0))"); }
- mpz_clear((__mpz_struct *)(e_acsl_cst_8));
mpz_clear((__mpz_struct *)(e_acsl_cst_7));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_8));
}
/*@ assert (y ≥ 1); */ ;
{ mpz_t e_acsl_cst_10 ; mpz_t e_acsl_cst_11 ; int e_acsl_cst_12 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_10));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_10),(long )y);
- mpz_init((__mpz_struct *)(e_acsl_cst_11));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_11),(long )1);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_10),(long )y);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_11),(long )1);
e_acsl_cst_12 = mpz_cmp((__mpz_struct *)(e_acsl_cst_10),
(__mpz_struct *)(e_acsl_cst_11));
if (e_acsl_cst_12 < 0) { e_acsl_fail((char *)"((y >= 1))"); }
- mpz_clear((__mpz_struct *)(e_acsl_cst_11));
mpz_clear((__mpz_struct *)(e_acsl_cst_10));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_11));
}
s = (char *)"toto";
@@ -511,80 +408,68 @@ void main(void)
if ("toto" == "titi") { e_acsl_fail((char *)"((\"toto\" != \"titi\"))"); }
/*@ assert (5 < 18); */ ;
{ mpz_t e_acsl_cst_13 ; mpz_t e_acsl_cst_14 ; int e_acsl_cst_15 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_13));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_13),(long )5);
- mpz_init((__mpz_struct *)(e_acsl_cst_14));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_14),(long )18);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_13),(long )5);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_14),(long )18);
e_acsl_cst_15 = mpz_cmp((__mpz_struct *)(e_acsl_cst_13),
(__mpz_struct *)(e_acsl_cst_14));
if (e_acsl_cst_15 >= 0) { e_acsl_fail((char *)"((5 < 18))"); }
- mpz_clear((__mpz_struct *)(e_acsl_cst_14));
mpz_clear((__mpz_struct *)(e_acsl_cst_13));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_14));
}
/*@ assert (32 > 3); */ ;
{ mpz_t e_acsl_cst_16 ; mpz_t e_acsl_cst_17 ; int e_acsl_cst_18 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_16));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_16),(long )32);
- mpz_init((__mpz_struct *)(e_acsl_cst_17));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_17),(long )3);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_16),(long )32);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_17),(long )3);
e_acsl_cst_18 = mpz_cmp((__mpz_struct *)(e_acsl_cst_16),
(__mpz_struct *)(e_acsl_cst_17));
if (e_acsl_cst_18 <= 0) { e_acsl_fail((char *)"((32 > 3))"); }
- mpz_clear((__mpz_struct *)(e_acsl_cst_17));
mpz_clear((__mpz_struct *)(e_acsl_cst_16));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_17));
}
/*@ assert (12 ≤ 13); */ ;
{ mpz_t e_acsl_cst_19 ; mpz_t e_acsl_cst_20 ; int e_acsl_cst_21 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_19));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_19),(long )12);
- mpz_init((__mpz_struct *)(e_acsl_cst_20));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_20),(long )13);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_19),(long )12);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_20),(long )13);
e_acsl_cst_21 = mpz_cmp((__mpz_struct *)(e_acsl_cst_19),
(__mpz_struct *)(e_acsl_cst_20));
if (e_acsl_cst_21 > 0) { e_acsl_fail((char *)"((12 <= 13))"); }
- mpz_clear((__mpz_struct *)(e_acsl_cst_20));
mpz_clear((__mpz_struct *)(e_acsl_cst_19));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_20));
}
/*@ assert (123 ≥ 12); */ ;
{ mpz_t e_acsl_cst_22 ; mpz_t e_acsl_cst_23 ; int e_acsl_cst_24 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_22));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_22),(long )123);
- mpz_init((__mpz_struct *)(e_acsl_cst_23));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_23),(long )12);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_22),(long )123);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_23),(long )12);
e_acsl_cst_24 = mpz_cmp((__mpz_struct *)(e_acsl_cst_22),
(__mpz_struct *)(e_acsl_cst_23));
if (e_acsl_cst_24 < 0) { e_acsl_fail((char *)"((123 >= 12))"); }
- mpz_clear((__mpz_struct *)(e_acsl_cst_23));
mpz_clear((__mpz_struct *)(e_acsl_cst_22));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_23));
}
/*@ assert (0xff ≡ 0xff); */ ;
{ mpz_t e_acsl_cst_25 ; mpz_t e_acsl_cst_26 ; int e_acsl_cst_27 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_25));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_25),(long )0xff);
- mpz_init((__mpz_struct *)(e_acsl_cst_26));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_26),(long )0xff);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_25),(long )0xff);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_26),(long )0xff);
e_acsl_cst_27 = mpz_cmp((__mpz_struct *)(e_acsl_cst_25),
(__mpz_struct *)(e_acsl_cst_26));
if (e_acsl_cst_27 != 0) { e_acsl_fail((char *)"((0xff == 0xff))"); }
- mpz_clear((__mpz_struct *)(e_acsl_cst_26));
mpz_clear((__mpz_struct *)(e_acsl_cst_25));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_26));
}
/*@ assert (1 ≢ 2); */ ;
{ mpz_t e_acsl_cst_28 ; mpz_t e_acsl_cst_29 ; int e_acsl_cst_30 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_28));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_28),(long )1);
- mpz_init((__mpz_struct *)(e_acsl_cst_29));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_29),(long )2);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_28),(long )1);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_29),(long )2);
e_acsl_cst_30 = mpz_cmp((__mpz_struct *)(e_acsl_cst_28),
(__mpz_struct *)(e_acsl_cst_29));
if (e_acsl_cst_30 == 0) { e_acsl_fail((char *)"((1 != 2))"); }
- mpz_clear((__mpz_struct *)(e_acsl_cst_29));
mpz_clear((__mpz_struct *)(e_acsl_cst_28));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_29));
}
return;
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 83e60b6ded3a6d54d03502a6fc92e5975df909e8..9be9cc4733af9796cdc9829217d545e63c83b0e0 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
@@ -3,28 +3,19 @@
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE:73:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
+[value] computing for function mpz_init_set_si <-main.
Called from PROJECT_FILE:75.
-PROJECT_FILE:75:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
+PROJECT_FILE:75:[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.
-PROJECT_FILE:75:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:76.
-PROJECT_FILE:76:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:76.
-PROJECT_FILE:76:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
+[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:77.
-PROJECT_FILE:77:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:76.
+PROJECT_FILE:76:[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:78.
+ Called from PROJECT_FILE:77.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -35,35 +26,26 @@ PROJECT_FILE:69:[value] Function exit: postcondition got status invalid
[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:79.
-PROJECT_FILE:79:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:78.
+PROJECT_FILE:78:[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:79.
+ Called from PROJECT_FILE:78.
[value] Done for function mpz_clear
-PROJECT_FILE:82:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:84.
-PROJECT_FILE:84:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:84.
-PROJECT_FILE:84:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:85.
-PROJECT_FILE:85:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:85.
-PROJECT_FILE:85:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
+PROJECT_FILE:81:[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
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <-main.
+ Called from PROJECT_FILE:83.
+[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:86.
-PROJECT_FILE:86:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:84.
+PROJECT_FILE:84:[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:87.
+ Called from PROJECT_FILE:85.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -73,35 +55,27 @@ PROJECT_FILE:86:[value] Function mpz_cmp: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:88.
-PROJECT_FILE:88:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:86.
+PROJECT_FILE:86:[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:88.
+ Called from PROJECT_FILE:86.
[value] Done for function mpz_clear
-PROJECT_FILE:91:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:93.
-PROJECT_FILE:93:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_str <-main.
- Called from PROJECT_FILE:94.
-PROJECT_FILE:94:[value] Function mpz_set_str: precondition got status valid
-[value] Done for function mpz_set_str
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:95.
-PROJECT_FILE:95:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_str <-main.
- Called from PROJECT_FILE:96.
-PROJECT_FILE:96:[value] Function mpz_set_str: precondition got status valid
-[value] Done for function mpz_set_str
+PROJECT_FILE:89:[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
+[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
+[value] Done for function mpz_init_set_str
[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:93.
+PROJECT_FILE:93:[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:99.
+ Called from PROJECT_FILE:95.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -111,18 +85,16 @@ PROJECT_FILE:97:[value] Function mpz_cmp: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:100.
-PROJECT_FILE:100:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:96.
+PROJECT_FILE:96:[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:100.
+ Called from PROJECT_FILE:96.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
-[from] Computing for function mpz_init
-[from] Done for function mpz_init
-[from] Computing for function mpz_set_si
-[from] Done for function mpz_set_si
+[from] Computing for function mpz_init_set_si
+[from] Done for function mpz_init_set_si
[from] Computing for function mpz_cmp
[from] Done for function mpz_cmp
[from] Computing for function e_acsl_fail
@@ -134,8 +106,8 @@ PROJECT_FILE:69:[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_set_str
-[from] Done for function mpz_set_str
+[from] Computing for function mpz_init_set_str
+[from] Done for function mpz_init_set_str
[dominators] computing for function main
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
@@ -150,18 +122,16 @@ struct __anonstruct___mpz_struct_1 {
};
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 ) ;
/*@ requires \valid(x);
assigns *x; */
extern void mpz_clear(__mpz_struct * /*[1]*/ x ) ;
-/*@ requires \valid(z);
+/*@ ensures \valid(\at(z,Old));
assigns *z; */
-extern void mpz_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
-/*@ requires \valid(z);
+extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
+/*@ ensures \valid(\at(z,Old));
assigns *z; */
-extern void mpz_set_str(__mpz_struct * /*[1]*/ z , char *str , int base ) ;
+extern void mpz_init_set_str(__mpz_struct * /*[1]*/ z , char *str ,
+ int base ) ;
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
@@ -183,43 +153,38 @@ void main(void)
{
/*@ assert (0 ≡ 0); */ ;
{ mpz_t e_acsl_cst_1 ; mpz_t e_acsl_cst_2 ; int e_acsl_cst_3 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_1));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_1),(long )0);
- mpz_init((__mpz_struct *)(e_acsl_cst_2));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_2),(long )0);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_1),(long )0);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_2),(long )0);
e_acsl_cst_3 = mpz_cmp((__mpz_struct *)(e_acsl_cst_1),
(__mpz_struct *)(e_acsl_cst_2));
if (e_acsl_cst_3 != 0) { e_acsl_fail((char *)"((0 == 0))"); }
- mpz_clear((__mpz_struct *)(e_acsl_cst_2));
mpz_clear((__mpz_struct *)(e_acsl_cst_1));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_2));
}
/*@ assert (0 ≢ 1); */ ;
{ mpz_t e_acsl_cst_4 ; mpz_t e_acsl_cst_5 ; int e_acsl_cst_6 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_4));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_4),(long )0);
- mpz_init((__mpz_struct *)(e_acsl_cst_5));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_5),(long )1);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_4),(long )0);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_cst_5),(long )1);
e_acsl_cst_6 = mpz_cmp((__mpz_struct *)(e_acsl_cst_4),
(__mpz_struct *)(e_acsl_cst_5));
if (e_acsl_cst_6 == 0) { e_acsl_fail((char *)"((0 != 1))"); }
- mpz_clear((__mpz_struct *)(e_acsl_cst_5));
mpz_clear((__mpz_struct *)(e_acsl_cst_4));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_5));
}
/*@ assert (0xfffffffffffffff ≡ 0xfffffffffffffff); */ ;
{ mpz_t e_acsl_cst_7 ; mpz_t e_acsl_cst_8 ; int e_acsl_cst_9 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_7));
- mpz_set_str((__mpz_struct *)(e_acsl_cst_7),(char *)"1152921504606846975",
- 10); mpz_init((__mpz_struct *)(e_acsl_cst_8));
- mpz_set_str((__mpz_struct *)(e_acsl_cst_8),(char *)"1152921504606846975",
- 10);
+ mpz_init_set_str((__mpz_struct *)(e_acsl_cst_7),
+ (char *)"1152921504606846975",10);
+ mpz_init_set_str((__mpz_struct *)(e_acsl_cst_8),
+ (char *)"1152921504606846975",10);
e_acsl_cst_9 = mpz_cmp((__mpz_struct *)(e_acsl_cst_7),
(__mpz_struct *)(e_acsl_cst_8));
if (e_acsl_cst_9 != 0) {
e_acsl_fail((char *)"((0xfffffffffffffff == 0xfffffffffffffff))");
- } mpz_clear((__mpz_struct *)(e_acsl_cst_8));
- mpz_clear((__mpz_struct *)(e_acsl_cst_7));
+ } mpz_clear((__mpz_struct *)(e_acsl_cst_7));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_8));
}
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 8815532e731dc82a04b13370f32032cb9c152065..682d6aca84d3478901c3008451fc904ded2e8825 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
@@ -3,127 +3,15 @@
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE:75:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:77.
-PROJECT_FILE:77:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:77.
-PROJECT_FILE:77:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:78.
-PROJECT_FILE:78:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:78.
-PROJECT_FILE:78:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:79.
-PROJECT_FILE:79:[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:80.
-[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
-[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
-[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:81.
-PROJECT_FILE:81:[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:81.
-[value] Done for function mpz_clear
-PROJECT_FILE:84:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:86.
-PROJECT_FILE:86:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:86.
-PROJECT_FILE:86:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:87.
-PROJECT_FILE:87:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
- Called from PROJECT_FILE:87.
-PROJECT_FILE:87:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:88.
-PROJECT_FILE:88:[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.
-[value] computing for function eprintf <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
-[value] Done for function eprintf
-[value] computing for function exit <-e_acsl_fail <-main.
- Called from PROJECT_FILE:69.
-[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
-[value] Done for function mpz_clear
-[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:91.
-[value] Done for function mpz_clear
+PROJECT_FILE:78:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
-[from] Computing for function mpz_init
-[from] Done for function mpz_init
-[from] Computing for function mpz_set_si
-[from] Done for function mpz_set_si
-[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:69:[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
[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 ∈ {0; }
/* 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 ) ;
-/*@ requires \valid(x);
- assigns *x; */
-extern void mpz_clear(__mpz_struct * /*[1]*/ x ) ;
-/*@ requires \valid(z);
- assigns *z; */
-extern void mpz_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
-/*@ requires \valid(z1);
- requires \valid(z2);
- assigns \nothing; */
-extern int mpz_cmp(__mpz_struct * /*[1]*/ z1 , __mpz_struct * /*[1]*/ z2 ) ;
/*@ terminates \false;
ensures \false;
assigns \nothing; */
@@ -142,33 +30,11 @@ void main(void)
int x ;
x = 0;
/*@ assert (sizeof(int ) ≡ sizeof(x)); */ ;
- { mpz_t e_acsl_cst_1 ; mpz_t e_acsl_cst_2 ; int e_acsl_cst_3 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_1));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_1),(long )4);
- mpz_init((__mpz_struct *)(e_acsl_cst_2));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_2),(long )4);
- e_acsl_cst_3 = mpz_cmp((__mpz_struct *)(e_acsl_cst_1),
- (__mpz_struct *)(e_acsl_cst_2));
- if (e_acsl_cst_3 != 0) {
- e_acsl_fail((char *)"((sizeof(int ) == sizeof(x)))");
- } mpz_clear((__mpz_struct *)(e_acsl_cst_2));
- mpz_clear((__mpz_struct *)(e_acsl_cst_1));
- }
-
+ if (4 != 4) { e_acsl_fail((char *)"((sizeof(int ) == sizeof(x)))"); }
/*@ assert (sizeof("totototototo") ≡ sizeof(char *)); */ ;
- { mpz_t e_acsl_cst_4 ; mpz_t e_acsl_cst_5 ; int e_acsl_cst_6 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_4));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_4),(long )4);
- mpz_init((__mpz_struct *)(e_acsl_cst_5));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_5),(long )4);
- e_acsl_cst_6 = mpz_cmp((__mpz_struct *)(e_acsl_cst_4),
- (__mpz_struct *)(e_acsl_cst_5));
- if (e_acsl_cst_6 != 0) {
- e_acsl_fail((char *)"((sizeof(\"totototototo\") == sizeof(char *)))");
- } mpz_clear((__mpz_struct *)(e_acsl_cst_5));
- mpz_clear((__mpz_struct *)(e_acsl_cst_4));
+ if (4 != 4) {
+ e_acsl_fail((char *)"((sizeof(\"totototototo\") == sizeof(char *)))");
}
-
return;
}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index e80a2ca84184250ef9f108860111a9f53dc580a3..306492bd15eb30268f75cad3cf2779d0e715aba8 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -65,14 +65,14 @@ let mk_if e p =
(* ************************************************************************** *)
module Mpz : sig
- val t_ty: typ (* type "mpz_t" *)
+ 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 set: varinfo -> exp -> stmt
-(* build stmt "mpz_set_*(v, e)" with the good function 'set' according to the
- type of e *)
+ val init_set: varinfo -> exp -> stmt
+(* build stmt "mpz_init_set_*(v, e)" with the good function 'set' according to
+ the type of e *)
end = struct
let t_torig =
@@ -83,26 +83,26 @@ end = struct
let is_now_referenced () = t_torig.treferenced <- true
- let t_ty = TNamed(t_torig, [])
- let is_t ty = Cil_datatype.Typ.equal ty t_ty
+ let t = TNamed(t_torig, [])
+ let is_t ty = Cil_datatype.Typ.equal ty t
let apply_on_var funname v = mk_call ("mpz_" ^ funname) [ new_lval v ]
let init = apply_on_var "init"
let clear = apply_on_var "clear"
- let set v e =
+ let init_set v e =
let fname, args = match typeOf e with
| TInt((IBool | IChar | IUChar | IUInt | IUShort | IULong), _) ->
- "set_ui", [ e ]
- | TInt((ISChar | IShort | IInt | ILong), _) -> "set_si", [ e ]
+ "ui", [ e ]
+ | TInt((ISChar | IShort | IInt | ILong), _) -> "si", [ e ]
| TInt((ILongLong | IULongLong), _) -> assert false
| TPtr(TInt(IChar, _), _) ->
- "set_str",
+ "str",
(* decimal base for the number given as string *)
[ e; integer ~loc:unknown_loc 10 ]
| _ -> assert false
in
- mk_call ("mpz_" ^ fname) (new_lval v :: args)
+ mk_call ("mpz_init_set_" ^ fname) (new_lval v :: args)
end
@@ -111,9 +111,8 @@ end
(* ************************************************************************** *)
module New_vars: sig
- (* constant option: mpz_t constant associated to the varinfo at init time *)
- val push: typ -> exp option -> varinfo
- val finalize: unit -> (varinfo * exp option) list
+ val push: typ -> (varinfo -> stmt list) -> varinfo
+ val finalize: unit -> (varinfo * stmt list * bool) list
end = struct
(* the finalizer resets the counter in order to keep it small. However, Cil
@@ -126,13 +125,10 @@ end = struct
let var_cpt = ref 0
let vlist = ref []
- let push ty e =
- if Mpz.is_t ty then begin
- assert (e <> None);
- Mpz.is_now_referenced ()
- end else
- assert (e = None);
+ let push ty mk_stmts =
incr var_cpt;
+ let is_t = Mpz.is_t ty in
+ if is_t then Mpz.is_now_referenced ();
let v =
makeVarinfo
~logic:false
@@ -142,7 +138,7 @@ end = struct
("e_acsl_cst_" ^ string_of_int !var_cpt)
ty
in
- vlist := (v, e) :: !vlist;
+ vlist := (v, mk_stmts v, is_t) :: !vlist;
v
let finalize () =
@@ -199,9 +195,20 @@ let tlval_to_lval = function
| TVar { lv_origin = Some v }, TNoOffset -> Var v, NoOffset
| _ -> not_yet "complex left value"
-let rec nocheck_term_to_exp t = match t.term_node with
- | TConst c -> constant_to_exp c
- | TLval lv -> new_exp ~loc:unknown_loc (Lval (tlval_to_lval lv))
+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
+ | Lreal -> not_yet "real number"
+ | Larrow _ -> not_yet "logic function"
+
+let rec term_to_exp t = match t.term_node with
+ | TConst c -> wrap_leaf (constant_to_exp c) t.term_type
+ | TLval lv ->
+ wrap_leaf (new_exp ~loc:unknown_loc (Lval (tlval_to_lval lv))) t.term_type
| TSizeOf ty -> sizeOf ~loc:unknown_loc ty
| TSizeOfE t ->
let e = term_to_exp t in
@@ -239,17 +246,6 @@ let rec nocheck_term_to_exp t = match t.term_node with
| Trange _ -> not_yet "range"
| Tlet _ -> not_yet "let binding"
-and term_to_exp t = match t.term_type with
- | Ctype _ -> nocheck_term_to_exp t
- | Ltype _ -> not_yet "term from an user defined type"
- | Lvar _ -> not_yet "polymorphic term"
- | Linteger ->
- let e = nocheck_term_to_exp t in
- let v = New_vars.push Mpz.t_ty (Some e) in
- new_lval v
- | Lreal -> not_yet "real number"
- | Larrow _ -> not_yet "logic function"
-
let relation_to_revbinop = function
| Rlt -> Ge
| Rgt -> Le
@@ -271,12 +267,16 @@ let rec named_predicate_to_revexp p = match p.content with
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 None in
- let result = var v in
- New_block.push (mk_call ~result "mpz_cmp" [ e1; 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 result),
+ new_exp unknown_loc (Lval (var v)),
zero unknown_loc,
intType)
in
@@ -372,20 +372,17 @@ class e_acsl_visitor prj generate = object
assert generate;
let mk_block stmt =
let b = New_block.finalize stmt in
- (* [TODO] efficiency could be improved *)
- gen_vars <-
+ let vars, clears =
List.fold_left
- (fun acc (v, e) ->
- b.blocals <- v :: b.blocals;
- Extlib.may
- (fun e ->
- let s1 = Mpz.init v in
- let s2 = Mpz.set v e in
- b.bstmts <- s1 :: s2 :: b.bstmts @ [ Mpz.clear v ])
- e;
- v :: acc)
- []
- new_vars;
+ (fun (vars, clears) (v, 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)
+ ([], [])
+ new_vars
+ in
+ gen_vars <- vars;
+ b.bstmts <- b.bstmts @ clears;
mkStmt ~valid_sid:true (Block b)
in
ChangeDoChildrenPost(stmt, mk_block)