From f73cc8dd6bb6c1f5f38bc109c17424ced0fce018 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 30 Nov 2011 09:19:49 +0000
Subject: [PATCH] [e-acsl] update tests according to Value's changes [e-acsl]
update todo-list
---
src/plugins/e-acsl/TODO | 9 ++++++---
.../e-acsl-runtime/oracle/addrOf.res.oracle | 2 +-
.../e-acsl-runtime/oracle/arith.res.oracle | 4 ++--
.../e-acsl-runtime/oracle/array.res.oracle | 4 ++--
.../tests/e-acsl-runtime/oracle/at.res.oracle | 8 ++++----
.../e-acsl-runtime/oracle/cast.res.oracle | 4 ++--
.../oracle/comparison.res.oracle | 4 ++--
.../e-acsl-runtime/oracle/false.res.oracle | 2 +-
.../oracle/function_contract.res.oracle | 18 +++++++++---------
.../oracle/integer_constant.res.oracle | 4 ++--
.../e-acsl-runtime/oracle/lazy.res.oracle | 4 ++--
.../oracle/nested_code_annot.res.oracle | 4 ++--
.../tests/e-acsl-runtime/oracle/not.res.oracle | 2 +-
.../e-acsl-runtime/oracle/null.res.oracle | 2 +-
.../oracle/other_constants.res.oracle | 4 ++--
.../tests/e-acsl-runtime/oracle/ptr.res.oracle | 4 ++--
.../e-acsl-runtime/oracle/result.res.oracle | 10 +++++-----
.../e-acsl-runtime/oracle/sizeof.res.oracle | 4 ++--
.../oracle/stmt_contract.res.oracle | 4 ++--
.../e-acsl-runtime/oracle/true.res.oracle | 2 +-
src/plugins/e-acsl/visit.ml | 3 ++-
21 files changed, 53 insertions(+), 49 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index d52e1c85a3f..799deee59a6 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -19,13 +19,13 @@
- constante entière longue: utiliser la représentation sous forme de string et
rechercher la base appropriée.
- arithmetic overflows
-[Bernard] avoir une fonction
+- [Bernard] avoir une fonction
e_acsl_assert(int guard, char *msg, char *kind) {
if (guard) e_acsl_fail(msg, kind);
}
à appeler au lieu de générer la garde. La kind est le type de l'annotation
(assert, requires, ensures, RTE? ...)
-[Bernard] avoir une fonction
+- [Bernard] avoir une fonction
e_acsl_trace_behavior(char *bhv_name) {}
à appeler dès qu'un behavior est activé
- meilleur schéma de compilation des assumes:
@@ -35,6 +35,10 @@
run_function;
ensures_bhv;
}
+- utiliser Rte (get_rte_annotations dans Oxygen)
+- [Yannick] Logic functions
+- type system for generating C int/float when possible
+ (generalisation of current Visit.principal_type)
##############
# KNOWN BUGS #
@@ -47,7 +51,6 @@
#########
- fonction sans code
-- exécuter rte
- tester plusieurs fonctions contenant des annotations
- améliorer test "integer_constant.i" quand bug fixed #745
- test sizeof.i devraient être plus précis quand logic_typing plus précis
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
index ba7dde236b7..d76d6369f19 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
@@ -6,7 +6,7 @@ PROJECT_FILE.i:136:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
x ∈ {0}
/* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index 7d10e2a3f56..667ac7338dc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -808,9 +808,9 @@ PROJECT_FILE.i:521:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
x ∈ {-3}
y ∈ {2}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
index 71c56e656d7..60f253ae3c0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
@@ -37,9 +37,9 @@ PROJECT_FILE.i:157:[value] Assertion got status unknown.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
T1[0] ∈ {0; 2}
[1..2] ∈ {0; 1; 2}
T2[0] ∈ {0; 2}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
index 0b57da4f8fe..84ff0279486 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
@@ -346,9 +346,9 @@ PROJECT_FILE.i:256:[value] Assertion got status unknown.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function f:
+[value] Values at end of function f:
A ∈ {3}
e_acsl_1 ∈ {0}
e_acsl_5 ∈ {1}
@@ -356,7 +356,7 @@ PROJECT_FILE.i:256:[value] Assertion got status unknown.
e_acsl_13 ∈ {0}
e_acsl_14 ∈ {0}
e_acsl_18 ∈ {3}
-[value] Values for function g:
+[value] Values at end of function g:
A ∈ {4}
e_acsl_1 ∈ {0}
e_acsl_2 ∈ {2}
@@ -365,7 +365,7 @@ PROJECT_FILE.i:256:[value] Assertion got status unknown.
x ∈ {1}
t[0] ∈ {2}
[1] ∈ {3}
-[value] Values for function main:
+[value] Values at end of function main:
A ∈ {4}
__retres ∈ {0}
x ∈ {1}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
index 04fedcf0e64..419b294f379 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
@@ -52,9 +52,9 @@ PROJECT_FILE.i:100:[value] Function __gmpz_get_ui: precondition got status valid
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
x ∈ {0}
y ∈ {0}
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 edd0696c274..d5ae506c57d 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
@@ -279,9 +279,9 @@ PROJECT_FILE.i:285:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
x ∈ {0}
y ∈ {1}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
index beab2cdef0d..ef3b4b4c178 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
@@ -5,7 +5,7 @@
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
x ∈ {0}
/* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
index 81b033ed0e0..28f4cda1b75 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
@@ -539,22 +539,22 @@ PROJECT_FILE.i:410:[value] Function l: postcondition got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function f:
+[value] Values at end of function f:
X ∈ {1}
-[value] Values for function g:
+[value] Values at end of function g:
X ∈ {2}
-[value] Values for function h:
+[value] Values at end of function h:
X ∈ {3}
-[value] Values for function i:
+[value] Values at end of function i:
X ∈ {5}
-[value] Values for function j:
+[value] Values at end of function j:
X ∈ {3}
-[value] Values for function k:
+[value] Values at end of function k:
X ∈ {5}
-[value] Values for function l:
-[value] Values for function main:
+[value] Values at end of function l:
+[value] Values at end of function main:
X ∈ {5}
__retres ∈ {0}
/* Generated by Frama-C */
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 06d34e6faeb..92fbba22301 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
@@ -32,9 +32,9 @@ PROJECT_FILE.i:43:[value] Function __gmpz_clear: precondition got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
x ∈ {0}
/* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
index fb826c17cb2..2744a9206e5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
@@ -194,9 +194,9 @@ PROJECT_FILE.i:297:[value] Assertion got status invalid (stopping propagation).
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
x ∈ {0}
y ∈ {1}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
index 132e5846923..c19d36b485a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
@@ -161,9 +161,9 @@ PROJECT_FILE.i:43:[value] Function __gmpz_clear: precondition got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
x ∈ {2}
y ∈ {1}
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 b31bf420596..c48528acf5d 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
@@ -6,7 +6,7 @@ PROJECT_FILE.i:136:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
x ∈ {0}
/* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
index a7721d393d5..265e6cabe40 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
@@ -6,7 +6,7 @@ PROJECT_FILE.i:134:[value] Assertion got status unknown.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
index bd930837970..9b6270007a9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
@@ -32,9 +32,9 @@ PROJECT_FILE.i:152:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
index 2a420a79256..972b05cce49 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
@@ -514,9 +514,9 @@ PROJECT_FILE.i:310:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
x ∈ {1}
t[0] ∈ {2}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
index 7e8190c259b..5f62bd3b13f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
@@ -85,16 +85,16 @@ PROJECT_FILE.i:165:[value] Function h: postcondition got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function g:
-[value] Values for function e_acsl_fail:
+[value] Values at end of function g:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function f:
+[value] Values at end of function f:
x ∈ {0}
e_acsl_1 ∈ {1}
e_acsl_3 ∈ {1}
-[value] Values for function h:
+[value] Values at end of function h:
__retres ∈ {0}
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
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 5bb1671625b..098bbf627fb 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
@@ -62,9 +62,9 @@ PROJECT_FILE.i:150:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
x ∈ {0}
/* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
index fdd4bffc1e3..ebe5dc9303a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
@@ -543,9 +543,9 @@ PROJECT_FILE.i:312:[value] assigning non deterministic value for the first time
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
x ∈ {7}
y ∈ {2}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
index 540c8f0d059..6f641f5decb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
@@ -6,7 +6,7 @@ PROJECT_FILE.i:136:[value] Assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values for function main:
+[value] Values at end of function main:
__retres ∈ {0}
x ∈ {0}
/* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index a02d675b094..4016f2918eb 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -103,8 +103,9 @@ let principal_type_from_term t1 t2 =
Linteger
| TConst (CInt64(_, k, _)), _ ->
(* C-representable constant *)
- Ctype (TInt (k, []))
+ Ctype (TInt (k, []))
| _, _ ->
+ (* for direct C terms, should be able to infer the corresponding C type *)
ty
in
principal_type (typ t1) (typ t2)
--
GitLab