From a9bad37be97567da14d8fe40525d8aa6361c2c82 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 29 Jan 2021 16:32:03 +0100
Subject: [PATCH] [wp] Prove disjoint and complete
---
src/plugins/wp/cfgCalculus.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index f6e58803126..24527f5f773 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -347,8 +347,8 @@ struct
List.fold_right (use_property env) bhv.bhv_assumes @@
List.fold_right (use_property env) bhv.bhv_requires @@
List.fold_right (use_property env) (behaviors kf) @@
- List.fold_right (use_property env) (complete mode kf) @@
- List.fold_right (use_property env) (disjoint mode kf) @@
+ List.fold_right (prove_property env) (complete mode kf) @@
+ List.fold_right (prove_property env) (disjoint mode kf) @@
(* frame-in *)
W.scope env.we xs SC_Frame_in @@
(* function body *)
--
GitLab