Skip to content
Snippets Groups Projects
Commit 853f7a1a authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] force more stepouts

parent deac2a5b
No related branches found
No related tags found
No related merge requests found
/* run.config_qualif /* run.config_qualif
OPT: -wp-prover native:coq OPT: -wp-prover native:coq
OPT: -wp-prover native:alt-ergo -wp-steps 50 -wp-timeout 1 OPT: -wp-prover native:alt-ergo -wp-steps 5 -wp-timeout 100
OPT: -wp-prover alt-ergo -wp-steps 50 -wp-timeout 1 OPT: -wp-prover alt-ergo -wp-steps 5 -wp-timeout 100
*/ */
//@ ensures KO: \result == 0.2 + x ; //@ ensures KO: \result == 0.2 + x ;
......
...@@ -5,8 +5,8 @@ ...@@ -5,8 +5,8 @@
/* run.config_qualif /* run.config_qualif
OPT: -wp-prover alt-ergo -wp-prop=-ko -wp-timeout 100 -wp-steps 1500 OPT: -wp-prover alt-ergo -wp-prop=-ko -wp-timeout 100 -wp-steps 1500
OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report -wp-prop=-ko -wp-timeout 100 -wp-steps 1500 OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report -wp-prop=-ko -wp-timeout 100 -wp-steps 1500
OPT: -wp-prover alt-ergo -wp-prop=ko -wp-timeout 1 -wp-steps 50 OPT: -wp-prover alt-ergo -wp-prop=ko -wp-timeout 100 -wp-steps 10
OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report -wp-prop=ko -wp-timeout 1 OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report -wp-prop=ko -wp-timeout 100 -wp-steps 10
*/ */
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
......
# frama-c -wp -wp-timeout 1 -wp-steps 50 [...] # frama-c -wp -wp-timeout 100 -wp-steps 5 [...]
[kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing) [kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing)
[kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning: [kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning:
Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
......
# frama-c -wp -wp-timeout 1 -wp-steps 50 [...] # frama-c -wp -wp-timeout 100 -wp-steps 5 [...]
[kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing) [kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing)
[kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning: [kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning:
Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
......
# frama-c -wp -wp-timeout 1 -wp-steps 50 [...] # frama-c -wp -wp-timeout 100 -wp-steps 10 [...]
[kernel] Parsing tests/wp_plugin/math.i (no preprocessing) [kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver' [wp] Loading driver 'share/wp.driver'
......
# frama-c -wp -wp-timeout 1 [...] # frama-c -wp -wp-timeout 100 -wp-steps 10 [...]
[kernel] Parsing tests/wp_plugin/math.i (no preprocessing) [kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver' [wp] Loading driver 'share/wp.driver'
......
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