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

[wp] Prove disjoint and complete

parent ed7e49f5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/cfgCalculus.ml
+ 2
− 2
View file @ a9bad37b
...@@ -347,8 +347,8 @@ struct ...@@ -347,8 +347,8 @@ struct
List.fold_right (use_property env) bhv.bhv_assumes @@ List.fold_right (use_property env) bhv.bhv_assumes @@
List.fold_right (use_property env) bhv.bhv_requires @@ List.fold_right (use_property env) bhv.bhv_requires @@
List.fold_right (use_property env) (behaviors kf) @@ List.fold_right (use_property env) (behaviors kf) @@
List.fold_right (use_property env) (complete mode kf) @@ List.fold_right (prove_property env) (complete mode kf) @@
List.fold_right (use_property env) (disjoint mode kf) @@ List.fold_right (prove_property env) (disjoint mode kf) @@
(* frame-in *) (* frame-in *)
W.scope env.we xs SC_Frame_in @@ W.scope env.we xs SC_Frame_in @@
(* function body *) (* function body *)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment