From 166e36535540b5f2954b1039770e3f8c6a7d4a66 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 7 Jun 2021 10:51:56 +0200
Subject: [PATCH] [wp] Simplifies some details in CfgAnnot
---
src/plugins/wp/cfgAnnot.ml | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index d5ff495ee8e..16eb2e534cc 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -186,10 +186,10 @@ let normalize_terminates p =
let get_terminates kf =
Option.map
(fun p -> WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p)
- (Annotations.funspec kf).spec_terminates
+ (Annotations.terminates kf)
let get_terminates_call kf =
- match (Annotations.funspec kf).spec_terminates with
+ match Annotations.terminates kf with
| Some p ->
false, normalize_terminates p
| None when Kernel_function.is_definition kf ->
@@ -472,7 +472,7 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
WpStrategy.mk_variant_properties kf stmt ca term in
let intro_terminates (pid, v) =
pid,
- match (Annotations.funspec kf).spec_terminates with
+ match Annotations.terminates kf with
| Some t when Wp_parameters.TerminatesVariantHyp.get () ->
Logic_const.pimplies (normalize_terminates t, v)
| _ -> v
--
GitLab