From 889fe582e319623abbd67f09030dea8119af76d4 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 4 Mar 2011 16:09:35 +0000
Subject: [PATCH] handling C variables in terms (will be improved when fixing
issue #744) + good test for Pnot
---
.../e-acsl/tests/e-acsl-runtime/comparison.i | 16 +-
src/plugins/e-acsl/tests/e-acsl-runtime/not.i | 4 +-
.../oracle/comparison.res.oracle | 468 +++++++++++++-----
.../oracle/integer_constant.res.oracle | 82 +--
.../e-acsl-runtime/oracle/not.res.oracle | 8 +-
src/plugins/e-acsl/visit.ml | 136 ++---
6 files changed, 487 insertions(+), 227 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i b/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
index 2d4f23b501c..665a48280f5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
@@ -1,13 +1,15 @@
/* run.config
- COMMENT: TODO: this test is incomplete
- COMMENT: comparison operators */
+ COMMENT: comparison operators
+ COMMENT: will be improved by fixing BTS #744 */
void main() {
- /* /\*@ assert "toto" < "titi"; *\/ */
- /* /\*@ assert "toto" > "titi"; *\/ */
- /* /\*@ assert "toto" <= "titi"; *\/ */
- /* /\*@ assert "toto" >= "titi"; *\/ */
- /* /\*@ assert "toto" == "titi"; *\/ */
+ int x = 0, y = 1;
+ /*@ assert x < y; */
+ /*@ assert y > x; */
+ /*@ assert x <= 0; */
+ /*@ assert y >= 1; */
+ char *s = "toto";
+ /*@ assert s == s; */
/*@ assert "toto" != "titi"; */
/*@ assert 5 < 18; */
/*@ assert 32 > 3; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/not.i b/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
index 930555b0449..5349de31bc4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
@@ -2,6 +2,6 @@
COMMENT: predicate [!p] */
void main() {
int x = 0;
- /*@ assert ! \false; */
- if (x) /*@ assert ! \true; */ ;
+ /*@ assert ! x; */
+ if (x) /*@ assert x; */ ;
}
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 e784d46081d..5dcf0a3d4a3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -2,30 +2,29 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE:73:[value] Assertion got status valid.
-PROJECT_FILE:76:[value] Assertion got status valid.
+PROJECT_FILE:78:[value] Assertion got status valid.
[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:78.
-PROJECT_FILE:78:[value] Function mpz_init: postcondition got status unknown
+ 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.
- Called from PROJECT_FILE:78.
-PROJECT_FILE:78:[value] Function mpz_set_si: precondition got status valid
+ 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:79.
-PROJECT_FILE:79:[value] Function mpz_init: postcondition got status unknown
+ 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:79.
-PROJECT_FILE:79:[value] Function mpz_set_si: precondition got status valid
+ 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] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:80.
-PROJECT_FILE:80:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:82.
+PROJECT_FILE:82:[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:81.
+ Called from PROJECT_FILE:83.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -36,35 +35,35 @@ 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:82.
-PROJECT_FILE:82:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:84.
+PROJECT_FILE:84:[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:82.
+ Called from PROJECT_FILE:84.
[value] Done for function mpz_clear
-PROJECT_FILE:85:[value] Assertion got status valid.
+PROJECT_FILE:87:[value] Assertion got status valid.
[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:87.
-PROJECT_FILE:87:[value] Function mpz_init: postcondition got status unknown
+ 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:87.
-PROJECT_FILE:87:[value] Function mpz_set_si: precondition got status valid
+ 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:88.
-PROJECT_FILE:88:[value] Function mpz_init: postcondition got status unknown
+ 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:88.
-PROJECT_FILE:88:[value] Function mpz_set_si: precondition got status valid
+ Called from PROJECT_FILE:90.
+PROJECT_FILE:90:[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:89.
-PROJECT_FILE:89:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:91.
+PROJECT_FILE:91:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:90.
+ Called from PROJECT_FILE:92.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -74,35 +73,35 @@ PROJECT_FILE:89:[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:91.
-PROJECT_FILE:91:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:93.
+PROJECT_FILE:93:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
- Called from PROJECT_FILE:91.
+ Called from PROJECT_FILE:93.
[value] Done for function mpz_clear
-PROJECT_FILE:94:[value] Assertion got status valid.
+PROJECT_FILE:96:[value] Assertion got status valid.
[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:96.
-PROJECT_FILE:96:[value] Function mpz_init: postcondition got status unknown
+ 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:96.
-PROJECT_FILE:96:[value] Function mpz_set_si: precondition got status valid
+ 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:97.
-PROJECT_FILE:97:[value] Function mpz_init: postcondition got status unknown
+ 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:97.
-PROJECT_FILE:97:[value] Function mpz_set_si: precondition got status valid
+ Called from PROJECT_FILE:99.
+PROJECT_FILE:99:[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:98.
-PROJECT_FILE:98:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:100.
+PROJECT_FILE:100:[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:101.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -112,35 +111,35 @@ PROJECT_FILE:98:[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:102.
+PROJECT_FILE:102:[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:102.
[value] Done for function mpz_clear
-PROJECT_FILE:103:[value] Assertion got status valid.
+PROJECT_FILE:105:[value] Assertion got status valid.
[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:105.
-PROJECT_FILE:105:[value] Function mpz_init: postcondition got status unknown
+ 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:105.
-PROJECT_FILE:105:[value] Function mpz_set_si: precondition got status valid
+ 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:106.
-PROJECT_FILE:106:[value] Function mpz_init: postcondition got status unknown
+ 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:106.
-PROJECT_FILE:106:[value] Function mpz_set_si: precondition got status valid
+ Called from PROJECT_FILE:108.
+PROJECT_FILE:108:[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:107.
-PROJECT_FILE:107:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:109.
+PROJECT_FILE:109:[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:108.
+ Called from PROJECT_FILE:110.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -150,27 +149,37 @@ PROJECT_FILE:107:[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:109.
-PROJECT_FILE:109:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:111.
+PROJECT_FILE:111:[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:109.
+ Called from PROJECT_FILE:111.
[value] Done for function mpz_clear
-PROJECT_FILE:112:[value] Assertion got status valid.
+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:113.
-PROJECT_FILE:113:[value] Function mpz_init: postcondition got status unknown
+ 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:114.
-PROJECT_FILE:114:[value] Function mpz_set_si: precondition got status valid
+ 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
[value] computing for function mpz_cmp <-main.
- Called from PROJECT_FILE:115.
-PROJECT_FILE:115:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:125.
+PROJECT_FILE:125:[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:116.
+ Called from PROJECT_FILE:126.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -180,32 +189,35 @@ PROJECT_FILE:115:[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:117.
-PROJECT_FILE:117:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:127.
+PROJECT_FILE:127:[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.
[value] Done for function mpz_clear
-PROJECT_FILE:120:[value] Assertion got status valid.
+PROJECT_FILE:130:[value] Assertion got status valid.
[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:122.
-PROJECT_FILE:122:[value] Function mpz_init: postcondition got status unknown
+ 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:122.
-PROJECT_FILE:122:[value] Function mpz_set_si: precondition got status valid
+ 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:123.
-PROJECT_FILE:123:[value] Function mpz_init: postcondition got status unknown
+ 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:123.
-PROJECT_FILE:123:[value] Function mpz_set_si: precondition got status valid
+ Called from PROJECT_FILE:133.
+PROJECT_FILE:133:[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:124.
-PROJECT_FILE:124:[value] Function mpz_cmp: precondition got status valid
+ Called from PROJECT_FILE:134.
+PROJECT_FILE:134:[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:125.
+ Called from PROJECT_FILE:135.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -215,11 +227,163 @@ PROJECT_FILE:124:[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:126.
-PROJECT_FILE:126:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:136.
+PROJECT_FILE:136:[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:126.
+ Called from PROJECT_FILE:136.
+[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
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:143.
+PROJECT_FILE:143:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:144.
+[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:145.
+PROJECT_FILE:145:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:145.
+[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
+[value] computing for function mpz_cmp <-main.
+ 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:153.
+[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: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:154.
+[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
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:161.
+PROJECT_FILE:161:[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.
+[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:163.
+PROJECT_FILE:163:[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.
+[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
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:170.
+PROJECT_FILE:170:[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.
+[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:172.
+PROJECT_FILE:172:[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.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
@@ -244,6 +408,9 @@ PROJECT_FILE:69:[from] Non terminating function (no dependencies)
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
[value] Values for function main:
+ x ∈ {0; }
+ y ∈ {1; }
+ s ∈ {{ &"toto" ;}}
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
int _mp_alloc ;
@@ -280,81 +447,144 @@ void e_acsl_fail(char *msg )
void main(void)
{
- /*@ assert ("toto" ≢ "titi"); */ ;
- if ("toto" == "titi") { e_acsl_fail((char *)"((\"toto\" != \"titi\"))"); }
- /*@ assert (5 < 18); */ ;
+ int x ;
+ int y ;
+ char *s ;
+ x = 0;
+ 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 )5);
+ 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 )18);
+ mpz_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 *)"((5 < 18))"); }
+ 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));
}
- /*@ assert (32 > 3); */ ;
+ /*@ 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 )32);
+ 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 )3);
+ mpz_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 *)"((32 > 3))"); }
+ 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));
}
- /*@ assert (12 ≤ 13); */ ;
+ /*@ 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 )12);
+ 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 )13);
+ mpz_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 *)"((12 <= 13))"); }
+ 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));
}
- /*@ assert (123 ≥ 12); */ ;
+ /*@ 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 )123);
+ 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 )12);
+ mpz_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 *)"((123 >= 12))"); }
+ 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));
}
- /*@ assert (0xff ≡ 0xff); */ ;
- { mpz_t e_acsl_cst_13 ; int e_acsl_cst_14 ;
+ s = (char *)"toto";
+ /*@ assert (s ≡ s); */ ;
+ if (s != s) { e_acsl_fail((char *)"((s == s))"); }
+ /*@ assert ("toto" ≢ "titi"); */ ;
+ 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 )0xff);
- e_acsl_cst_14 = mpz_cmp((__mpz_struct *)(e_acsl_cst_13),
- (__mpz_struct *)(e_acsl_cst_13));
- if (e_acsl_cst_14 != 0) { e_acsl_fail((char *)"((0xff == 0xff))"); }
+ 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);
+ 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));
}
- /*@ assert (1 ≢ 2); */ ;
- { mpz_t e_acsl_cst_15 ; mpz_t e_acsl_cst_16 ; int e_acsl_cst_17 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_15));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_15),(long )1);
+ /*@ 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 )2);
- e_acsl_cst_17 = mpz_cmp((__mpz_struct *)(e_acsl_cst_15),
- (__mpz_struct *)(e_acsl_cst_16));
- if (e_acsl_cst_17 == 0) { e_acsl_fail((char *)"((1 != 2))"); }
+ 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);
+ 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_15));
+ }
+
+ /*@ 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);
+ 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));
+ }
+
+ /*@ 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);
+ 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));
+ }
+
+ /*@ 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);
+ 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));
+ }
+
+ /*@ 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);
+ 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));
}
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 3d7e25ad0c9..6e1164c4bd2 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
@@ -4,19 +4,27 @@
[value] Values of globals at initialization
PROJECT_FILE:73:[value] Assertion got status valid.
[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:74.
-PROJECT_FILE:74:[value] Function mpz_init: postcondition got status unknown
+ 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.
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_cmp <-main.
+[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_cmp: precondition got status valid
+PROJECT_FILE:76:[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:77.
+PROJECT_FILE:77:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
- Called from PROJECT_FILE:77.
+ Called from PROJECT_FILE:78.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -27,18 +35,13 @@ 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:78.
-PROJECT_FILE:78:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:79.
+PROJECT_FILE:79:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
-PROJECT_FILE:81:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
- Called from PROJECT_FILE:83.
-PROJECT_FILE:83:[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:83.
-PROJECT_FILE:83:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:79.
+[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
@@ -47,12 +50,20 @@ PROJECT_FILE:84:[value] Function mpz_init: postcondition got status unknown
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_cmp <-main.
+[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_cmp: precondition got status valid
+PROJECT_FILE:85:[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:86.
+PROJECT_FILE:86:[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:86.
+ Called from PROJECT_FILE:87.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
@@ -62,11 +73,11 @@ PROJECT_FILE:85:[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:87.
-PROJECT_FILE:87:[value] Function mpz_clear: precondition got status valid
+ Called from PROJECT_FILE:88.
+PROJECT_FILE:88:[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:87.
+ Called from PROJECT_FILE:88.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
@@ -128,26 +139,29 @@ void e_acsl_fail(char *msg )
void main(void)
{
/*@ assert (0 ≡ 0); */ ;
- { mpz_t e_acsl_cst_1 ; int e_acsl_cst_2 ;
+ { 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);
- e_acsl_cst_2 = mpz_cmp((__mpz_struct *)(e_acsl_cst_1),
- (__mpz_struct *)(e_acsl_cst_1));
- if (e_acsl_cst_2 != 0) { e_acsl_fail((char *)"((0 == 0))"); }
+ mpz_init((__mpz_struct *)(e_acsl_cst_2));
+ mpz_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));
}
/*@ assert (0 ≢ 1); */ ;
- { mpz_t e_acsl_cst_3 ; mpz_t e_acsl_cst_4 ; int e_acsl_cst_5 ;
- mpz_init((__mpz_struct *)(e_acsl_cst_3));
- mpz_set_si((__mpz_struct *)(e_acsl_cst_3),(long )0);
+ { 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 )1);
- e_acsl_cst_5 = mpz_cmp((__mpz_struct *)(e_acsl_cst_3),
- (__mpz_struct *)(e_acsl_cst_4));
- if (e_acsl_cst_5 == 0) { e_acsl_fail((char *)"((0 != 1))"); }
+ 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);
+ 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_3));
}
return;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
index f10407fb313..f4443a2fb64 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
@@ -28,8 +28,12 @@ void main(void)
{
int x ;
x = 0;
- /*@ assert \true; */ ;
- if (x) { /*@ assert \false; */ ; e_acsl_fail((char *)"(\\false)"); }
+ /*@ assert (x ≡ 0); */ ;
+ if ((long )x != 0L) { e_acsl_fail((char *)"((x == 0))"); }
+ if (x) {
+ /*@ assert (x ≢ 0); */ ;
+ if ((long )x == 0L) { e_acsl_fail((char *)"((x != 0))"); }
+ }
return;
}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 2c6e18cc999..ddc96da100d 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -56,30 +56,44 @@ let mk_if e p =
let s = mk_call "e_acsl_fail" [ mkString unknown_loc msg ] in
mkStmt ~valid_sid:true (If(e, mkBlock [ s ], mkBlock [], unknown_loc))
+(* ************************************************************************** *)
+(* GMP values *)
+(* ************************************************************************** *)
+
+let mpz_t_torig =
+ { torig_name = "mpz_t";
+ tname = "mpz_t";
+ ttype = TVoid [] (* incorrect but does not matter *);
+ treferenced = false }
+
+let mpz_t_ty = TNamed(mpz_t_torig, [])
+
+let is_mpz_t ty = Cil_datatype.Typ.equal ty mpz_t_ty
+
let apply_mpz_on_var funname v = mk_call ("mpz_" ^ funname) [ new_lval v ]
let apply_mpz_init = apply_mpz_on_var "init"
let apply_mpz_clear = apply_mpz_on_var "clear"
-let apply_mpz_set v cst =
- let fname, args = match cst with
- | CInt64(n, k, s) ->
+let apply_mpz_set v e =
+ let fname, args = match typeOf e with
+ | TInt(k, _) ->
(match k with
| IBool
| IChar
| IUChar
| IUInt
| IUShort
- | IULong -> "set_ui", [ kinteger64_repr ~loc:unknown_loc IULong n s ]
+ | IULong -> "set_ui", [ e ]
| ISChar
| IShort
| IInt
- | ILong -> "set_si", [ kinteger64_repr ~loc:unknown_loc ILong n s ]
+ | ILong -> "set_si", [ e ]
| ILongLong | IULongLong ->
"set_str",
- [ mkString ~loc:unknown_loc (Int64.to_string n);
- integer ~loc:unknown_loc 10 (* decimal base for the number given as
- string *) ])
- | CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _ ->
+ (* [TODO] untested *)
+ (* 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)
@@ -90,11 +104,11 @@ let apply_mpz_set v cst =
module New_vars: sig
- val push: bool -> typ -> constant option -> varinfo
+ val push: bool -> typ -> exp option -> varinfo
(* boolean: [true] if global var
constant option: mpz_t constant associated to the varinfo at init time *)
- val finalize: unit -> (varinfo * constant option) list
+ val finalize: unit -> (varinfo * exp option) list
end = struct
@@ -105,41 +119,29 @@ end = struct
Could be a real issue in practice since **many** variables are generated
for E-ACSL (at least one variable by integer constant). *)
- (* Memoization is local to a stmt: thus it only merges multiple uses of one
- constant in one stmt. *)
- module H = Datatype.Int64.Hashtbl
- let memo_tbl = H.create 7
-
let var_cpt = ref 0
let vlist = ref []
- exception Unknown of int64 option
-
- let push is_global typ c =
- try
- match c with
- | None -> raise (Unknown None)
- | Some (CInt64(n, _, _)) ->
- (try H.find memo_tbl n
- with Not_found -> raise (Unknown (Some n)))
- | Some (CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _) -> assert false
- with Unknown n ->
- incr var_cpt;
- let v =
- makeVarinfo
- ~logic:false
- ~generated:true
- is_global
- false (* is a formal? *)
- ("e_acsl_cst_" ^ string_of_int !var_cpt)
- typ
- in
- (match n with None -> () | Some n -> H.add memo_tbl n v);
- vlist := (v, c) :: !vlist;
- v
+ let push is_global ty e =
+ if is_mpz_t ty then begin
+ assert (e <> None);
+ mpz_t_torig.treferenced <- true
+ end else
+ assert (e = None);
+ incr var_cpt;
+ let v =
+ makeVarinfo
+ ~logic:false
+ ~generated:true (* [TODO] put it to [false]? *)
+ is_global
+ false (* is a formal? *)
+ ("e_acsl_cst_" ^ string_of_int !var_cpt)
+ ty
+ in
+ vlist := (v, e) :: !vlist;
+ v
let finalize () =
- H.clear memo_tbl;
var_cpt := 0;
let l = !vlist in
vlist := [];
@@ -176,31 +178,28 @@ end
(* Transforming terms and predicates into C expressions (if any) *)
(* ************************************************************************** *)
-let mpz_t_torig =
- { torig_name = "mpz_t";
- tname = "mpz_t";
- ttype = TVoid [] (* incorrect but does not matter *);
- treferenced = false }
-
-let mpz_t_ty = TNamed(mpz_t_torig, [])
-
-let is_mpz_t ty = Cil_datatype.Typ.equal ty mpz_t_ty
-
-let constant_to_exp is_global = function
- | CInt64(_, _, _) as c ->
-(* Options.debug ~level:3 "new variable for constant %S" (Int64.to_string n);*)
- mpz_t_torig.treferenced <- true;
- let v = New_vars.push is_global mpz_t_ty (Some c) in
- new_lval v
+let constant_to_exp _is_global = function
+ | CInt64(n, k, s) ->
+ (match k with
+ | IBool | IChar | IUChar | IUInt | IUShort | IULong ->
+ kinteger64_repr ~loc:unknown_loc IULong n s
+ | ISChar | IShort | IInt | ILong ->
+ kinteger64_repr ~loc:unknown_loc ILong n s
+ | ILongLong | IULongLong ->
+ mkString ~loc:unknown_loc (Int64.to_string n))
| CStr _ as c -> new_exp unknown_loc (Const c)
| CWStr _ -> not_yet "wide character string constant"
| CChr _ -> not_yet "character constant"
| CReal _ -> not_yet "floating point constant"
| CEnum _ -> not_yet "enum constant"
-let rec term_to_exp is_global t = match t.term_node with
+let lval_to_exp v off = match v, off with
+ | TVar { lv_origin = Some v }, TNoOffset -> new_lval v
+ | _ -> not_yet "complex left value"
+
+let nocheck_term_to_exp is_global t = match t.term_node with
| TConst c -> constant_to_exp is_global c
- | TLval _ -> not_yet "left value"
+ | TLval(v, off) -> lval_to_exp v off
| TSizeOf _ -> not_yet "sizeof"
| TSizeOfE _ -> not_yet "sizeof(expr)"
| TSizeOfStr _ -> not_yet "sizeof(string constant)"
@@ -232,6 +231,17 @@ let rec term_to_exp is_global t = match t.term_node with
| Trange _ -> not_yet "range"
| Tlet _ -> not_yet "let binding"
+let rec term_to_exp is_global t = match t.term_type with
+ | Ctype _ -> nocheck_term_to_exp is_global t
+ | Ltype _ -> not_yet "term from an user defined type"
+ | Lvar _ -> not_yet "polymorphic term"
+ | Linteger ->
+ let e = nocheck_term_to_exp is_global t in
+ let v = New_vars.push is_global 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
@@ -368,14 +378,14 @@ class e_acsl_visitor prj generate = object (self)
(* [TODO] efficiency could be improved *)
gen_vars <-
List.fold_left
- (fun acc (v, c) ->
+ (fun acc (v, e) ->
b.blocals <- v :: b.blocals;
Extlib.may
- (fun c ->
+ (fun e ->
let s1 = apply_mpz_init v in
- let s2 = apply_mpz_set v c in
+ let s2 = apply_mpz_set v e in
b.bstmts <- s1 :: s2 :: b.bstmts @ [ apply_mpz_clear v ])
- c;
+ e;
v :: acc)
[]
new_vars;
--
GitLab