Skip to content
Snippets Groups Projects
Commit 67fac618 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

tentative robustification of WP output

parent 612e8436
No related branches found
No related tags found
No related merge requests found
Showing
with 24 additions and 14 deletions
# frama-c -wp [...]
[kernel] Parsing tests/bugs/issue11.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
......
# frama-c -wp [...]
[kernel] Parsing tests/bugs/issue23.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
......
# frama-c -wp [...]
[kernel] Parsing tests/bugs/issue24.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
......
# frama-c -wp [...]
[kernel] Parsing tests/bugs/issue27-pred.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
......
# frama-c -wp [...]
[kernel] Parsing tests/bugs/logiccast.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
......
# frama-c -wp [...]
[kernel] Parsing tests/bugs/term.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
......
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@
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@
# frama-c -wp [...]
[kernel] Parsing tests/ppwp/expand.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
......
# frama-c -wp [...]
[kernel] Parsing tests/ppwp/expandf.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
......
# frama-c -wp [...]
[kernel] Parsing tests/ppwp/simple.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
......
# frama-c -wp [...]
[kernel] Parsing tests/ppwp/z.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
......
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@
/* run.config
OPT: -wp -wp-msg-key shell -wp-cache none @CXX@
OPT: @CXX@ @WP@
*/
class Point2
{
......
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"
{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0065,
"steps": 4 }
{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0131,
"steps": 7 }
{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0068,
"steps": 5 }
{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0024,
"steps": 6 }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment