Module CfgAnnot

module CfgAnnot: sig .. end

Normalization of Annotations.

Labels are renamed wrt NormAtLabels and reorganized for use/prove dispatching in CfgCalculus.

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 -> 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 : WpPropId.pred_info list;
   code_verified : WpPropId.pred_info list;
}
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 : WpPropId.pred_info list; (*

to be assumed for loop current

*)
   loop_invariants : WpPropId.pred_info list; (*

to be proved after loop invariants

*)
   loop_smoke : WpPropId.pred_info list; (*

to be verified after loop body

*)
   loop_preserved : WpPropId.pred_info list; (*

assigned by loop body

*)
   loop_assigns : WpPropId.assigns_full_info list;
}
val get_loop_contract : ?smoking:bool ->
Cil_types.kernel_function -> Cil_types.stmt -> 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;
}
val get_call_contract : ?smoking:Cil_types.stmt ->
Cil_types.kernel_function -> Cil_types.stmt -> contract
val clear : unit -> unit