diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 7c0fa5e2fee5169f4987a60e46cd19f1fd243733..2a4bb7b50269cf021fe54e608ab12e5f5953938d 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -27,9 +27,9 @@ Plugin WP <next-release>
- WP [2021-10-25] Removes -wp-overflows option (unsound)
- WP [2021-06-11] Adds an experimental support of "terminates" clauses.
Adds the options -wp-declaration-terminate and
- -wp-frama-c-stdlib to claims that external functions
+ -wp-frama-c-stdlib to claim that external functions
terminates.
- Adds -wp-declarations-terminate option to claims that
+ Adds -wp-definitions-terminate option to claim that
defined function terminates.
Adds -wp-variant-with-terminates to verify loop
variants under the termination hypothesis.
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 207a87b2c820ab47af0b85bd12d531e7dc0749a9..930f3e439067597fe0408e5a2fd5c98396a940b2 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -202,18 +202,25 @@ let get_terminates_clause kf =
* - then handled in a Some case (as user defined) and returns Defined *)
let defined p =
Defined (WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p) in
- let populate_true () =
+ let populate_true ?(silence=false) () =
let p = Logic_const.new_predicate @@ Logic_const.ptrue in
- Wp_parameters.warning
- ~source:(fst @@ Kernel_function.get_location kf) ~once:true
- "Missing terminates clause for %a, populates 'terminates \\true'"
- Kernel_function.pretty kf ;
+ if not silence then
+ Wp_parameters.warning
+ ~source:(fst @@ Kernel_function.get_location kf) ~once:true
+ "Missing terminates clause for %a, populates 'terminates \\true'"
+ Kernel_function.pretty kf ;
Annotations.add_terminates wp_populate_terminates kf p ;
defined p
in
+ let kf_vi = Kernel_function.get_vi kf in
+ let kf_name = Kernel_function.get_name kf in
match Annotations.terminates kf with
+ | None
+ when Cil_builtins.is_builtin kf_vi
+ || Cil_builtins.is_special_builtin kf_name ->
+ populate_true ~silence:true ()
| None when Kernel_function.is_in_libc kf ->
- if not @@ Wp_parameters.TerminatesFCDeclarations.get ()
+ if not @@ Wp_parameters.TerminatesStdlibDeclarations.get ()
then Assumed Logic_const.pfalse
else populate_true ()
| None when Kernel_function.is_definition kf ->
@@ -237,6 +244,12 @@ let get_terminates_hyp kf =
| Defined (_, p) -> false, p
| Assumed p -> true, p
+let get_decreases_goal kf =
+ let defined t = WpPropId.mk_decrease_id kf Kglobal t, t in
+ match Annotations.decreases ~populate:false kf with
+ | None -> None
+ | Some v -> Some (defined v)
+
(* -------------------------------------------------------------------------- *)
(* --- Contracts --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index a6c4c5bcb36dbe60abecf8e23d8980b204212cbf..294b030675af76c28dd493b4728c972334280dd6 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -57,6 +57,7 @@ val get_complete_behaviors : kernel_function -> pred_info list
val get_disjoint_behaviors : kernel_function -> pred_info list
val get_terminates_goal : kernel_function -> pred_info option
+val get_decreases_goal : kernel_function -> variant_info option
(* -------------------------------------------------------------------------- *)
(* --- Property Accessors : Assertions --- *)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 41c62992ab860b55b9ef1a7228869fe9e3b34071..e867511bf0c67442688eab50df6a8127497d13e3 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -140,6 +140,7 @@ struct
succ: Cfg.vertex -> Cfg.G.edge list;
dead: stmt -> bool ;
terminates: WpPropId.pred_info option ;
+ decreases: WpPropId.variant_info option ;
we: W.t_env;
wp: W.t_prop option Vhash.t; (* None is used for non-dag detection *)
mutable wk: W.t_prop; (* end point *)
@@ -187,11 +188,18 @@ struct
let prove_property env (p : WpPropId.pred_info) w =
if is_selected ~goal:true env p then W.add_goal env.we p w else w
- let prove_subproperty env (p : WpPropId.pred_info) prop stmt source w =
+ let prove_subproperty env (p : WpPropId.pred_info) ?deps prop stmt source w =
if is_selected ~goal:true env p
- then W.add_subgoal env.we p prop stmt source w
+ then W.add_subgoal env.we ?deps p prop stmt source w
else w
+ let on_selected_terminates env f =
+ match env.terminates with
+ | Some t when is_default_bhv env.mode && is_selected ~goal:true env t ->
+ f env t
+ | _ ->
+ Extlib.id
+
(* --- Decomposition of WP Rules --- *)
let rec wp (env:env) (a:vertex) : W.t_prop =
@@ -355,6 +363,33 @@ struct
List.fold_right (prove_property env) complete @@
List.fold_right (prove_property env) disjoint w
+ let do_terminates_deps env w =
+ match env.body with
+ | None -> w
+ | Some _ ->
+ let deps = CfgInfos.terminates_deps env.mode.infos in
+ let return = Kernel_function.find_return env.mode.kf in
+ let prove goal env t w =
+ prove_subproperty env t ~deps goal return FromReturn w
+ in
+ if CfgInfos.is_recursive env.mode.kf then
+ (* there is a dependency on terminates or decreases is missing *)
+ let goal =
+ if None <> env.decreases then Logic_const.ptrue
+ else begin
+ WpLog.warning ~once:true
+ "No 'decreases' clause on recursive function '%a', \
+ cannot prove termination"
+ Kernel_function.pretty env.mode.kf ;
+ Logic_const.pfalse
+ end
+ in
+ on_selected_terminates env (prove goal) w
+ else
+ if not @@ Property.Set.is_empty deps then
+ on_selected_terminates env (prove Logic_const.ptrue) w
+ else w
+
let do_global_init env w =
I.process_global_init env.we env.mode.kf @@
W.scope env.we [] SC_Global w
@@ -378,7 +413,6 @@ struct
(* frame-in *)
W.scope env.we formals SC_Frame_in w
-
let do_post env ~formals (b : CfgAnnot.behavior) w =
W.label env.we None Clabels.post @@
W.scope env.we formals SC_Frame_out @@
@@ -415,9 +449,10 @@ struct
WpLog.SmokeDeadcode.get ()
then CfgInfos.smoking infos else (fun _ -> false) in
let terminates = CfgAnnot.get_terminates_goal kf in
+ let decreases = CfgAnnot.get_decreases_goal kf in
let env = {
mode ; props ; body ;
- succ ; dead ; terminates ;
+ succ ; dead ; terminates ; decreases ;
we = W.new_env kf ;
wp = Vhash.create 32 ;
wk = W.empty ;
@@ -428,6 +463,7 @@ struct
let bhv = CfgAnnot.get_behavior_goals kf ~smoking ~exits mode.bhv in
begin
W.close env.we @@
+ do_terminates_deps env @@
do_global_init env @@
do_preconditions env ~formals bhv @@
do_complete_disjoint env @@
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index a7592df0bfb6c2f3d939956d2358c1b833dad9da..c15ac2a858f54f23f3ab69d5e3649e0dbf8c49ab 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/src/plugins/wp/cfgDump.ml
@@ -106,7 +106,8 @@ let add_goal env (pid,pred) k =
Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
-let add_subgoal env (pid, t_pred) prop stmt _source k =
+let add_subgoal env (pid, t_pred) ?deps prop stmt _source k =
+ ignore deps ;
let u = node () in
if Wp_parameters.debug_atleast 1 then
Format.fprintf !out " %a [ color=red , label=\"Prove %a @@ %a (%a)\" ] ;@."
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 2fc2e6b4a4fab68b201fe30d18f9b3fbc6d8fecb..839c3cf03d55e305fa4125b35e9a0559b1f47124 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -23,6 +23,7 @@
module Cfg = Interpreted_automata
module Fset = Kernel_function.Set
module Sset = Cil_datatype.Stmt.Set
+module Pset = Property.Set
module Shash = Cil_datatype.Stmt.Hashtbl
(* -------------------------------------------------------------------------- *)
@@ -39,6 +40,7 @@ type t = {
mutable doomed : WpPropId.prop_id Bag.t;
mutable calls : Kernel_function.Set.t;
mutable no_variant_loops : Sset.t;
+ mutable terminates_deps : Pset.t;
}
(* -------------------------------------------------------------------------- *)
@@ -61,6 +63,8 @@ let unreachable infos v =
not @@ CheckPath.check_path checkpath cfg.entry_point v
| _ -> true
+let terminates_deps infos = infos.terminates_deps
+
(* -------------------------------------------------------------------------- *)
(* --- Selected Properties --- *)
(* -------------------------------------------------------------------------- *)
@@ -119,6 +123,14 @@ let selected_terminates ~prop kf =
let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
WpPropId.are_selected_names prop (tk_name :: tp_names)
+let selected_decreases ~prop kf =
+ match Annotations.decreases kf with
+ | None -> false
+ | Some (it, _) ->
+ let tk_name = "@decreases" in
+ let tp_names = WpPropId.ident_names it.term_name in
+ WpPropId.are_selected_names prop (tk_name :: tp_names)
+
let selected_disjoint_complete kf ~bhv ~prop =
selected_default ~bhv &&
( selected_clause ~prop "@complete_behaviors" Annotations.complete kf ||
@@ -140,7 +152,7 @@ let selected_main_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
(* --- Calls --- *)
(* -------------------------------------------------------------------------- *)
-let collect_calls ~bhv kf stmt =
+let collect_calls ~bhv ?(on_missing_calls=fun _ -> ()) kf stmt =
let open Cil_types in
match stmt.skind with
| Instr(Call(_,fct,_,_)) ->
@@ -152,11 +164,16 @@ let collect_calls ~bhv kf stmt =
if bhv = []
then List.map (fun b -> b.b_name) (Annotations.behaviors kf)
else bhv in
- List.fold_left
- (fun fs bhv -> match Dyncall.get ~bhv stmt with
- | None -> fs
- | Some(_,kfs) -> List.fold_right Fset.add kfs fs
- ) Fset.empty bhvs
+ let calls =
+ List.fold_left
+ (fun fs bhv -> match Dyncall.get ~bhv stmt with
+ | None -> fs
+ | Some(_,kfs) -> List.fold_right Fset.add kfs fs
+ ) Fset.empty bhvs
+ in
+ if Fset.is_empty calls then
+ on_missing_calls stmt ;
+ calls
end
| Instr(Local_init(x,ConsInit(vf, args, kind), loc)) ->
Cil.treat_constructor_as_func
@@ -167,21 +184,138 @@ let collect_calls ~bhv kf stmt =
x vf args kind loc
| _ -> Fset.empty
+(* -------------------------------------------------------------------------- *)
+(* --- Recursion --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Callees = WpContext.StaticGenerator(Kernel_function)
+ (struct
+ type key = Kernel_function.t
+ type data = Fset.t * Cil_types.stmt list
+ (** functions + unspecified function pointer calls *)
+ let name = "Wp.CfgInfos.SCallees"
+ let compile = function
+ | { Cil_types.fundec = Definition(fd, _ ) } as kf ->
+ let stmts = ref [] in
+ let on_missing_calls s = stmts := s :: !stmts in
+ let fold e s =
+ Fset.union e (collect_calls ~on_missing_calls ~bhv:[] kf s)
+ in
+ let kfs = List.fold_left fold Fset.empty fd.sallstmts in
+ kfs, !stmts
+ | _ -> Fset.empty, []
+ end)
+
+module RecursiveClusters : sig
+ val is_recursive : Kernel_function.t -> bool
+ val get_cluster : Kernel_function.t -> Kernel_function.Set.t option
+end =
+struct
+ (* Tarjan's algorithm, adapted from:
+ http://pauillac.inria.fr/~levy/why3/graph/abs/scct/2/scc.html
+ (proved in Why3)
+ *)
+ let successors kf = fst @@ Callees.get kf
+
+ module HT = Cil_datatype.Kf.Hashtbl
+
+ type env = {
+ mutable stack: Fset.elt list;
+ mutable id: int;
+ table: (Fset.elt, int) Hashtbl.t ;
+ clusters: Fset.t option HT.t ;
+ }
+
+ let rec unstack_to x ?(cluster=[]) = function
+ | [] -> cluster, []
+ | y :: s' when Kernel_function.equal y x -> x :: cluster, s'
+ | y :: s' -> unstack_to x ~cluster:(y :: cluster) s'
+
+ let rec dfs roots env =
+ try
+ let v = Fset.choose roots in
+ let vn =
+ try Hashtbl.find env.table v
+ with Not_found -> visit_node v env
+ in
+ let others_n = dfs (Fset.remove v roots) env in
+ min vn others_n
+ with Not_found -> max_int
+ and visit_node x env =
+ let n = env.id in
+ Hashtbl.replace env.table x n ;
+ env.id <- n + 1;
+ env.stack <- x :: env.stack;
+ let base = dfs (successors x) env in
+ if base < n then base
+ else begin
+ let (cluster, stack) = unstack_to x env.stack in
+ List.iter (fun v -> Hashtbl.replace env.table v max_int) cluster ;
+ env.stack <- stack;
+ begin match cluster with
+ | [ x ] when base = max_int ->
+ HT.add env.clusters x None
+ | cluster ->
+ let set = Some (Fset.of_list cluster) in
+ List.iter (fun kf -> HT.add env.clusters kf set) cluster
+ end ;
+ max_int
+ end
+
+ let make_clusters s =
+ let e = {
+ stack = []; id = 0; table = Hashtbl.create 37; clusters = HT.create 37
+ } in
+ ignore (dfs s e);
+ e.clusters
+
+ module RTable =
+ State_builder.Option_ref(HT.Make(Datatype.Option(Fset)))
+ (struct
+ let name = "Wp.CfgInfo.RecursiveClusters"
+ let dependencies = [ Ast.self ]
+ end)
+
+ let create () =
+ let kfs = ref Kernel_function.Set.empty in
+ Globals.Functions.iter(fun kf -> kfs := Fset.add kf !kfs) ;
+ make_clusters !kfs
+
+ let table () = RTable.memo create
+
+ let get_cluster kf = HT.find (table ()) kf
+ let is_recursive kf =
+ (* in a recursive cluster or contains unspecified function pointer call *)
+ None <> get_cluster kf || [] <> snd @@ Callees.get kf
+end
+
+let is_recursive = RecursiveClusters.is_recursive
+let get_cluster = RecursiveClusters.get_cluster
+
(* -------------------------------------------------------------------------- *)
(* --- No variant loops --- *)
(* -------------------------------------------------------------------------- *)
-let collect_loops_no_variant stmt =
+let collect_loops_no_variant kf stmt =
let open Cil_types in
let fold_no_variant _ = function
- | { annot_content = AVariant _ } -> (&&) false
- | _ -> (&&) true
+ | { annot_content = AVariant v } as ca -> fun _ -> Some (ca, v)
+ | _ -> Extlib.id
+ in
+ let props_of_v ca v =
+ let (d, _), (p, _) = WpStrategy.mk_variant_properties kf stmt ca v in
+ Pset.union
+ (Pset.singleton @@ WpPropId.property_of_id d)
+ (Pset.singleton @@ WpPropId.property_of_id p)
in
match stmt.skind with
- | Loop _ when Annotations.fold_code_annot fold_no_variant stmt true ->
- Sset.singleton stmt
+ | Loop _ ->
+ begin match Annotations.fold_code_annot fold_no_variant stmt None with
+ | None -> Sset.singleton stmt, Pset.empty
+ | Some (ca, v) -> Sset.empty, props_of_v ca (fst v)
+ end
| _ ->
- Sset.empty
+ Sset.empty, Pset.empty
(* -------------------------------------------------------------------------- *)
(* --- Memoization Key --- *)
@@ -265,7 +399,8 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
annots = false ;
doomed = Bag.empty ;
calls = Fset.empty ;
- no_variant_loops = Sset.empty
+ no_variant_loops = Sset.empty ;
+ terminates_deps = Pset.empty ;
} in
let behaviors = Annotations.behaviors kf in
(* Inits *)
@@ -275,6 +410,10 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
Option.iter
begin fun (cfg : Cfg.automaton) ->
(* Spec Iteration *)
+ if selected_decreases ~prop kf then
+ Wp_parameters.warning
+ "Unsupported clause @decreases in '%a' (ignored)"
+ Kernel_function.pretty kf ;
if selected_terminates ~prop kf ||
selected_disjoint_complete kf ~bhv ~prop ||
(List.exists (selected_bhv ~smoking ~bhv ~prop) behaviors)
@@ -283,7 +422,7 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
Shash.iter
(fun stmt (src,_) ->
let fs = collect_calls ~bhv kf stmt in
- let nv_loops = collect_loops_no_variant stmt in
+ let nv_loops, term_deps = collect_loops_no_variant kf stmt in
let dead = unreachable infos src in
let ca = CfgAnnot.get_code_assertions kf stmt in
let ca_pids = List.map fst ca.code_verified in
@@ -306,6 +445,8 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
infos.calls <- Fset.union fs infos.calls ;
infos.no_variant_loops <-
Sset.union nv_loops infos.no_variant_loops ;
+ infos.terminates_deps <-
+ Pset.union term_deps infos.terminates_deps
end
) cfg.stmt_table ;
(* Dead Post Conditions *)
@@ -327,16 +468,44 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
Bag.iter
(fun p -> if WpPropId.filter_status p then WpAnnot.set_unreachable p)
infos.doomed ;
- (* Trivial terminates *)
- if Kernel_function.is_definition kf then
- begin match CfgAnnot.get_terminates_goal kf with
- | Some (id, _t)
- when selected_terminates ~prop kf
- && infos.calls = Fset.empty
- && infos.no_variant_loops = Sset.empty ->
- WpAnnot.set_trivially_terminates id
- | _ -> ()
- end ;
+ (* Termination *)
+ let infos =
+ if Kernel_function.is_definition kf then
+ match CfgAnnot.get_terminates_goal kf with
+ | Some (id, _) when selected_terminates ~prop kf ->
+ let warning_locs =
+ List.map Cil_datatype.Stmt.loc @@ snd @@ Callees.get kf
+ in
+ if warning_locs <> [] then
+ Wp_parameters.warning ~once:true
+ "In '%a', no 'calls' specification for statement(s) on \
+ line(s): %a, @\nAssuming that they can call '%a'"
+ Kernel_function.pretty kf
+ (Pretty_utils.pp_list ~sep:", " Cil_datatype.Location.pretty_line)
+ warning_locs
+ Kernel_function.pretty kf ;
+ if is_recursive kf then
+ (* Notes:
+ - a recursive function never trivially terminates,
+ - in absence of decreases, CfgCalculus will warn *)
+ begin match CfgAnnot.get_decreases_goal kf with
+ | None -> infos
+ | Some (id, _) ->
+ let deps =
+ Pset.add (WpPropId.property_of_id id) infos.terminates_deps
+ in
+ { infos with terminates_deps = deps }
+ end
+ else if infos.calls = Fset.empty
+ && infos.no_variant_loops = Sset.empty then begin
+ WpAnnot.set_trivially_terminates id infos.terminates_deps ;
+ (* Drop dependencies for this terminates, we've used it. *)
+ { infos with terminates_deps = Pset.empty }
+ end
+ else infos
+ | _ -> infos
+ else infos
+ in
(* Collected Infos *)
infos
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
index 472a321933a16e7853b7fd20727ceb0136b27d0f..45172d3653075c7ba3dd971dd286ab2022ac7bec 100644
--- a/src/plugins/wp/cfgInfos.mli
+++ b/src/plugins/wp/cfgInfos.mli
@@ -38,5 +38,9 @@ val doomed : t -> WpPropId.prop_id Bag.t
val calls : t -> Kernel_function.Set.t
val smoking : t -> Cil_types.stmt -> bool
val unreachable : t -> Cfg.vertex -> bool
+val terminates_deps : t -> Property.Set.t
+
+val is_recursive : Kernel_function.t -> bool
+val get_cluster : Kernel_function.t -> Kernel_function.Set.t option
(**************************************************************************)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 869a3f3915845f8bf290cc1f736ed76c918ad304..7c5edf076e143af3de5c65afa06401a88a5fa86b 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -438,10 +438,11 @@ struct
(F.varsp goal) hs
in xs , hs , goal
- let add_vc target ?(warn=Warning.Set.empty) pred vcs =
+ let add_vc
+ target ?(warn=Warning.Set.empty) ?(deps=Property.Set.empty) pred vcs =
let xs , hs , goal = introduction pred in
let hyps = Conditions.intros hs Conditions.nil in
- let vc = { empty_vc with goal=goal ; vars=xs ; hyps=hyps ; warn=warn } in
+ let vc = { empty_vc with goal ; vars=xs ; hyps ; warn ; deps } in
Gmap.add target (Splitter.singleton vc) vcs
(* ------------------------------------------------------------------------ *)
@@ -507,7 +508,7 @@ struct
let vcs = add_vc (Gprop gpid) ~warn goal wp.vcs in
{ wp with vcs = vcs })
- let add_subgoal wenv (gpid, _) predicate stmt source wp = in_wenv wenv wp
+ let add_subgoal wenv (gpid,_) ?deps predicate stmt src wp = in_wenv wenv wp
(fun env wp ->
let outcome = Warning.catch
~severe:true ~effect:"Degenerated goal"
@@ -516,7 +517,7 @@ struct
| Warning.Result(warn,goal) -> warn,goal
| Warning.Failed warn -> warn,F.p_false
in
- let vcs = add_vc (Gsource(gpid, stmt, source)) ~warn goal wp.vcs in
+ let vcs = add_vc (Gsource(gpid, stmt, src)) ~warn ?deps goal wp.vcs in
{ wp with vcs = vcs })
let add_assigns wenv (gpid,ainfo) wp = in_wenv wenv wp
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 937fcb63221b3deac4e2cec20d30eb37727a3547..bd11618cab799e9a36358a40b27274bc1eaad2db 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -797,7 +797,8 @@ interface of the programmatic API.
Recognized categories are: \texttt{@lemma}, \texttt{@requires}, \texttt{@assigns},
\texttt{@ensures}, \texttt{@exits}, \texttt{@assert}, \texttt{@check},
\texttt{@invariant}, \texttt{@variant}, \texttt{@breaks},
- \texttt{@continues}, \texttt{@returns}, \\
+ \texttt{@continues}, \texttt{@returns}, \texttt{@terminates},\\
+ \texttt{@decreases},
\texttt{\mbox{@complete\_behaviors}}, \texttt{\mbox{@disjoint\_behaviors}}.
\\
Properties can be prefixed with a minus sign to \emph{skip} the associated annotations.
@@ -986,7 +987,7 @@ weakest precondition calculus.
\texttt{terminates \textbackslash{}false}, any loop variant proof is trivial)
(default is: \texttt{no}).
\item[\tt -wp-(no)-dynamic] handles calls \textit{via} function pointers
- thanks to the dedicated \verb+@calls f1,...,fn+ code annotation (default is: \texttt{yes}).
+ thanks to the dedicated code annotation \verb+@calls f1,...,fn+ (default is: \texttt{yes}).
\end{description}
\subsubsection{ACSL extension \texttt{@calls}}
@@ -1018,6 +1019,99 @@ These annotations split post-conditions to the dynamic call into two sub-goals:
a second for the call to \verb+f2+. A last goal is generated at the call
site: one must prove that \verb+fp+ is either \verb+f1+ or \verb+f2+.
+\subsubsection{Proof of \texttt{@terminates}}
+
+In ACSL, a function can be specified to terminate when some condition \verb+P+ holds
+in pre-condition.
+
+\begin{lstlisting}[language=c, alsolanguage=acsl]
+/*@ terminates P ; */
+void function(void){
+ ...
+}
+\end{lstlisting}
+
+If terminates verification is active (depending on \verb+-wp+ options) WP collects all function calls and loops
+and generate verification conditions (VCs) to prove them, as detailed below.
+
+\paragraph{Loop variants.} When a loop has a variant, no particular verification
+is generated for termination. However, if \verb+-wp-variant-with-terminates+ is
+active, the variant is verified only when \verb+P+ holds in pre-condition.
+Intuitively, this option means that variant has to decrease only if the function has to terminate. For example:
+
+\begin{lstlisting}[language=c, alsolanguage=acsl]
+//@ terminates i >= 0 ;
+void positive(int i){
+ /*@ loop invariant \at(i, Pre) >= 0 ==> 0 <= i <= \at(i, Pre) ;
+ loop assigns i ;
+ loop variant i ; // verified when i >= 0 at pre
+ */
+ while(i) --i;
+}
+\end{lstlisting}
+
+Note that when \verb+terminates \false+ is specified, any loop
+variant would trivially holds.
+
+When a loop does not have a variant, WP checks that the loop is unreachable
+when \verb+P+ holds in precondition, which means that a loop is allowed to not
+terminate when the function does not have to terminate. For example:
+
+\begin{lstlisting}[language=c, alsolanguage=acsl]
+//@ terminates i >= 0 ;
+void function(int i){
+ if(i < 0){
+ // note i >= 0 && i < 0 ==> \false
+ while(1);
+ }
+}
+\end{lstlisting}
+
+\paragraph{Function call.} When a function \verb+f+ is required to terminate on
+\verb+P+, and calling function \verb+g+ only terminates when \verb+Q+, WP tries to
+prove that \verb+P@pre ==> Q@call-point+. Indeed, for \verb+f+ to terminates while calling
+\verb+g+, then \verb+g+ shall terminate. Note that it
+means that if the function under verification shall terminate, any call to a
+non-terminating function shall be unreachable. For example:
+
+\begin{lstlisting}[language=c, alsolanguage=acsl]
+//@ terminates i <= 0 ;
+void f(int i) ;
+
+//@ terminates i > 0 ;
+void g(int i) ;
+
+/*@ requires i <= 0 ;
+ terminates \true ; */
+void caller(int i){
+ f(i); // succeeds
+ g(i); // fails, thus global termination is not proved
+}
+\end{lstlisting}
+
+When a called function does not have a terminates specification, WP assumes one
+as specified by the options:
+
+\begin{itemize}
+\item \verb+-wp-frama-c-stdlib-terminate+,
+\item \verb+-wp-declarations-terminate+,
+\item \verb+-wp-definitions-terminate+.
+\end{itemize}
+
+\paragraph{(Mutually) recursive function.} When a function is involved in a
+recursive cluster (as defined in the ACSL manual) and shall terminate, WP checks that a
+\verb+decreases+ clause is available for the function. Proving that existing
+recursive calls might be unreachable is delegated to the proof of the
+\verb+decreases+ clause. Note however that, currenlty, the proof of \verb+decreases+
+clauses is not supported yet.
+
+\paragraph{Function pointers. } On a call via a function pointer, WP checks that
+a \verb+@calls+ is specified for this function pointer. If so, WP just behaves
+as explained before for function calls. If such a specification is not available,
+WP considers that the pointed function might call the function under
+verification and thus that it is part of a recursive cluster and shall provide
+a \verb+decreases+ clause.
+
\subsection{Smoke Tests}
During modular deductive verification, inconsistencies in function requirements
diff --git a/src/plugins/wp/mcfg.mli b/src/plugins/wp/mcfg.mli
index 15905e4eab2aecfcec837c07a2690c903bf33cab..3ecd5a5f9a2ae8fe6549d4ba40fd9eaec575d988 100644
--- a/src/plugins/wp/mcfg.mli
+++ b/src/plugins/wp/mcfg.mli
@@ -67,7 +67,7 @@ module type S = sig
val add_axiom : WpPropId.prop_id -> LogicUsage.logic_lemma -> unit
val add_hyp : t_env -> WpPropId.pred_info -> t_prop -> t_prop
val add_goal : t_env -> WpPropId.pred_info -> t_prop -> t_prop
- val add_subgoal : t_env -> WpPropId.pred_info ->
+ val add_subgoal : t_env -> WpPropId.pred_info -> ?deps:Property.Set.t ->
predicate -> stmt -> WpPropId.effect_source -> t_prop -> t_prop
val add_assigns : t_env -> WpPropId.assigns_info -> t_prop -> t_prop
diff --git a/src/plugins/wp/tests/wp_acsl/clusters.i b/src/plugins/wp/tests/wp_acsl/clusters.i
new file mode 100644
index 0000000000000000000000000000000000000000..c1a2e71653c867c4a4cb93eba854d6f5f55f69fa
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/clusters.i
@@ -0,0 +1,64 @@
+/* run.config
+ OPT: -wp-definitions-terminate -wp-declarations-terminate
+*/
+/* run.config_qualif
+ OPT: -wp-definitions-terminate -wp-declarations-terminate
+*/
+
+///// Simple recursion
+
+//@ decreases n ;
+void simpl_r(unsigned n){ // prove termination, warns unsupported decreases
+ if(n) simpl_r(n-1);
+}
+
+void simpl_rf(unsigned n){ // fails termination
+ if(n) simpl_rf(n-1);
+}
+
+///// Mutual recursion
+
+// asks for decreases on both functions "mutual_"
+void mutual_1(unsigned);
+void mutual_2(unsigned);
+// not part of the cluster, termination must succeed
+void callee_no_r(void);
+
+// fails termination (no decreases)
+void mutual_1(unsigned n){
+ if(n) mutual_2(n-1);
+ callee_no_r();
+}
+
+// succeeds termination
+//@ decreases n ;
+void mutual_2(unsigned n){
+ if(n) mutual_1(n-1);
+ simpl_rf(n); // this does not prevent termination proof
+}
+
+void callee_no_r(void){
+
+}
+
+// calls a cluster but not in cluster, termination must succeed
+void caller_no_cluster(void){
+ mutual_1(42);
+}
+
+///// Mutual recursion with function pointer
+
+void fp(void (*)(unsigned), unsigned);
+
+//@ decreases n ;
+void function(unsigned n){
+ if(n) fp(&function, n-1);
+}
+
+// termination fails : recursion without decreases
+//@ requires pf == &function ;
+void fp(void (*pf)(unsigned), unsigned n){
+ if (n)
+ //@ calls function ;
+ (*pf)(n-1) ;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8b18d6554a35709cd335f477d3d044182a349fc0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
@@ -0,0 +1,118 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/clusters.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] tests/wp_acsl/clusters.i:40: Warning:
+ Missing terminates clause for callee_no_r, populates 'terminates \true'
+[wp] [CFG] Goal callee_no_r_terminates : Valid (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/clusters.i:45: Warning:
+ Missing terminates clause for caller_no_cluster, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ Missing terminates clause for fp, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ Unsupported clause @decreases in 'function' (ignored)
+[wp] tests/wp_acsl/clusters.i:54: Warning:
+ Missing terminates clause for function, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:28: Warning:
+ Missing terminates clause for mutual_1, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ Unsupported clause @decreases in 'mutual_2' (ignored)
+[wp] tests/wp_acsl/clusters.i:35: Warning:
+ Missing terminates clause for mutual_2, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ Unsupported clause @decreases in 'simpl_r' (ignored)
+[wp] tests/wp_acsl/clusters.i:11: Warning:
+ Missing terminates clause for simpl_r, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:15: Warning:
+ Missing terminates clause for simpl_rf, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ No 'decreases' clause on recursive function 'simpl_rf', cannot prove termination
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ No 'decreases' clause on recursive function 'mutual_1', cannot prove termination
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ No 'decreases' clause on recursive function 'fp', cannot prove termination
+------------------------------------------------------------
+ Function caller_no_cluster
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'caller_no_cluster':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fp
+------------------------------------------------------------
+
+Goal Call point function in 'fp' at instruction (file tests/wp_acsl/clusters.i, line 63):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'fp' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'fp' (2/2):
+Call Result at line 64
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function function
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'function':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/clusters.i, line 59) in 'fp'' in 'function' at call 'fp' (file tests/wp_acsl/clusters.i, line 55)
+:
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function mutual_1
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'mutual_1' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'mutual_1' (2/2):
+Call Result at line 31
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function mutual_2
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'mutual_2':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function simpl_r
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'simpl_r':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function simpl_rf
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'simpl_rf' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'simpl_rf' (2/2):
+Call Result at line 17
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_fp.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_fp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b4d58200d98eed31ee23fd13bb87396a010c8761
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_fp.res.oracle
@@ -0,0 +1,252 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/terminates_fp.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] tests/wp_acsl/terminates_fp.i:42: Warning:
+ Missing terminates clause for no_t_spec, populates 'terminates \true'
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/terminates_fp.i:62: Warning:
+ Missing terminates clause for no_t_spec_cond, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:70: Warning:
+ Missing terminates clause for no_t_spec_cond_m, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:56: Warning:
+ Missing terminates clause for no_t_spec_in_bhv, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:22: Warning:
+ Missing terminates clause for t_spec, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:36: Warning:
+ Missing terminates clause for t_spec_in_bhv, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:78: Warning:
+ Missing terminates clause for warns_recursive, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:78: Warning:
+ In 'warns_recursive', no 'calls' specification for statement(s) on line(s):
+ line 79,
+ Assuming that they can call 'warns_recursive'
+[wp] tests/wp_acsl/terminates_fp.i:9: Warning:
+ Missing terminates clause for gt, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:11: Warning:
+ Missing terminates clause for ht, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:79: Warning:
+ Missing 'calls' for default behavior
+[wp] tests/wp_acsl/terminates_fp.i:78: Warning:
+ No 'decreases' clause on recursive function 'warns_recursive', cannot prove termination
+------------------------------------------------------------
+ Function no_t_spec
+------------------------------------------------------------
+
+Goal Call point gnt hnt in 'no_t_spec' at instruction (file tests/wp_acsl/terminates_fp.i, line 44):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'no_t_spec' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'no_t_spec' (2/2):
+Call Effect at line 44
+Tags: Call gnt.
+Assume { (* Heap *) Type: region(G_gnt_32) <= 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function no_t_spec_cond
+------------------------------------------------------------
+
+Goal Call point gt hnt in 'no_t_spec_cond' at instruction (file tests/wp_acsl/terminates_fp.i, line 64):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'no_t_spec_cond' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'no_t_spec_cond' (2/2):
+Call Effect at line 64
+Tags: Call hnt.
+Assume { (* Heap *) Type: region(G_hnt_37) <= 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function no_t_spec_cond_m
+------------------------------------------------------------
+
+Goal Call point gt ht in 'no_t_spec_cond_m' at instruction (file tests/wp_acsl/terminates_fp.i, line 72):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Call point hnt in 'no_t_spec_cond_m' at instruction (file tests/wp_acsl/terminates_fp.i, line 75) (1/2):
+Tags: Call gt.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Call point hnt in 'no_t_spec_cond_m' at instruction (file tests/wp_acsl/terminates_fp.i, line 75) (2/2):
+Tags: Call ht.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'no_t_spec_cond_m' (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'no_t_spec_cond_m' (2/3):
+Call Effect at line 75
+Tags: Call gt Call hnt.
+Assume { (* Heap *) Type: (region(G_gt_22) <= 0) /\ (region(G_hnt_37) <= 0).
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'no_t_spec_cond_m' (3/3):
+Call Effect at line 75
+Tags: Call ht Call hnt.
+Assume { (* Heap *) Type: (region(G_hnt_37) <= 0) /\ (region(G_ht_27) <= 0).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function no_t_spec_in_bhv
+------------------------------------------------------------
+
+Goal Call point gnt hnt in 'no_t_spec_in_bhv' at instruction (file tests/wp_acsl/terminates_fp.i, line 58):
+Let a = global(G_hnt_37).
+Let a_1 = global(G_gnt_32).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: region(f.base) <= 0.
+ (* Pre-condition for 'B1' *)
+ Have: ((x = 0) -> (a_1 = f)).
+ (* Pre-condition for 'B2' *)
+ Have: ((x != 0) -> (a = f)).
+}
+Prove: (a_1 = f) \/ (a = f).
+
+------------------------------------------------------------
+
+Goal Complete behaviors 'B1', 'B2':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Disjoint behaviors 'B1', 'B2':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'no_t_spec_in_bhv' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'no_t_spec_in_bhv' (2/2):
+Call Effect at line 58
+Tags: Call gnt.
+Assume { (* Heap *) Type: region(G_gnt_32) <= 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function no_t_spec_in_bhv with behavior B1
+------------------------------------------------------------
+
+Goal Call point gnt hnt in 'no_t_spec_in_bhv' at instruction (file tests/wp_acsl/terminates_fp.i, line 58):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function no_t_spec_in_bhv with behavior B2
+------------------------------------------------------------
+
+Goal Call point gnt hnt in 'no_t_spec_in_bhv' at instruction (file tests/wp_acsl/terminates_fp.i, line 58):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function t_spec
+------------------------------------------------------------
+
+Goal Call point gt ht in 't_spec' at instruction (file tests/wp_acsl/terminates_fp.i, line 24):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 't_spec':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function t_spec_in_bhv
+------------------------------------------------------------
+
+Goal Call point gt hnt in 't_spec_in_bhv' at instruction (file tests/wp_acsl/terminates_fp.i, line 38):
+Let a = global(G_gt_22).
+Let a_1 = global(G_hnt_37).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: region(f.base) <= 0.
+ (* Pre-condition for 'B1' *)
+ Have: ((x = 0) -> (a_1 = f)).
+ (* Pre-condition for 'B2' *)
+ Have: ((x != 0) -> (a = f)).
+}
+Prove: (a = f) \/ (a_1 = f).
+
+------------------------------------------------------------
+
+Goal Complete behaviors 'B1', 'B2':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Disjoint behaviors 'B1', 'B2':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 't_spec_in_bhv' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 't_spec_in_bhv' (2/2):
+Call Effect at line 38
+Tags: Call hnt.
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function t_spec_in_bhv with behavior B1
+------------------------------------------------------------
+
+Goal Call point gt hnt in 't_spec_in_bhv' at instruction (file tests/wp_acsl/terminates_fp.i, line 38):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function t_spec_in_bhv with behavior B2
+------------------------------------------------------------
+
+Goal Call point gt hnt in 't_spec_in_bhv' at instruction (file tests/wp_acsl/terminates_fp.i, line 38):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function warns_recursive
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'warns_recursive':
+Call Result at line 80
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/clusters.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/clusters.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3ce7b7d03b5435e08f555a555d00ab5c0d1b9641
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/clusters.res.oracle
@@ -0,0 +1,59 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/clusters.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] tests/wp_acsl/clusters.i:40: Warning:
+ Missing terminates clause for callee_no_r, populates 'terminates \true'
+[wp] [CFG] Goal callee_no_r_terminates : Valid (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/clusters.i:45: Warning:
+ Missing terminates clause for caller_no_cluster, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ Missing terminates clause for fp, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ Unsupported clause @decreases in 'function' (ignored)
+[wp] tests/wp_acsl/clusters.i:54: Warning:
+ Missing terminates clause for function, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:28: Warning:
+ Missing terminates clause for mutual_1, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ Unsupported clause @decreases in 'mutual_2' (ignored)
+[wp] tests/wp_acsl/clusters.i:35: Warning:
+ Missing terminates clause for mutual_2, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ Unsupported clause @decreases in 'simpl_r' (ignored)
+[wp] tests/wp_acsl/clusters.i:11: Warning:
+ Missing terminates clause for simpl_r, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:15: Warning:
+ Missing terminates clause for simpl_rf, populates 'terminates \true'
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ No 'decreases' clause on recursive function 'simpl_rf', cannot prove termination
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ No 'decreases' clause on recursive function 'mutual_1', cannot prove termination
+[wp] tests/wp_acsl/clusters.i:60: Warning:
+ No 'decreases' clause on recursive function 'fp', cannot prove termination
+[wp] 12 goals scheduled
+[wp] [Qed] Goal typed_simpl_r_terminates : Valid
+[wp] [Qed] Goal typed_simpl_rf_terminates_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_simpl_rf_terminates_part2 : Unsuccess
+[wp] [Qed] Goal typed_mutual_1_terminates_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_mutual_1_terminates_part2 : Unsuccess
+[wp] [Qed] Goal typed_mutual_2_terminates : Valid
+[wp] [Qed] Goal typed_caller_no_cluster_terminates : Valid
+[wp] [Qed] Goal typed_fp_call_point_function_s41 : Valid
+[wp] [Qed] Goal typed_fp_terminates_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_fp_terminates_part2 : Unsuccess
+[wp] [Qed] Goal typed_function_terminates : Valid
+[wp] [Qed] Goal typed_function_call_fp_requires : Valid
+[wp] Proved goals: 10 / 13
+ Qed: 9
+ Alt-Ergo: 0 (unsuccess: 3)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ simpl_r 1 - 1 100%
+ simpl_rf 1 - 2 50.0%
+ mutual_1 1 - 2 50.0%
+ mutual_2 1 - 1 100%
+ caller_no_cluster 1 - 1 100%
+ fp 2 - 3 66.7%
+ function 2 - 2 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_fp.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_fp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..080a16135ea4b4f841d9a85a5bad19597e487f6d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_fp.res.oracle
@@ -0,0 +1,73 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/terminates_fp.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] tests/wp_acsl/terminates_fp.i:42: Warning:
+ Missing terminates clause for no_t_spec, populates 'terminates \true'
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/terminates_fp.i:62: Warning:
+ Missing terminates clause for no_t_spec_cond, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:70: Warning:
+ Missing terminates clause for no_t_spec_cond_m, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:56: Warning:
+ Missing terminates clause for no_t_spec_in_bhv, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:22: Warning:
+ Missing terminates clause for t_spec, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:36: Warning:
+ Missing terminates clause for t_spec_in_bhv, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:78: Warning:
+ Missing terminates clause for warns_recursive, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:78: Warning:
+ In 'warns_recursive', no 'calls' specification for statement(s) on line(s):
+ line 79,
+ Assuming that they can call 'warns_recursive'
+[wp] tests/wp_acsl/terminates_fp.i:9: Warning:
+ Missing terminates clause for gt, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:11: Warning:
+ Missing terminates clause for ht, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_fp.i:79: Warning:
+ Missing 'calls' for default behavior
+[wp] tests/wp_acsl/terminates_fp.i:78: Warning:
+ No 'decreases' clause on recursive function 'warns_recursive', cannot prove termination
+[wp] 29 goals scheduled
+[wp] [Qed] Goal typed_t_spec_call_point_gt_ht_s2 : Valid
+[wp] [Qed] Goal typed_t_spec_terminates : Valid
+[wp] [Alt-Ergo] Goal typed_t_spec_in_bhv_call_point_gt_hnt_s6 : Valid
+[wp] [Qed] Goal typed_t_spec_in_bhv_complete_B1_B2 : Valid
+[wp] [Qed] Goal typed_t_spec_in_bhv_disjoint_B1_B2 : Valid
+[wp] [Qed] Goal typed_t_spec_in_bhv_terminates_part1 : Valid
+[wp] [Qed] Goal typed_t_spec_in_bhv_terminates_part2 : Valid
+[wp] [Qed] Goal typed_t_spec_in_bhv_call_point_gt_hnt_s6 : Valid
+[wp] [Qed] Goal typed_t_spec_in_bhv_call_point_gt_hnt_s6 : Valid
+[wp] [Qed] Goal typed_no_t_spec_call_point_gnt_hnt_s10 : Valid
+[wp] [Qed] Goal typed_no_t_spec_terminates_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_no_t_spec_terminates_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_no_t_spec_in_bhv_call_point_gnt_hnt_s14 : Valid
+[wp] [Qed] Goal typed_no_t_spec_in_bhv_complete_B1_B2 : Valid
+[wp] [Qed] Goal typed_no_t_spec_in_bhv_disjoint_B1_B2 : Valid
+[wp] [Qed] Goal typed_no_t_spec_in_bhv_terminates_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_no_t_spec_in_bhv_terminates_part2 : Unsuccess
+[wp] [Qed] Goal typed_no_t_spec_in_bhv_call_point_gnt_hnt_s14 : Valid
+[wp] [Qed] Goal typed_no_t_spec_in_bhv_call_point_gnt_hnt_s14 : Valid
+[wp] [Qed] Goal typed_no_t_spec_cond_call_point_gt_hnt_s18 : Valid
+[wp] [Qed] Goal typed_no_t_spec_cond_terminates_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_no_t_spec_cond_terminates_part2 : Unsuccess
+[wp] [Qed] Goal typed_no_t_spec_cond_m_call_point_gt_ht_s22 : Valid
+[wp] [Qed] Goal typed_no_t_spec_cond_m_call_point_hnt_s24_part1 : Valid
+[wp] [Qed] Goal typed_no_t_spec_cond_m_call_point_hnt_s24_part2 : Valid
+[wp] [Qed] Goal typed_no_t_spec_cond_m_terminates_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_no_t_spec_cond_m_terminates_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_no_t_spec_cond_m_terminates_part3 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_warns_recursive_terminates : Unsuccess
+[wp] Proved goals: 23 / 29
+ Qed: 21
+ Alt-Ergo: 2 (unsuccess: 6)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ t_spec 2 - 2 100%
+ t_spec_in_bhv 6 1 7 100%
+ no_t_spec 2 - 3 66.7%
+ no_t_spec_in_bhv 5 1 7 85.7%
+ no_t_spec_cond 2 - 3 66.7%
+ no_t_spec_cond_m 4 - 6 66.7%
+ warns_recursive - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/terminates_fp.i b/src/plugins/wp/tests/wp_acsl/terminates_fp.i
new file mode 100644
index 0000000000000000000000000000000000000000..533ea26d3c1ae4d84888bd0cedf9b0b8d066d0b1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/terminates_fp.i
@@ -0,0 +1,80 @@
+/* run.config
+ OPT: -wp-definitions-terminate -wp-declarations-terminate
+*/
+/* run.config_qualif
+ OPT: -wp-definitions-terminate -wp-declarations-terminate
+*/
+
+//@ assigns \nothing ;
+void gt(int);
+//@ assigns \nothing ;
+void ht(int);
+
+/*@ terminates \false ;
+ assigns \nothing ; */
+void gnt(int i);
+
+/*@ terminates i == 0 ;
+ assigns \nothing ; */
+void hnt(int i);
+
+//@ requires f == gt || f == ht ;
+void t_spec(void (*f) (int)){
+ //@ calls gt, ht ;
+ f(0);
+}
+
+/*@ behavior B1:
+ assumes x == 0 ;
+ requires f == hnt ;
+ behavior B2:
+ assumes x != 0 ;
+ requires f == gt ;
+ complete behaviors ;
+ disjoint behaviors ;
+*/
+void t_spec_in_bhv(void (*f) (int), int x){
+ //@ calls gt, hnt ;
+ f(x);
+}
+
+//@ requires f == gnt || f == hnt ;
+void no_t_spec(void (*f) (int)){
+ //@ calls gnt, hnt ;
+ f(0);
+}
+
+/*@ behavior B1:
+ assumes x == 0 ;
+ requires f == gnt ;
+ behavior B2:
+ assumes x != 0 ;
+ requires f == hnt ;
+ complete behaviors ;
+ disjoint behaviors ;
+*/
+void no_t_spec_in_bhv(void (*f) (int), int x){
+ //@ calls gnt, hnt ;
+ f(0);
+}
+
+//@ requires f == gt || f == hnt ;
+void no_t_spec_cond(void (*f) (int)){
+ //@ calls gt, hnt ;
+ f(1);
+}
+
+/*@ requires f == gt || f == ht ;
+ requires g == hnt ;
+*/
+void no_t_spec_cond_m(void (*f) (int), void (*g) (int)){
+ //@ calls gt, ht ;
+ f(0);
+
+ //@ calls hnt ;
+ g(1);
+}
+
+void warns_recursive(void (*f) (int)){
+ f(42);
+}
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 7f6b34561c7a477d185f523f4a2062febb460a50..7a0dc8f397154c76cfcfc13f8aa029173ab82de8 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -89,11 +89,12 @@ let wp_trivially_terminates =
~correctness:[] (* TBC *)
~tuning:[] (* TBC *)
-let set_trivially_terminates p =
+let set_trivially_terminates p hyps =
incr trivial_terminates ;
Wp_parameters.result "[CFG] Goal %a : Valid (Trivial)" WpPropId.pp_propid p ;
let pid = WpPropId.property_of_id p in
- Property_status.emit wp_trivially_terminates ~hyps:[] pid Property_status.True
+ let hyps = Property.Set.elements hyps in
+ Property_status.emit wp_trivially_terminates ~hyps pid Property_status.True
(* -------------------------------------------------------------------------- *)
(* --- Preconditions at Callsites --- *)
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index 171a83e4299dd5991544d77a0d13e102a0a1c3e3..a2b4ebcf85106f1964d12a6273f8296d4ced158e 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -36,7 +36,7 @@ val unreachable_proved : int ref
val unreachable_failed : int ref
val trivial_terminates : int ref
val set_unreachable : WpPropId.prop_id -> unit
-val set_trivially_terminates : WpPropId.prop_id -> unit
+val set_trivially_terminates : WpPropId.prop_id -> Property.Set.t -> unit
type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 7d30a86199f42b9353311eee209fd5e65edcfbf8..904d488371713df01e86d8f875623224f47e8378 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -150,7 +150,7 @@ let mk_disj_bhv_id (kf,ki,active,disj) =
mk_prop PKProp (Property.ip_of_disjoint kf ki active disj)
let mk_compl_bhv_id (kf,ki,active,comp) =
mk_prop PKProp (Property.ip_of_complete kf ki active comp)
-let mk_decrease_id (kf, s, x) =
+let mk_decrease_id kf s x =
mk_prop PKProp (Property.ip_of_decreases kf s x)
let mk_lemma_id l = mk_prop PKProp (LogicUsage.ip_lemma l)
@@ -934,6 +934,7 @@ let pp_assigns_desc fmt a = Wp_error.pp_assigns fmt a.a_assigns
(*----------------------------------------------------------------------------*)
type pred_info = prop_id * Cil_types.predicate
+type variant_info = prop_id * Cil_types.variant
let mk_pred_info id p = (id, p)
let pred_info_id (id, _) = id
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 643b69d72d03055c3323e9dda7e53b95be818221..4be96caf2049b165a4fe196bc98ffd91f1701e07 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -173,7 +173,7 @@ val mk_disj_bhv_id :
val mk_compl_bhv_id :
kernel_function * kinstr * string list * string list -> prop_id
-val mk_decrease_id : kernel_function * kinstr * variant -> prop_id
+val mk_decrease_id : kernel_function -> kinstr -> variant -> prop_id
(** axiom identification *)
val mk_lemma_id : logic_lemma -> prop_id
@@ -265,7 +265,8 @@ type axiom_info = prop_id * LogicUsage.logic_lemma
val mk_axiom_info : LogicUsage.logic_lemma -> axiom_info
val pp_axiom_info : Format.formatter -> axiom_info -> unit
-type pred_info = (prop_id * Cil_types.predicate)
+type pred_info = prop_id * Cil_types.predicate
+type variant_info = prop_id * Cil_types.variant
val mk_pred_info : prop_id -> Cil_types.predicate -> pred_info
val pred_info_id : pred_info -> prop_id
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 528a9b251ff910b2b78a1cf4303b73e8259e9718..d037da922d3448206ffcd2da3aea622730a853c8 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -113,12 +113,12 @@ module Properties =
let arg_name = "p,..."
let help =
"Select properties based names and category.\n\
- Use +name or +category to select properties and -name or -category\n\
+ Use +name or +category to select properties and -name or -category \
to remove them from the selection. The '+' sign can be omitted.\n\
- Categories are: @lemma, @requires, @assigns, @ensures, @exits,\n\
- @assert, @invariant, @variant, @breaks, @continues, @returns,\n\
- @complete_behaviors, @disjoint_behaviors and\n\
- @check (which includes all check clauses)."
+ Categories are: @lemma, @requires, @assigns, @ensures, @exits, \
+ @assert, @invariant, @variant, @breaks, @continues, @returns, \
+ @complete_behaviors, @disjoint_behaviors, @terminates, \
+ @decreases and @check (which includes all check clauses)."
end)
let () = on_reset Properties.clear
@@ -487,7 +487,7 @@ module TerminatesDefinitions =
considered to terminate when called."
end)
-module TerminatesFCDeclarations =
+module TerminatesStdlibDeclarations =
False(struct
let option_name = "-wp-frama-c-stdlib-terminate"
let help = "Frama-C stdlib functions without terminates specification \
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index bcd61322625875596952fe032fdd4899c4000e4e..9c7961f3df2bda0a0235f294a216c67a41372501 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -102,7 +102,7 @@ module SimplifyType : Parameter_sig.Bool
module CalleePreCond : Parameter_sig.Bool
module PrecondWeakening : Parameter_sig.Bool
module TerminatesExtDeclarations : Parameter_sig.Bool
-module TerminatesFCDeclarations : Parameter_sig.Bool
+module TerminatesStdlibDeclarations : Parameter_sig.Bool
module TerminatesDefinitions : Parameter_sig.Bool
module TerminatesVariantHyp : Parameter_sig.Bool