module CfgAnnot:sig
..end
Normalization of Annotations.
Labels are renamed wrt NormAtLabels and reorganized for use/prove
dispatching in CfgCalculus
.
type
behavior = {
|
bhv_assumes : |
|
bhv_requires : |
|
bhv_smokes : |
|
bhv_ensures : |
|
bhv_exits : |
|
bhv_post_assigns : |
|
bhv_exit_assigns : |
}
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 -> 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
type
code_assertions = {
|
code_admitted : |
|
code_verified : |
}
val get_code_assertions : ?smoking:bool ->
Cil_types.kernel_function -> Cil_types.stmt -> 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_established : |
(* | to be assumed for loop current | *) |
|
loop_invariants : |
(* | to be proved after loop invariants | *) |
|
loop_smoke : |
(* | to be verified after loop body | *) |
|
loop_preserved : |
(* | assigned by loop body | *) |
|
loop_assigns : |
}
val get_loop_contract : ?smoking:bool ->
Cil_types.kernel_function -> Cil_types.stmt -> loop_contract
type
contract = {
|
contract_cond : |
|
contract_hpre : |
|
contract_post : |
|
contract_exit : |
|
contract_smoke : |
|
contract_assigns : |
}
val get_call_contract : ?smoking:Cil_types.stmt ->
Cil_types.kernel_function -> Cil_types.stmt -> contract
val clear : unit -> unit