From c7cdc2285ed4343833301bf00f1a2c5bc2419938 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 2 Mar 2011 12:23:57 +0000
Subject: [PATCH] negation + better tests
---
.../e-acsl/tests/e-acsl-runtime/empty.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/false.i | 6 ++++
.../e-acsl-runtime/{trivial.i => false.i~} | 0
src/plugins/e-acsl/tests/e-acsl-runtime/not.i | 7 ++++
.../{trivial.err.oracle => false.err.oracle} | 0
.../e-acsl-runtime/oracle/false.res.oracle | 34 ++++++++++++++++++
.../e-acsl-runtime/oracle/not.err.oracle | 0
.../{trivial.res.oracle => not.res.oracle} | 0
.../e-acsl-runtime/oracle/true.err.oracle | 0
.../e-acsl-runtime/oracle/true.res.oracle | 35 +++++++++++++++++++
.../e-acsl/tests/e-acsl-runtime/true.i | 6 ++++
src/plugins/e-acsl/visit.ml | 13 +++----
12 files changed, 96 insertions(+), 7 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/false.i
rename src/plugins/e-acsl/tests/e-acsl-runtime/{trivial.i => false.i~} (100%)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/not.i
rename src/plugins/e-acsl/tests/e-acsl-runtime/oracle/{trivial.err.oracle => false.err.oracle} (100%)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.err.oracle
rename src/plugins/e-acsl/tests/e-acsl-runtime/oracle/{trivial.res.oracle => not.res.oracle} (100%)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/true.i
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i b/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i
index 8198e9065e1..7f71fcedc6f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i
@@ -1,3 +1,3 @@
/* run.config
- COMMENT: testing the empty file
+ COMMENT: empty file
OPT: -e-acsl-project p -then-on p -print */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/false.i b/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
new file mode 100644
index 00000000000..8a7597fd11a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
@@ -0,0 +1,6 @@
+/* run.config
+ COMMENT: assert \false */
+void main() {
+ int x = 0;
+ if (x) /*@ assert \false; */ ;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/trivial.i b/src/plugins/e-acsl/tests/e-acsl-runtime/false.i~
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/trivial.i
rename to src/plugins/e-acsl/tests/e-acsl-runtime/false.i~
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/not.i b/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
new file mode 100644
index 00000000000..930555b0449
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
@@ -0,0 +1,7 @@
+/* run.config
+ COMMENT: predicate [!p] */
+void main() {
+ int x = 0;
+ /*@ assert ! \false; */
+ if (x) /*@ assert ! \true; */ ;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/trivial.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/trivial.err.oracle
rename to src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.err.oracle
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
new file mode 100644
index 00000000000..b5118788d6a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
@@ -0,0 +1,34 @@
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+[value] Recording results for main
+[value] done for function main
+[dominators] computing for function main
+[dominators] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values for function main:
+ x ∈ {0; }
+/* Generated by Frama-C */
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status ) ;
+/*@ assigns \nothing; */
+extern void eprintf(char * ) ;
+void e_acsl_fail(char *msg )
+{
+ eprintf(msg);
+ exit(1);
+ return;
+}
+
+void main(void)
+{
+ int x ;
+ x = 0;
+ if (x) { /*@ assert \false; */ ; e_acsl_fail((char *)"(\\false)"); }
+ return;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/trivial.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/trivial.res.oracle
rename to src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
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
new file mode 100644
index 00000000000..476bc8a8161
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
@@ -0,0 +1,35 @@
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+PROJECT_FILE:15:[value] Assertion got status valid.
+[value] Recording results for main
+[value] done for function main
+[dominators] computing for function main
+[dominators] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values for function main:
+ x ∈ {0; }
+/* Generated by Frama-C */
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status ) ;
+/*@ assigns \nothing; */
+extern void eprintf(char * ) ;
+void e_acsl_fail(char *msg )
+{
+ eprintf(msg);
+ exit(1);
+ return;
+}
+
+void main(void)
+{
+ int x ;
+ x = 0;
+ /*@ assert \true; */ ;
+ return;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/true.i b/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
new file mode 100644
index 00000000000..3eb6b45ebe8
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
@@ -0,0 +1,6 @@
+/* run.config
+ COMMENT: assert \true */
+void main() {
+ int x = 0;
+ /*@ assert \true; */
+}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 4bf69d84dd5..c3e545b2d88 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -55,11 +55,9 @@ let mk_if acc e p =
let s = Instr(Call(None, f, [ mkString unknown_loc msg ], unknown_loc))in
mkStmt(If(e, mkBlock [ mkStmt s ], mkBlock [], unknown_loc)) :: acc
-let convert_named_predicate acc generate p =
- let mk_if e = mk_if acc e p in
- match p.content with
- | Pfalse -> if generate then mk_if (one ~loc:unknown_loc) else acc
- | Ptrue -> if generate then mk_if (zero ~loc:unknown_loc) else acc
+let rec named_predicate_to_revexp p = match p.content with
+ | Pfalse -> one ~loc:unknown_loc
+ | Ptrue -> zero ~loc:unknown_loc
| Papp _ -> not_yet "logic function application"
| Pseparated _ -> not_yet "separated"
| Prel _ -> not_yet "relation"
@@ -68,7 +66,7 @@ let convert_named_predicate acc generate p =
| Pxor _ -> not_yet "xor"
| Pimplies _ -> not_yet "==>"
| Piff _ -> not_yet "<==>"
- | Pnot _ -> not_yet "!"
+ | Pnot p -> named_predicate_to_revexp p
| Pif _ -> not_yet "_ ? _ : _"
| Plet _ -> not_yet "let _ = _ in _"
| Pforall _ -> not_yet "\\forall"
@@ -81,6 +79,9 @@ let convert_named_predicate acc generate p =
| Pfresh _ -> not_yet "\\fresh"
| Psubtype _ -> not_yet "subtyping relation"
+let convert_named_predicate acc generate p =
+ if generate then mk_if acc (named_predicate_to_revexp p) p else acc
+
let convert_annotation acc generate annot = match annot.annot_content with
| AAssert(_l, p) -> convert_named_predicate acc generate p
| AStmtSpec _ -> not_yet "stmt spec"
--
GitLab