diff --git a/tests/bugs/oracle/issue11.res.oracle b/tests/bugs/oracle/issue11.res.oracle index ad84c99eb9025f3fed969dd44d4af5eafd6b693b..5329ef6f11cf2c4bd3158cd0235eb03306f5d817 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 8d7efd4fd7dffe99612c6917c8c342a025639e1d..95a1a4e393e1afac010b4e760534fc926e5ea1b2 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 bc36bc2635df80ad79d5fd089a772a1bd319c740..a0e6f10bd7a2ad26a05f087b3db5d298a17013b4 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 9947e135d7bb41de300eea5d4da858c2599c2d33..b504fe1c1e2b2ea8a1f509acd50fa2b3af2891c2 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 af2e9c07c7293c4dedfe45d9f06a9ff56bdae71d..264135561713fbc1ddeba1e4f4b9989d9a5fb02e 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 a3d27a6d1e75ae51b2de8892a0a42eaf111d94cd..8e5f08430c384e6594b5add5050f563405641c2e 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 1c8641d6a624bf12a3a0c335883c5239bc61cb34..0e6ce2b634d2e4b9c4a16fea9061a5b049dac352 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 19fd2233b38e8d691128135165840ef3403a3113..0e6ce2b634d2e4b9c4a16fea9061a5b049dac352 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 51e6b1b00aa4f235431a697e18b5956a7131af05..be98e82df5099c66c69cc2aade5d7788bf3db91d 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 b3239b7f2fa8b4d62398b67070ba5c85c08f1fba..a53a464596cbb9cc3ebd790abbb84cd5848d99bc 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 80373643d6d335127dec6d90bfba47ce147d4198..9df53dba01f8a9cbb2b995711ca7c1f3abd17597 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 fbc8797c38e03de54890cabd9c7f985afe9c7af9..1b430d321518bd28e32c8ea7825005a4ca3c5d95 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 360cc0a6b7e0d6c45fd6fee716388872ad99b2dc..0e6ce2b634d2e4b9c4a16fea9061a5b049dac352 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 44cb11432fd7fb1db4f0ca4785e5ed05a28e8757..2a9f5a5fff70502038832180d860da2a4d36a9e1 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 3cdd26972dff1676fb65e95b80ac275e24d1221e..72b8655548bc640c60e77831da4b8b93bd683b55 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 0000000000000000000000000000000000000000..56c395504289168c539ec44e6877a919ac85adc8 --- /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 0000000000000000000000000000000000000000..fb01e1e39fd5e5c992231114ea222b05b36be2fa --- /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 0000000000000000000000000000000000000000..7b2b9ee7ac681c3828e77a038e271090f84bc8e4 --- /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 0000000000000000000000000000000000000000..79901d730bcef3e9cb22de329023f0b42e06aaec --- /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 0000000000000000000000000000000000000000..5c430d21c441d5273b82c7daef957c6d8f35988e --- /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 0000000000000000000000000000000000000000..a854dd8b5d93a5e541b4f26d3c368ad37d1f043b --- /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 }