diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml index 4069d50b9e25cae0f4f427b42b79dbf40a4cd6e7..c2190cc487b228a0cd82d9aa6db817033c1915ed 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