sig
type behavior = {
bhv_assumes : WpPropId.pred_info list;
bhv_requires : WpPropId.pred_info list;
bhv_smokes : WpPropId.pred_info list;
bhv_ensures : WpPropId.pred_info list;
bhv_exits : WpPropId.pred_info list;
bhv_post_assigns : WpPropId.assigns_full_info;
bhv_exit_assigns : WpPropId.assigns_full_info;
}
val get_requires :
goal:bool ->
Cil_types.kernel_function ->
Cil_types.funbehavior -> WpPropId.pred_info list
val get_preconditions :
goal:bool -> Cil_types.kernel_function -> WpPropId.pred_info list
val get_behavior_goals :
Cil_types.kernel_function ->
?smoking:bool ->
?exits:bool -> Cil_types.funbehavior -> CfgAnnot.behavior
val get_complete_behaviors :
Cil_types.kernel_function -> WpPropId.pred_info list
val get_disjoint_behaviors :
Cil_types.kernel_function -> WpPropId.pred_info list
val get_terminates_goal :
Cil_types.kernel_function -> WpPropId.pred_info option
val get_decreases_goal :
Cil_types.kernel_function -> WpPropId.variant_info option
type code_assertions = {
code_admitted : WpPropId.pred_info list;
code_verified : WpPropId.pred_info list;
}
val get_code_assertions :
?smoking:bool ->
Cil_types.kernel_function -> Cil_types.stmt -> CfgAnnot.code_assertions
val get_unreachable :
Cil_types.kernel_function -> Cil_types.stmt -> WpPropId.prop_id
val get_stmt_assigns :
Cil_types.kernel_function ->
Cil_types.stmt -> WpPropId.assigns_full_info list
type loop_contract = {
loop_terminates : Cil_types.predicate option;
loop_established : WpPropId.pred_info list;
loop_invariants : WpPropId.pred_info list;
loop_smoke : WpPropId.pred_info list;
loop_preserved : WpPropId.pred_info list;
loop_assigns : WpPropId.assigns_full_info list;
}
val get_loop_contract :
?smoking:bool ->
?terminates:Cil_types.predicate ->
Cil_types.kernel_function -> Cil_types.stmt -> CfgAnnot.loop_contract
type contract = {
contract_cond : WpPropId.pred_info list;
contract_hpre : WpPropId.pred_info list;
contract_post : WpPropId.pred_info list;
contract_exit : WpPropId.pred_info list;
contract_smoke : WpPropId.pred_info list;
contract_assigns : Cil_types.assigns;
contract_terminates : bool * Cil_types.predicate;
}
val get_call_contract :
?smoking:Cil_types.stmt ->
Cil_types.kernel_function -> Cil_types.stmt -> CfgAnnot.contract
val clear : unit -> unit
end