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

[wp] do not set true on terminates for declarations

parent 8c47b930
No related branches found
No related tags found
No related merge requests found
...@@ -328,14 +328,15 @@ let compile Key.{ kf ; smoking ; bhv ; prop } = ...@@ -328,14 +328,15 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
(fun p -> if WpPropId.filter_status p then WpAnnot.set_unreachable p) (fun p -> if WpPropId.filter_status p then WpAnnot.set_unreachable p)
infos.doomed ; infos.doomed ;
(* Trivial terminates *) (* Trivial terminates *)
begin match CfgAnnot.get_terminates_goal kf with if Kernel_function.is_definition kf then
| Some (id, _t) begin match CfgAnnot.get_terminates_goal kf with
when selected_terminates ~prop kf | Some (id, _t)
&& infos.calls = Fset.empty when selected_terminates ~prop kf
&& infos.no_variant_loops = Sset.empty -> && infos.calls = Fset.empty
WpAnnot.set_trivially_terminates id && infos.no_variant_loops = Sset.empty ->
| _ -> () WpAnnot.set_trivially_terminates id
end ; | _ -> ()
end ;
(* Collected Infos *) (* Collected Infos *)
infos infos
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment