diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index a921d7ac21a0e8021a796aaa960b970eebf4a4a0..d26c4ef545c2f186914e7a08169f08d500705ce4 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -178,6 +178,25 @@ let get_disjoint_behaviors kf =
L.preproc_annot L.labels_fct_pre @@ Ast_info.disjoint_behaviors spec bs
) spec.spec_disjoint_behaviors
+let normalize_terminates p =
+ let module L = NormAtLabels in
+ L.preproc_annot L.labels_fct_pre @@
+ Logic_const.pat (p.ip_content.tp_statement, BuiltinLabel Pre)
+
+let get_terminates kf =
+ Option.map
+ (fun p -> WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p)
+ (Annotations.funspec kf).spec_terminates
+
+let get_terminates_goal kf =
+ match (Annotations.funspec kf).spec_terminates with
+ | Some p ->
+ normalize_terminates p
+ | None when Kernel_function.is_definition kf ->
+ Logic_const.pfalse
+ | None ->
+ Logic_const.ptrue
+
(* -------------------------------------------------------------------------- *)
(* --- Contracts --- *)
(* -------------------------------------------------------------------------- *)
@@ -189,6 +208,7 @@ type contract = {
contract_exit : WpPropId.pred_info list ;
contract_smoke : WpPropId.pred_info list ;
contract_assigns : Cil_types.assigns ;
+ contract_terminates : Cil_types.predicate ;
}
let assigns_upper_bound behaviors =
@@ -264,13 +284,15 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
| WritesAny -> WritesAny
| Writes froms -> Writes (normalize_froms Normal froms)
in
+ let terminates = get_terminates_goal kf in
{
contract_cond = List.rev !wcond ;
contract_hpre = List.rev !whpre ;
contract_post = List.rev !wpost ;
contract_exit = List.rev !wexit ;
contract_smoke = [] ;
- contract_assigns = assigns
+ contract_assigns = assigns ;
+ contract_terminates = terminates ;
}
end)
@@ -383,6 +405,7 @@ let get_code_assertions ?(smoking=false) kf stmt =
(* -------------------------------------------------------------------------- *)
type loop_contract = {
+ loop_terminates: predicate option;
(* to be verified at loop entry *)
loop_established: WpPropId.pred_info list;
(* to be assumed for loop current *)
@@ -396,6 +419,7 @@ type loop_contract = {
}
let reverse_loop_contract l = {
+ loop_terminates = l.loop_terminates ;
loop_established = List.rev l.loop_established ;
loop_invariants = List.rev l.loop_invariants ;
loop_preserved = List.rev l.loop_preserved ;
@@ -439,9 +463,16 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
| AVariant(term, None) ->
let vpos , vdec =
WpStrategy.mk_variant_properties kf stmt ca term in
- { l with loop_preserved =
- normalize_annot vdec ::
- normalize_annot vpos ::
+ let intro_terminates (pid, v) =
+ pid,
+ match (Annotations.funspec kf).spec_terminates with
+ | None -> v
+ | Some t -> Logic_const.pimplies (normalize_terminates t, v)
+ in
+ { l with loop_terminates = None ;
+ loop_preserved =
+ intro_terminates (normalize_annot vdec) ::
+ intro_terminates (normalize_annot vpos) ::
l.loop_preserved }
| AAssigns(_,WritesAny) ->
let asgn = WpPropId.mk_loop_any_assigns_info stmt in
@@ -457,6 +488,7 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
end
| _ -> l
end stmt {
+ loop_terminates = Some Logic_const.pfalse ;
loop_established = [] ;
loop_invariants = [] ;
loop_preserved = [] ;
@@ -465,12 +497,21 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
}
end)
-let get_loop_contract ?(smoking=false) kf stmt =
+let get_loop_contract ?(smoking=false) ?terminates kf stmt =
let lc = LoopContract.get (kf,stmt) in
- if smoking && not (WpReached.is_dead_code stmt) then
- let g = smoke kf ~id:"dead_loop" ~unreachable:stmt () in
- { lc with loop_smoke = g :: lc.loop_smoke }
- else lc
+ let lc_smoke = if smoking && not (WpReached.is_dead_code stmt) then
+ let g = smoke kf ~id:"dead_loop" ~unreachable:stmt () in
+ { lc with loop_smoke = g :: lc.loop_smoke }
+ else lc
+ in
+ match lc_smoke.loop_terminates, terminates with
+ | None, _->
+ lc_smoke
+ | Some _, None ->
+ { lc_smoke with loop_terminates = None }
+ | Some loop_terminates, Some terminates ->
+ let prop = Logic_const.pimplies(terminates, loop_terminates) in
+ { lc_smoke with loop_terminates = Some prop }
(* -------------------------------------------------------------------------- *)
(* --- Clear Tablesnts --- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 1ca50e9f0ce2ca26a0462d03491ae619278641dd..0c42f7aab3cbccaa2fde6d5345715203b1cc5fef 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -56,6 +56,8 @@ val get_behavior_goals :
val get_complete_behaviors : kernel_function -> pred_info list
val get_disjoint_behaviors : kernel_function -> pred_info list
+val get_terminates : kernel_function -> pred_info option
+
(* -------------------------------------------------------------------------- *)
(* --- Property Accessors : Assertions --- *)
(* -------------------------------------------------------------------------- *)
@@ -76,6 +78,7 @@ val get_stmt_assigns : kernel_function -> stmt -> assigns_full_info list
(* -------------------------------------------------------------------------- *)
type loop_contract = {
+ loop_terminates: predicate option;
(** to be verified at loop entry *)
loop_established: pred_info list;
(** to be assumed for loop current *)
@@ -88,7 +91,7 @@ type loop_contract = {
loop_assigns: assigns_full_info list;
}
-val get_loop_contract : ?smoking:bool ->
+val get_loop_contract : ?smoking:bool -> ?terminates:predicate ->
kernel_function -> stmt -> loop_contract
(* -------------------------------------------------------------------------- *)
@@ -102,6 +105,7 @@ type contract = {
contract_exit : pred_info list ;
contract_smoke : pred_info list ;
contract_assigns : assigns ;
+ contract_terminates : predicate ;
}
val get_call_contract : ?smoking:stmt -> kernel_function -> stmt -> contract
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 697b3eb75e3b8dd4b7f3aa1ce01b892aa447453c..953aab3bce73223ada331ddb1d509f05e5b44e3b 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -139,6 +139,7 @@ struct
body: Cfg.automaton option;
succ: Cfg.vertex -> Cfg.G.edge list;
dead: stmt -> bool ;
+ terminates: WpPropId.pred_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 *)
@@ -186,6 +187,11 @@ 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 =
+ if is_selected ~goal:true env p
+ then W.add_subgoal env.we p prop stmt source w
+ else w
+
(* --- Decomposition of WP Rules --- *)
let rec wp (env:env) (a:vertex) : W.t_prop =
@@ -235,11 +241,17 @@ struct
is_default_bhv m &&
WpLog.SmokeTests.get () &&
WpLog.SmokeDeadloop.get () in
- loop env a s (CfgAnnot.get_loop_contract ~smoking m.kf s)
+ let terminates = Option.map snd env.terminates in
+ loop env a s (CfgAnnot.get_loop_contract ~smoking ?terminates m.kf s)
| Edges -> successors env a
(* Compute loops *)
and loop env a s (lc : CfgAnnot.loop_contract) : W.t_prop =
+ let insert_terminates w = match env.terminates, lc.loop_terminates with
+ | None, _ | _, None -> w (* no terminates goal or nothing to prove *)
+ | Some t, Some prop -> prove_subproperty env t prop s FromCode w
+ in
+ insert_terminates @@
List.fold_right (prove_property env) lc.loop_established @@
List.fold_right (use_assigns env) lc.loop_assigns @@
W.label env.we None (Clabels.loop_current s) @@
@@ -319,10 +331,15 @@ struct
~pexit:c.contract_exit
~assigns:c.contract_assigns
~p_post ~p_exit in
- if is_default_bhv env.mode then
- let pre = List.filter (is_selected_callpre env) c.contract_cond in
- W.call_goal_precond env.we s kf es ~pre w_call
- else w_call
+ let w_pre = if is_default_bhv env.mode then
+ let pre = List.filter (is_selected_callpre env) c.contract_cond in
+ W.call_goal_precond env.we s kf es ~pre w_call
+ else w_call
+ in
+ match env.terminates with
+ | Some p when is_default_bhv env.mode && is_selected ~goal:true env p ->
+ W.call_terminates env.we p s kf es ~callee_t:c.contract_terminates w_pre
+ | _ -> w_pre
let do_complete_disjoint env w =
if not (is_default_bhv env.mode) then w
@@ -378,6 +395,12 @@ struct
env.wk <- if exits then do_exit env ~formals b w else w ;
wp env cfg.entry_point
+ let do_terminates env w =
+ match env.terminates with
+ | Some p when is_default_bhv env.mode && is_selected ~goal:true env p ->
+ prove_property env (fst p, Logic_const.ptrue) w
+ | _ -> w
+
(* Putting everything together *)
let compute ~mode ~props =
let kf = mode.kf in
@@ -392,9 +415,10 @@ struct
WpLog.SmokeTests.get () &&
WpLog.SmokeDeadcode.get ()
then CfgInfos.smoking infos else (fun _ -> false) in
+ let terminates = CfgAnnot.get_terminates kf in
let env = {
mode ; props ; body ;
- succ ; dead ;
+ succ ; dead ; terminates ;
we = W.new_env kf ;
wp = Vhash.create 32 ;
wk = W.empty ;
@@ -409,6 +433,7 @@ struct
do_preconditions env ~formals bhv @@
do_complete_disjoint env @@
do_funbehavior env ~formals ~exits bhv @@
+ do_terminates env @@
W.empty
end
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index 798d85ac72a8951197527fa8d11c9672bf87f8b1..a7592df0bfb6c2f3d939956d2358c1b833dad9da 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/src/plugins/wp/cfgDump.ml
@@ -106,6 +106,19 @@ 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 u = node () in
+ if Wp_parameters.debug_atleast 1 then
+ Format.fprintf !out " %a [ color=red , label=\"Prove %a @@ %a (%a)\" ] ;@."
+ pretty u
+ Printer.pp_predicate t_pred
+ Cil_printer.pp_stmt stmt
+ Printer.pp_predicate prop
+ else
+ Format.fprintf !out " %a [ color=red , label=\"Prove %a\" ] ;@."
+ pretty u WpPropId.pp_propid pid ;
+ merge env u k
+
let pp_assigns fmt = function
| Cil_types.WritesAny -> Format.pp_print_string fmt " \\everything"
| Cil_types.Writes [] -> Format.pp_print_string fmt " \\nothing"
@@ -223,7 +236,20 @@ let call_goal_precond env _stmt kf _es ~pre k =
(fun (_,p) -> Format.fprintf fmt "\n@[<hov 2>Requires %a ;@]"
Printer.pp_predicate p) pre
end ;
- ignore pre ;
+ Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
+ merge env u k
+
+let call_terminates env (_gpid, prop) _stmt kf _es ~callee_t k =
+ let _ = callee_t in
+ let u = node () in
+ Format.fprintf !out " %a [ color=red , label=\"Prove PreCond %a%t\" ] ;@."
+ pretty u Kernel_function.pretty kf
+ begin fun fmt ->
+ if Wp_parameters.debug_atleast 1 then
+ Format.fprintf fmt "\n@[<hov 2>Terminates if %a[%s] ==> %a[%a];@]"
+ Printer.pp_predicate prop "Caller"
+ Printer.pp_predicate callee_t Kernel_function.pretty kf
+ end ;
Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 50ce82a8271924c9a7cef07741647fb3fb0cad87..0bb9bfc65f1412121bdb5b75d644628ff5a08279 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -108,13 +108,14 @@ let selected_call ~bhv ~prop kf =
let selected_clause ~prop name getter kf =
getter kf <> [] && selected_name ~prop name
-let selected_terminates kf =
+let selected_terminates ~prop kf =
match Annotations.terminates kf with
- | None -> ()
+ | None ->
+ false
| Some ip ->
- let loc = ip.ip_content.tp_statement.pred_loc in
- Wp_parameters.warning ~source:(fst loc)
- "Terminates not implemented yet (skipped)."
+ let tk_name = "@terminates" in
+ let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
+ WpPropId.are_selected_names prop (tk_name :: tp_names)
let selected_disjoint_complete kf ~bhv ~prop =
selected_default ~bhv &&
@@ -255,8 +256,8 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
Option.iter
begin fun (cfg : Cfg.automaton) ->
(* Spec Iteration *)
- selected_terminates kf ;
- if selected_disjoint_complete kf ~bhv ~prop ||
+ if selected_terminates ~prop kf ||
+ selected_disjoint_complete kf ~bhv ~prop ||
(List.exists (selected_bhv ~smoking ~bhv ~prop) behaviors)
then infos.annots <- true ;
(* Stmt Iteration *)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index ba8d3245e87db470fa5b710e25c811b79803fa4e..5f0767c667b169e7b5eff49b5007636e14a92a0b 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -55,7 +55,7 @@ struct
type target =
| Gprop of P.t
- | Geffect of P.t * Stmt.t * effect_source
+ | Gsource of P.t * Stmt.t * effect_source
| Gposteffect of P.t
module TARGET =
@@ -65,33 +65,33 @@ struct
| FromCode -> 1 | FromCall -> 2 | FromReturn -> 3
let hash = function
| Gprop p | Gposteffect p -> P.hash p
- | Geffect(p,s,e) -> P.hash p * 37 + 41 * Stmt.hash s + hsrc e
+ | Gsource(p,s,e) -> P.hash p * 37 + 41 * Stmt.hash s + hsrc e
let compare g1 g2 =
if g1 == g2 then 0 else
match g1,g2 with
| Gprop p1 , Gprop p2 -> P.compare p1 p2
| Gprop _ , _ -> (-1)
| _ , Gprop _ -> 1
- | Geffect(p1,s1,e1) , Geffect(p2,s2,e2) ->
+ | Gsource(p1,s1,e1) , Gsource(p2,s2,e2) ->
let c = P.compare p1 p2 in
if c <> 0 then c else
let c = Stmt.compare s1 s2 in
if c <> 0 then c else
hsrc e1 - hsrc e2
- | Geffect _ , _ -> (-1)
- | _ , Geffect _ -> 1
+ | Gsource _ , _ -> (-1)
+ | _ , Gsource _ -> 1
| Gposteffect p1 , Gposteffect p2 -> P.compare p1 p2
let equal g1 g2 = (compare g1 g2 = 0)
- let prop_id = function Gprop p | Gposteffect p | Geffect(p,_,_) -> p
- let source = function Gprop _ | Gposteffect _ -> None | Geffect(_,s,e) -> Some(s,e)
+ let prop_id = function Gprop p | Gposteffect p | Gsource(p,_,_) -> p
+ let source = function Gprop _ | Gposteffect _ -> None | Gsource(_,s,e) -> Some(s,e)
let is_smoke_test = function
| Gprop p -> WpPropId.is_smoke_test p
- | Gposteffect _ | Geffect _ -> false
+ | Gposteffect _ | Gsource _ -> false
let pretty fmt = function
| Gprop p -> WpPropId.pretty fmt p
- | Geffect(p,s,FromCode) -> Format.fprintf fmt "%a at sid:%d" WpPropId.pretty p s.sid
- | Geffect(p,s,FromCall) -> Format.fprintf fmt "Call %a at sid:%d" WpPropId.pretty p s.sid
- | Geffect(p,s,FromReturn) -> Format.fprintf fmt "Return %a at sid:%d" WpPropId.pretty p s.sid
+ | Gsource(p,s,FromCode) -> Format.fprintf fmt "%a at sid:%d" WpPropId.pretty p s.sid
+ | Gsource(p,s,FromCall) -> Format.fprintf fmt "Call %a at sid:%d" WpPropId.pretty p s.sid
+ | Gsource(p,s,FromReturn) -> Format.fprintf fmt "Return %a at sid:%d" WpPropId.pretty p s.sid
| Gposteffect p -> Format.fprintf fmt "%a post-effect" WpPropId.pretty p
end
@@ -507,6 +507,18 @@ 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
+ (fun env wp ->
+ let outcome = Warning.catch
+ ~severe:true ~effect:"Degenerated goal"
+ (L.pred `Positive env) predicate in
+ let warn,goal = match outcome with
+ | 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
+ { wp with vcs = vcs })
+
let add_assigns wenv (gpid,ainfo) wp = in_wenv wenv wp
begin fun env wp ->
let outcome = Warning.catch
@@ -577,7 +589,7 @@ struct
in
let target = match sloc with
| None -> Gprop e.e_pid
- | Some stmt -> Geffect(e.e_pid,stmt,source)
+ | Some stmt -> Gsource(e.e_pid,stmt,source)
in
Gmap.add target group vcs
) effects vcs
@@ -593,7 +605,7 @@ struct
(fun e vcs ->
let target = match stmt with
| None -> Gprop e.e_pid
- | Some s -> Geffect(e.e_pid,s,FromCode)
+ | Some s -> Gsource(e.e_pid,s,FromCode)
in
add_vc target ?warn F.p_false vcs)
effects vcs
@@ -1026,6 +1038,52 @@ struct
) wp.vcs pre
in { wp with vcs = vcs })
+ (* -------------------------------------------------------------------------- *)
+ (* --- WP RULE : call terminates --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ let call_terminates wenv (gpid, caller_t) stmt kf es ~callee_t wp =
+ in_wenv wenv wp
+ (fun env wp ->
+ let gid = Gsource(gpid, stmt, FromCall) in
+ let outcome = Warning.catch
+ ~severe:true ~effect:"Can not prove call termination"
+ (L.pred `Positive env) caller_t
+ in
+ match outcome with
+ | Warning.Failed warn ->
+ let vcs = add_vc gid ~warn p_false wp.vcs in
+ { wp with vcs = vcs }
+ | Warning.Result(warn, caller_t) ->
+ let sigma = L.current env in
+ let outcome = Warning.catch
+ ~severe:true ~effect:"Can not prove call preconditions"
+ (List.map (C.exp sigma)) es in
+ match outcome with
+ | Warning.Failed warn2 ->
+ let warn = W.union warn warn2 in
+ let vcs = add_vc gid ~warn p_false wp.vcs in
+ { wp with vcs = vcs }
+ | Warning.Result(warn2, vs) ->
+ let warn = W.union warn warn2 in
+ let init = L.mem_at env Clabels.init in
+ let call = L.call kf vs in
+ let call_e = L.mk_env ~here:sigma () in
+ let call_f = L.call_pre init call sigma in
+ let outcome = Warning.catch
+ ~severe:true ~effect:"Can not prove call precondition"
+ (L.in_frame call_f (L.pred `Positive call_e)) callee_t in
+ match outcome with
+ | Warning.Result(warn3,callee_t) ->
+ let warn = W.union warn warn3 in
+ let goal = p_imply caller_t callee_t in
+ let vcs = add_vc gid ~warn goal wp.vcs in
+ { wp with vcs = vcs }
+ | Warning.Failed warn3 ->
+ let warn = W.union warn warn3 in
+ let vcs = add_vc gid ~warn p_false wp.vcs in
+ { wp with vcs = vcs })
+
(* -------------------------------------------------------------------------- *)
(* --- WP RULE : call postcondition --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/mcfg.ml b/src/plugins/wp/mcfg.ml
index 568b894770929317b5078add8bfb06d9979f5055..15905e4eab2aecfcec837c07a2690c903bf33cab 100644
--- a/src/plugins/wp/mcfg.ml
+++ b/src/plugins/wp/mcfg.ml
@@ -67,6 +67,8 @@ 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 ->
+ predicate -> stmt -> WpPropId.effect_source -> t_prop -> t_prop
val add_assigns : t_env -> WpPropId.assigns_info -> t_prop -> t_prop
@@ -101,6 +103,10 @@ module type S = sig
pre: WpPropId.pred_info list ->
t_prop -> t_prop
+ val call_terminates : t_env -> WpPropId.pred_info ->
+ stmt -> kernel_function -> exp list ->
+ callee_t:predicate -> t_prop -> t_prop
+
val call : t_env -> stmt ->
lval option -> kernel_function -> exp list ->
pre: WpPropId.pred_info list ->
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index c3312d5f84313af0f14bb82cdfc8351ddd311322..7d30a86199f42b9353311eee209fd5e65edcfbf8 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -44,6 +44,7 @@ type prop_kind =
| PKVarPos (** computation related to a loop variant being positive *)
| PKAFctOut (** computation related to the function assigns on normal termination *)
| PKAFctExit (** computation related to the function assigns on exit termination *)
+ | PKTerminates (** computation related to the termination *)
| PKSmoke (** expected to fail *)
| PKPre of kernel_function * stmt * Property.t
(** precondition for function
@@ -177,6 +178,9 @@ let mk_pre_id kf ki b p =
let mk_post_id kf ki b p =
mk_prop PKProp (Property.ip_of_ensures kf ki b p)
+let mk_terminates_id kf kinstr p =
+ mk_prop PKTerminates (Property.ip_of_terminates kf kinstr p)
+
let mk_stmt_post_id kf s b p =
mk_prop PKProp (Property.ip_of_ensures kf (Kstmt s) b p)
@@ -214,6 +218,7 @@ let kind_order = function
| PKCheck -> 9
| PKTactic -> 10
| PKSmoke -> 11
+ | PKTerminates -> 12
let compare_kind k1 k2 = match k1, k2 with
PKPre (kf1, ki1, p1), PKPre (kf2, ki2, p2) ->
@@ -328,7 +333,7 @@ end = struct
let basename_of_prop_id p =
match p.p_kind , p.p_prop with
- | (PKTactic | PKCheck | PKProp | PKPropLoop | PKSmoke) , p ->
+ | (PKTactic | PKCheck | PKProp | PKPropLoop | PKSmoke | PKTerminates) , p ->
base_id_prop_txt p
| PKEstablished , p -> base_id_prop_txt p ^ "_established"
| PKPreserved , p -> base_id_prop_txt p ^ "_preserved"
@@ -411,7 +416,8 @@ struct
let get_prop_id_base p =
match p.p_kind , p.p_prop with
- | (PKTactic | PKCheck | PKProp | PKPropLoop | PKSmoke) , p -> get_ip p
+ | (PKTactic | PKCheck | PKProp | PKPropLoop | PKSmoke | PKTerminates) , p ->
+ get_ip p
| PKEstablished , p -> get_ip p ^ "_established"
| PKPreserved , p -> get_ip p ^ "_preserved"
| PKVarDecr , p -> get_ip p ^ "_decrease"
@@ -563,6 +569,7 @@ let label_of_kind = function
| PKVarPos -> "Positive"
| PKAFctOut -> "Function assigns"
| PKAFctExit -> "Exit assigns"
+ | PKTerminates -> "Terminates"
| PKPre(kf,_,_) ->
Printf.sprintf "Precondition for '%s'" (Kernel_function.get_name kf)
@@ -579,7 +586,7 @@ struct
| None -> ()
| Some(k,n) -> fprintf fmt " (%d/%d)" (succ k) n
let pp_subprop fmt p = match p.p_kind with
- | PKProp | PKTactic | PKCheck | PKPropLoop | PKSmoke -> ()
+ | PKProp | PKTactic | PKCheck | PKPropLoop | PKSmoke | PKTerminates -> ()
| PKEstablished -> pp_print_string fmt " (established)"
| PKPreserved -> pp_print_string fmt " (preserved)"
| PKVarDecr -> pp_print_string fmt " (decrease)"
@@ -657,6 +664,7 @@ let propid_hints hs p =
| PKVarPos , _ -> add_required hs "positive"
| PKAFctOut , _ -> add_required hs "return"
| PKAFctExit , _ -> add_required hs "exit"
+ | PKTerminates , _ -> add_required hs "terminates"
| PKPre(kf,st,_) , _ ->
add_required hs ("precond-" ^ Kernel_function.get_name kf) ;
stmt_hints hs st
@@ -731,7 +739,7 @@ let prop_id_keys p =
let pp_goal_kind fmt = function
| PKTactic | PKSmoke | PKCheck
- | PKProp | PKPropLoop | PKAFctOut | PKAFctExit
+ | PKProp | PKPropLoop | PKAFctOut | PKAFctExit | PKTerminates
| PKPre _ -> ()
| PKEstablished -> Format.pp_print_string fmt "Establishment of "
| PKPreserved -> Format.pp_print_string fmt "Preservation of "
@@ -1040,14 +1048,15 @@ let split_map f pid gs =
let subproofs id = match id.p_kind with
| PKCheck -> 0
- | PKProp | PKSmoke | PKTactic | PKPre _ | PKPropLoop -> 1
+ | PKProp | PKSmoke | PKTactic | PKPre _ | PKPropLoop | PKTerminates -> 1
| PKEstablished | PKPreserved
| PKVarDecr | PKVarPos
| PKAFctExit | PKAFctOut -> 2
let subproof_idx id = match id.p_kind with
| PKCheck -> (-1) (* 0/0 *)
- | PKProp | PKTactic | PKPre _ | PKSmoke | PKPropLoop -> 0 (* 1/1 *)
+ | PKProp | PKTactic | PKPre _ | PKSmoke | PKPropLoop
+ | PKTerminates -> 0 (* 1/1 *)
| PKPreserved -> 0 (* 1/2 *)
| PKEstablished-> 1 (* 2/2 *)
| PKVarDecr -> 0 (* 1/2 *)
@@ -1097,7 +1106,8 @@ let get_induction p =
| IPAssigns {ias_kf; ias_kinstr=Kstmt stmt} -> Some (ias_kf, stmt)
| _ -> None
in match p.p_kind with
- | PKCheck|PKSmoke |PKAFctOut|PKAFctExit|PKPre _ | PKTactic -> None
+ | PKCheck|PKSmoke |PKAFctOut|PKAFctExit|PKPre _ | PKTactic| PKTerminates ->
+ None
| PKProp ->
let loop_stmt_opt = match get_stmt (property_of_id p) with
| None -> None
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 20ba4ab98d8f7742b304325fe97835e4e2273322..643b69d72d03055c3323e9dda7e53b95be818221 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -100,6 +100,7 @@ type prop_kind =
| PKVarPos (** computation related to a loop variant being positive *)
| PKAFctOut (** computation related to the function assigns on normal termination *)
| PKAFctExit (** computation related to the function assigns on exit termination *)
+ | PKTerminates (** computation related to the termination *)
| PKSmoke (** smoke property *)
| PKPre of kernel_function * stmt * Property.t (** precondition for function
at stmt, property of the require. Many information that should come
@@ -196,6 +197,9 @@ val mk_pre_id : kernel_function -> kinstr -> funbehavior ->
val mk_post_id : kernel_function -> kinstr -> funbehavior ->
termination_kind * identified_predicate -> prop_id
+val mk_terminates_id :
+ kernel_function -> kinstr -> identified_predicate -> prop_id
+
val mk_stmt_post_id : kernel_function -> stmt -> funbehavior ->
termination_kind * identified_predicate -> prop_id