Commit ec888b85 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add an "ignore_missing_diverges" debug flag, and use it to check trywhy3's examples.

parent 65cba90e
......@@ -261,6 +261,7 @@ goods bench/typing/x-good --parse-only
bads bench/typing/x-good --type-only
goods bench/programs/good
goods bench/ce
goods src/trywhy3/examples "--debug ignore_missing_diverges"
goods examples/bts
goods examples/tests
goods examples/tests-provers
......
......@@ -32,6 +32,9 @@ let debug_sp = Debug.register_flag "vc_sp"
let no_eval = Debug.register_flag "vc_no_eval"
~desc:"Do@ not@ simplify@ pattern@ matching@ on@ record@ datatypes@ in@ VCs."
let debug_ignore_missing_diverges = Debug.register_info_flag "ignore_missing_diverges"
~desc:"Suppress@ warnings@ on@ missing@ diverges"
let case_split = Ident.create_attribute "case_split"
let add_case t = t_attr_add case_split t
......@@ -520,6 +523,7 @@ let rec k_expr env lps e res xmap =
let var_or_proxy = var_or_proxy_case xmap in
let check_divergence k =
if eff.eff_oneway && not env.divergent then begin
if Debug.test_noflag debug_ignore_missing_diverges then
Warning.emit ?loc "termination@ of@ this@ expression@ \
cannot@ be@ proved,@ but@ there@ is@ no@ `diverges'@ \
clause@ in@ the@ outer@ specification";
......
Markdown is supported
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