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

[wp/cache] move test using scripts in qualif

parent c1ebf079
No related branches found
No related tags found
No related merge requests found
......@@ -5,11 +5,6 @@
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/unroll.i:20: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 1 goal scheduled
[wp] [Tactical] Goal typed_unrolled_loop_ensures_zero : Valid
[wp] Proved goals: 1 / 1
Qed: 0
Script: 1
------------------------------------------------------------
Function unrolled_loop
------------------------------------------------------------
......@@ -30,6 +25,5 @@ Prove: P_zeroed(Mint_0[a <- 0][shift_uint32(t, 1) <- 0][shift_uint32(t, 2)
[shift_uint32(t, 11) <- 0][shift_uint32(t, 12) <- 0]
[shift_uint32(t, 13) <- 0][shift_uint32(t, 14) <- 0]
[shift_uint32(t, 15) <- 0], t, 0, 15).
Prover Tactical returns Valid
------------------------------------------------------------
# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...]
[kernel] Parsing tests/wp_plugin/unroll.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/unroll.i:20: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 1 goal scheduled
[wp] [Tactical] Goal typed_unrolled_loop_ensures_zero : Valid
[wp] Proved goals: 1 / 1
Qed: 0
Script: 1
[wp] Report in: 'tests/wp_plugin/oracle_qualif/unroll.0.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/unroll.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
unrolled_loop - - 1 100%
-------------------------------------------------------------
/* run.config
OPT: -ulevel=1 -wp -wp-prop=@ensures -wp-prover script -session tests/wp_plugin/unroll -wp-msg-key no-time-info,no-step-info
OPT: -ulevel=1 -wp-prop=@ensures
*/
/* run.config_qualif
DONTRUN:
OPT: -ulevel=1 -wp-prop=@ensures -wp-prover script
*/
enum {Max = 16};
......
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