CfgAnnot (frama-c-wp.Wp.CfgAnnot)

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 ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.funbehavior ->
  WpPropId.pred_info list

val get_preconditions : 
  goal:bool ->
  Frama_c_kernel.Cil_types.kernel_function ->
  WpPropId.pred_info list

val get_behavior_goals : 
  Frama_c_kernel.Cil_types.kernel_function ->
  ?smoking:bool ->
  ?exits:bool ->
  Frama_c_kernel.Cil_types.funbehavior ->
  behavior

val get_complete_behaviors : 
  Frama_c_kernel.Cil_types.kernel_function ->
  WpPropId.pred_info list

val get_disjoint_behaviors : 
  Frama_c_kernel.Cil_types.kernel_function ->
  WpPropId.pred_info list

val get_terminates_goal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  WpPropId.pred_info option

val get_decreases_goal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  WpPropId.variant_info option

type code_assertion = {

code_admitted : WpPropId.pred_info option;

code_verified : WpPropId.pred_info option;

}

val get_code_assertions : 
  ?smoking:bool ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  code_assertion list

val get_unreachable : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  WpPropId.prop_id

val get_stmt_assigns : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  WpPropId.assigns_full_info list

type loop_hypothesis =

| NoHyp

| Check of WpPropId.prop_id

| Always of WpPropId.prop_id

type loop_invariant = {

loop_hyp : loop_hypothesis;

loop_est : WpPropId.prop_id option;

loop_ind : WpPropId.prop_id option;

loop_pred : Frama_c_kernel.Cil_types.predicate;

}

type loop_contract = {

`loop_terminates : Frama_c_kernel.Cil_types.predicate option;`
`loop_invariants : loop_invariant list;`	(* to be proved after loop invariants *)
`loop_smoke : WpPropId.pred_info list;`	(* assigned by loop body *)
`loop_assigns : WpPropId.assigns_full_info list;`

}

val get_loop_contract : 
  ?smoking:bool ->
  ?terminates:Frama_c_kernel.Cil_types.predicate ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  loop_contract

val mk_variant_properties : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.code_annotation ->
  Frama_c_kernel.Cil_types.term ->
  WpPropId.pred_info * WpPropId.pred_info

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 : Frama_c_kernel.Cil_types.assigns;

contract_terminates : bool * Frama_c_kernel.Cil_types.predicate;

contract_decreases : Frama_c_kernel.Cil_types.variant option;

}

val get_call_contract : 
  ?smoking:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  contract

val clear : unit -> unit