Module Eval_annots

module Eval_annots: sig .. end
Statuses for code annotations and function contracts


Statuses for code annotations and function contracts
val emit_status : Property.t -> Property_status.emitted_status -> unit
val notify_status : Property.t ->
Property_status.emitted_status ->
'a -> Value_messages.Value_Message_Callback.result
module ActiveBehaviors: sig .. end
val has_requires : Cil_types.kernel_function -> bool
val conv_status : Eval_terms.predicate_status -> Property_status.emitted_status
val behavior_inactive : Format.formatter -> unit
val pp_header : Kernel_function.t -> Format.formatter -> ('a, 'b) Cil_types.behavior -> unit
type postcondition_kf_kind = 
| PostLeaf
| PostBody
| PostUseSpec
type pre_post_kind = 
| Precondition
| Postcondition of postcondition_kf_kind
val pp_pre_post_kind : Format.formatter -> pre_post_kind -> unit
val post_kind : Kernel_function.t -> postcondition_kf_kind
val eval_and_reduce_pre_post : Kernel_function.t ->
ActiveBehaviors.t ->
Cil_types.funbehavior ->
pre_post_kind ->
Cil_types.identified_predicate list ->
State_set.t ->
(Cil_types.identified_predicate -> Property.t) ->
(Cvalue.Model.t -> Eval_terms.eval_env) -> State_set.t
val check_fct_postconditions : Kernel_function.t ->
ActiveBehaviors.t ->
result:Cil_types.varinfo option ->
init_state:Cvalue.Model.t ->
post_states:State_set.t -> Cil_types.termination_kind -> State_set.t
val check_fct_preconditions : Kernel_function.t ->
ActiveBehaviors.t ->
Cil_types.kinstr -> Cvalue.Model.t -> State_set.t
Check the precondition of kf. This may result in splitting init_state into multiple states if the precondition contains disjunctions.
val interp_annot : Cil_types.kernel_function ->
ActiveBehaviors.t ->
Cvalue.Model.t ->
int ->
State_set.t ->
Cil_types.stmt -> Cil_datatype.Code_annotation.t -> bool -> State_set.t
val mark_unreachable : unit -> unit
val mark_rte : unit -> unit