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 : ('a, 'b, 'c) Cil_types.spec -> 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_assigns : Kernel_function.t ->
ActiveBehaviors.t ->
pre_state:Cvalue.Model.t -> Function_Froms.froms -> unit
val verify_assigns_from : Kernel_function.t -> pre:Cvalue.Model.t -> Function_Froms.froms -> unit
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 code_annotation_text : Cil_types.code_annotation -> string
val code_annotation_source : Cil_datatype.Code_annotation.t -> Lexing.position
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
val eval_by_callstack : Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.predicate Cil_types.named -> Eval_terms.predicate_status
val mark_green_and_red : unit -> unit