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

[wp] upgrade float oracles for qualif tests

parent 0df493a9
No related branches found
No related tags found
No related merge requests found
# frama-c -wp -wp-model 'Typed (Real)' -wp-timeout 45 -wp-steps 1500 [...] # frama-c -wp -wp-model 'Typed (Real)' [...]
[kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing) [kernel] Parsing tests/wp_acsl/classify_float.c (with 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-model 'Typed (Real)' -wp-timeout 45 -wp-steps 1500 [...] # frama-c -wp -wp-model 'Typed (Real)' [...]
[kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing) [kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver' [wp] Loading driver 'share/wp.driver'
......
{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0057,
"steps": 4 }
{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0047,
"steps": 4 }
{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0056,
"steps": 4 }
{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.005,
"steps": 4 }
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