From d6689494c96ccf8065037041c201c6d35765eee6 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 4 May 2021 06:47:53 +0000
Subject: [PATCH] [wp] Better comment about assumes normalization
---
src/plugins/wp/cfgAnnot.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 4069d50b9e2..c2190cc487b 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -241,7 +241,7 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
setup_preconditions kf ;
List.iter
begin fun bhv ->
- (* No assumes normalization at this point, Here depends on usage *)
+ (* Normalization of assumes is specific to each case *)
let assumes = Ast_info.behavior_assumes bhv in
let mk_cond = normalize_pre ~goal:true kf bhv ~assumes in
let mk_hpre = normalize_pre ~goal:false kf bhv ~assumes in
--
GitLab