Skip to content
Snippets Groups Projects
Commit fb5c6303 authored by Loïc Correnson's avatar Loïc Correnson Committed by Allan Blanchard
Browse files

[wp/tests] changed dry-run oracles (generated only)

parent 8f9e020e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/register.ml
+ 1
− 1
View file @ fb5c6303
...@@ -369,7 +369,7 @@ let do_wpo_success ~shell ~updating goal success = ...@@ -369,7 +369,7 @@ let do_wpo_success ~shell ~updating goal success =
| None -> () | None -> ()
| Some prover -> | Some prover ->
Wp_parameters.feedback ~ontty:`Silent Wp_parameters.feedback ~ontty:`Silent
"[%a] Goal %s : Valid" VCS.pp_prover prover (Wpo.get_gid goal) "[Generated] Goal %s (%a)" (Wpo.get_gid goal) VCS.pp_prover prover
else else
if Wpo.is_smoke_test goal then if Wpo.is_smoke_test goal then
begin match success with begin match success with
......
src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
+ 3
− 3
View file @ fb5c6303
...@@ -3,9 +3,9 @@ ...@@ -3,9 +3,9 @@
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] 4 goals scheduled [wp] 4 goals scheduled
[wp] [Qed] Goal typed_u8_is_continue_assigns_part3 : Valid [wp] [Generated] Goal typed_u8_is_continue_assigns_part3 (Qed)
[wp] [Qed] Goal typed_u8_is_continue_assigns_part2 : Valid [wp] [Generated] Goal typed_u8_is_continue_assigns_part2 (Qed)
[wp] [Qed] Goal typed_u8_is_continue_assigns_part1 : Valid [wp] [Generated] Goal typed_u8_is_continue_assigns_part1 (Qed)
[wp] 4 goals generated [wp] 4 goals generated
------------------------------------------------------------ ------------------------------------------------------------
Function u8_is_continue Function u8_is_continue
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment