Skip to content
Snippets Groups Projects
Commit d6689494 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Better comment about assumes normalization

parent 027d8a9e
No related branches found
No related tags found
No related merge requests found
...@@ -241,7 +241,7 @@ module CallContract = WpContext.StaticGenerator(Kernel_function) ...@@ -241,7 +241,7 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
setup_preconditions kf ; setup_preconditions kf ;
List.iter List.iter
begin fun bhv -> 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 assumes = Ast_info.behavior_assumes bhv in
let mk_cond = normalize_pre ~goal:true kf bhv ~assumes in let mk_cond = normalize_pre ~goal:true kf bhv ~assumes in
let mk_hpre = normalize_pre ~goal:false kf bhv ~assumes in let mk_hpre = normalize_pre ~goal:false kf bhv ~assumes in
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment