From ec888b855b01acd2d3af9178d0f014753cfcd98c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond <guillaume.melquiond@inria.fr> Date: Sun, 24 Jun 2018 09:07:47 +0200 Subject: [PATCH] Add an "ignore_missing_diverges" debug flag, and use it to check trywhy3's examples. --- bench/bench | 1 + src/mlw/vc.ml | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/bench/bench b/bench/bench index 5eb08a0d0..c6a053f0d 100755 --- a/bench/bench +++ b/bench/bench @@ -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 diff --git a/src/mlw/vc.ml b/src/mlw/vc.ml index 6d01cd737..045acf8bf 100644 --- a/src/mlw/vc.ml +++ b/src/mlw/vc.ml @@ -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"; -- GitLab