From 67fac61865ab48572f04c007fce580e4cee4e7ee Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 28 Aug 2020 11:25:54 +0200
Subject: [PATCH] tentative robustification of WP output
---
tests/bugs/oracle/issue11.res.oracle | 1 +
tests/bugs/oracle/issue23.res.oracle | 1 +
tests/bugs/oracle/issue24.res.oracle | 1 +
tests/bugs/oracle/issue27-pred.res.oracle | 1 +
tests/bugs/oracle/logiccast.res.oracle | 1 +
tests/bugs/oracle/term.res.oracle | 1 +
tests/bugs/test_config | 5 +----
tests/da/test_config | 5 +----
tests/ppwp/oracle/expand.res.oracle | 1 +
tests/ppwp/oracle/expandf.res.oracle | 1 +
tests/ppwp/oracle/simple.res.oracle | 1 +
tests/ppwp/oracle/z.res.oracle | 1 +
tests/ppwp/test_config | 5 +----
tests/specs/wp_empty_struct.cpp | 2 +-
tests/test_config | 2 +-
tests/wp-cache/cache/2457e9e3ceffadd99affa2bac5b00701.json | 1 +
tests/wp-cache/cache/4825227cab959df9b11836e5a86b9400.json | 2 ++
tests/wp-cache/cache/700a49708dbbfb8a3d11c4175ff16350.json | 2 ++
tests/wp-cache/cache/8a114a0d4786d3d300536602a4e51312.json | 2 ++
tests/wp-cache/cache/bbde3b8fa9c480d2796fc88f6c7828a2.json | 2 ++
tests/wp-cache/cache/ea611486826c14112cf2d1bc8011a2a8.json | 2 ++
21 files changed, 26 insertions(+), 14 deletions(-)
create mode 100644 tests/wp-cache/cache/2457e9e3ceffadd99affa2bac5b00701.json
create mode 100644 tests/wp-cache/cache/4825227cab959df9b11836e5a86b9400.json
create mode 100644 tests/wp-cache/cache/700a49708dbbfb8a3d11c4175ff16350.json
create mode 100644 tests/wp-cache/cache/8a114a0d4786d3d300536602a4e51312.json
create mode 100644 tests/wp-cache/cache/bbde3b8fa9c480d2796fc88f6c7828a2.json
create mode 100644 tests/wp-cache/cache/ea611486826c14112cf2d1bc8011a2a8.json
diff --git a/tests/bugs/oracle/issue11.res.oracle b/tests/bugs/oracle/issue11.res.oracle
index ad84c99e..5329ef6f 100644
--- a/tests/bugs/oracle/issue11.res.oracle
+++ b/tests/bugs/oracle/issue11.res.oracle
@@ -1,3 +1,4 @@
+# frama-c -wp [...]
[kernel] Parsing tests/bugs/issue11.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
diff --git a/tests/bugs/oracle/issue23.res.oracle b/tests/bugs/oracle/issue23.res.oracle
index 8d7efd4f..95a1a4e3 100644
--- a/tests/bugs/oracle/issue23.res.oracle
+++ b/tests/bugs/oracle/issue23.res.oracle
@@ -1,3 +1,4 @@
+# frama-c -wp [...]
[kernel] Parsing tests/bugs/issue23.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
diff --git a/tests/bugs/oracle/issue24.res.oracle b/tests/bugs/oracle/issue24.res.oracle
index bc36bc26..a0e6f10b 100644
--- a/tests/bugs/oracle/issue24.res.oracle
+++ b/tests/bugs/oracle/issue24.res.oracle
@@ -1,3 +1,4 @@
+# frama-c -wp [...]
[kernel] Parsing tests/bugs/issue24.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
diff --git a/tests/bugs/oracle/issue27-pred.res.oracle b/tests/bugs/oracle/issue27-pred.res.oracle
index 9947e135..b504fe1c 100644
--- a/tests/bugs/oracle/issue27-pred.res.oracle
+++ b/tests/bugs/oracle/issue27-pred.res.oracle
@@ -1,3 +1,4 @@
+# frama-c -wp [...]
[kernel] Parsing tests/bugs/issue27-pred.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
diff --git a/tests/bugs/oracle/logiccast.res.oracle b/tests/bugs/oracle/logiccast.res.oracle
index af2e9c07..26413556 100644
--- a/tests/bugs/oracle/logiccast.res.oracle
+++ b/tests/bugs/oracle/logiccast.res.oracle
@@ -1,3 +1,4 @@
+# frama-c -wp [...]
[kernel] Parsing tests/bugs/logiccast.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
diff --git a/tests/bugs/oracle/term.res.oracle b/tests/bugs/oracle/term.res.oracle
index a3d27a6d..8e5f0843 100644
--- a/tests/bugs/oracle/term.res.oracle
+++ b/tests/bugs/oracle/term.res.oracle
@@ -1,3 +1,4 @@
+# frama-c -wp [...]
[kernel] Parsing tests/bugs/term.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
diff --git a/tests/bugs/test_config b/tests/bugs/test_config
index 1c8641d6..0e6ce2b6 100644
--- a/tests/bugs/test_config
+++ b/tests/bugs/test_config
@@ -1,4 +1 @@
-FILEREG:.*\.\(cc\|cpp\|ii\)$
-MACRO: CXX -machdep=x86_64 -cxx-c++stdlib-path share/libc++ -cxx-clang-command="bin/framaCIRGen -target x86_64-linux-gnu -D__FC_MACHDEP_X86_64"
-OPT:-print -wp -wp-msg-key shell -wp-cache none @CXX@
-FILTER:/bin/sed -e '/^#[^\n]*/d' -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g" -e 's/Alt-Ergo [0-9.]\+/Alt-Ergo/' -e "s|$(pwd)/||g"
+OPT:-print @CXX@ @WP@
diff --git a/tests/da/test_config b/tests/da/test_config
index 19fd2233..0e6ce2b6 100644
--- a/tests/da/test_config
+++ b/tests/da/test_config
@@ -1,4 +1 @@
-FILEREG:.*\.\(cc\|cpp\|ii\)$
-MACRO: CXX -machdep=x86_64 -cxx-c++stdlib-path share/libc++ -cxx-clang-command="bin/framaCIRGen -target x86_64-linux-gnu -D__FC_MACHDEP_X86_64"
-OPT:-print -wp @CXX@
-##FILTER:/bin/sed -e '/^#[^\n]*/d' -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g"
+OPT:-print @CXX@ @WP@
diff --git a/tests/ppwp/oracle/expand.res.oracle b/tests/ppwp/oracle/expand.res.oracle
index 51e6b1b0..be98e82d 100644
--- a/tests/ppwp/oracle/expand.res.oracle
+++ b/tests/ppwp/oracle/expand.res.oracle
@@ -1,3 +1,4 @@
+# frama-c -wp [...]
[kernel] Parsing tests/ppwp/expand.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
diff --git a/tests/ppwp/oracle/expandf.res.oracle b/tests/ppwp/oracle/expandf.res.oracle
index b3239b7f..a53a4645 100644
--- a/tests/ppwp/oracle/expandf.res.oracle
+++ b/tests/ppwp/oracle/expandf.res.oracle
@@ -1,3 +1,4 @@
+# frama-c -wp [...]
[kernel] Parsing tests/ppwp/expandf.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
diff --git a/tests/ppwp/oracle/simple.res.oracle b/tests/ppwp/oracle/simple.res.oracle
index 80373643..9df53dba 100644
--- a/tests/ppwp/oracle/simple.res.oracle
+++ b/tests/ppwp/oracle/simple.res.oracle
@@ -1,3 +1,4 @@
+# frama-c -wp [...]
[kernel] Parsing tests/ppwp/simple.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
diff --git a/tests/ppwp/oracle/z.res.oracle b/tests/ppwp/oracle/z.res.oracle
index fbc8797c..1b430d32 100644
--- a/tests/ppwp/oracle/z.res.oracle
+++ b/tests/ppwp/oracle/z.res.oracle
@@ -1,3 +1,4 @@
+# frama-c -wp [...]
[kernel] Parsing tests/ppwp/z.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
diff --git a/tests/ppwp/test_config b/tests/ppwp/test_config
index 360cc0a6..0e6ce2b6 100644
--- a/tests/ppwp/test_config
+++ b/tests/ppwp/test_config
@@ -1,4 +1 @@
-FILEREG:.*\.\(cc\|cpp\|ii\)$
-MACRO: CXX -cxx-c++stdlib-path share/libc++ -cxx-clang-command="bin/framaCIRGen"
-OPT:-print -wp @CXX@
-##FILTER:/bin/sed -e '/^#[^\n]*/d' -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g"
+OPT:-print @CXX@ @WP@
diff --git a/tests/specs/wp_empty_struct.cpp b/tests/specs/wp_empty_struct.cpp
index 44cb1143..2a9f5a5f 100644
--- a/tests/specs/wp_empty_struct.cpp
+++ b/tests/specs/wp_empty_struct.cpp
@@ -1,5 +1,5 @@
/* run.config
-OPT: -wp -wp-msg-key shell -wp-cache none @CXX@
+OPT: @CXX@ @WP@
*/
class Point2
{
diff --git a/tests/test_config b/tests/test_config
index 3cdd2697..72b86555 100644
--- a/tests/test_config
+++ b/tests/test_config
@@ -1,6 +1,6 @@
FILEREG:.*\.\(cc\|cpp\|ii\)$
MACRO: CXX -cxx-c++stdlib-path share/libc++ -cxx-clang-command="bin/framaCIRGen"
MACRO: EVA -eva -eva-msg-key=-summary
+MACRO: WP -wp -wp-session tests/wp-cache -wp-cache update -wp-msg-key shell
OPT:-print -check @CXX@
FILTER:/bin/sed -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g" -e "s|$(pwd)/||g"
-##FILTER:/bin/sed -e '/^#[^\n]*/d' -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g"
diff --git a/tests/wp-cache/cache/2457e9e3ceffadd99affa2bac5b00701.json b/tests/wp-cache/cache/2457e9e3ceffadd99affa2bac5b00701.json
new file mode 100644
index 00000000..56c39550
--- /dev/null
+++ b/tests/wp-cache/cache/2457e9e3ceffadd99affa2bac5b00701.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/tests/wp-cache/cache/4825227cab959df9b11836e5a86b9400.json b/tests/wp-cache/cache/4825227cab959df9b11836e5a86b9400.json
new file mode 100644
index 00000000..fb01e1e3
--- /dev/null
+++ b/tests/wp-cache/cache/4825227cab959df9b11836e5a86b9400.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0065,
+ "steps": 4 }
diff --git a/tests/wp-cache/cache/700a49708dbbfb8a3d11c4175ff16350.json b/tests/wp-cache/cache/700a49708dbbfb8a3d11c4175ff16350.json
new file mode 100644
index 00000000..7b2b9ee7
--- /dev/null
+++ b/tests/wp-cache/cache/700a49708dbbfb8a3d11c4175ff16350.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0131,
+ "steps": 7 }
diff --git a/tests/wp-cache/cache/8a114a0d4786d3d300536602a4e51312.json b/tests/wp-cache/cache/8a114a0d4786d3d300536602a4e51312.json
new file mode 100644
index 00000000..79901d73
--- /dev/null
+++ b/tests/wp-cache/cache/8a114a0d4786d3d300536602a4e51312.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0068,
+ "steps": 5 }
diff --git a/tests/wp-cache/cache/bbde3b8fa9c480d2796fc88f6c7828a2.json b/tests/wp-cache/cache/bbde3b8fa9c480d2796fc88f6c7828a2.json
new file mode 100644
index 00000000..5c430d21
--- /dev/null
+++ b/tests/wp-cache/cache/bbde3b8fa9c480d2796fc88f6c7828a2.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0024,
+ "steps": 6 }
diff --git a/tests/wp-cache/cache/ea611486826c14112cf2d1bc8011a2a8.json b/tests/wp-cache/cache/ea611486826c14112cf2d1bc8011a2a8.json
new file mode 100644
index 00000000..a854dd8b
--- /dev/null
+++ b/tests/wp-cache/cache/ea611486826c14112cf2d1bc8011a2a8.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0077,
+ "steps": 3 }
--
GitLab