From c0ef44b1f6eebcf98a127cdb4ab743e3fcdfda7d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 9 Jun 2021 15:47:44 +0200
Subject: [PATCH] [wp] do not set true on terminates for declarations
---
src/plugins/wp/cfgInfos.ml | 17 +++++++++--------
1 file changed, 9 insertions(+), 8 deletions(-)
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 78eed54a2d7..2fc2e6b4a4f 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -328,14 +328,15 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
(fun p -> if WpPropId.filter_status p then WpAnnot.set_unreachable p)
infos.doomed ;
(* Trivial terminates *)
- begin match CfgAnnot.get_terminates_goal kf with
- | Some (id, _t)
- when selected_terminates ~prop kf
- && infos.calls = Fset.empty
- && infos.no_variant_loops = Sset.empty ->
- WpAnnot.set_trivially_terminates id
- | _ -> ()
- end ;
+ if Kernel_function.is_definition kf then
+ begin match CfgAnnot.get_terminates_goal kf with
+ | Some (id, _t)
+ when selected_terminates ~prop kf
+ && infos.calls = Fset.empty
+ && infos.no_variant_loops = Sset.empty ->
+ WpAnnot.set_trivially_terminates id
+ | _ -> ()
+ end ;
(* Collected Infos *)
infos
--
GitLab