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

[wp] fix WP target for main function

parent 7dd5bd76
No related branches found
No related tags found
No related merge requests found
...@@ -111,6 +111,8 @@ let check_properties behaviors props kf = ...@@ -111,6 +111,8 @@ let check_properties behaviors props kf =
with Annotations.No_funspec _ -> () with Annotations.No_funspec _ -> ()
in in
let check_bhv kf kinstr bv = let check_bhv kf kinstr bv =
if CfgInfos.is_entry_point kf then
check_bhv_requires kf kinstr bv ;
check_bhv_assigns kf kinstr bv ; check_bhv_assigns kf kinstr bv ;
check_bhv_allocation kf kinstr bv ; check_bhv_allocation kf kinstr bv ;
check_bhv_ensures kf kinstr bv ; check_bhv_ensures kf kinstr bv ;
......
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