Module Eval_annots

module Eval_annots: sig .. end
Check the postcondition of kf for a given behavior b. This may result in splitting post_states if the postconditions contain disjunctions.

val emit_status : Property.t -> Property_status.emitted_status -> unit
val msg_status : Eval_terms.predicate_status ->
?current:bool ->
?once:bool ->
?source:Lexing.position ->
('a, Format.formatter, unit) Pervasives.format -> 'a
module ActiveBehaviors: sig .. end
val has_requires : 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 -> Cil_types.behavior -> unit
type postcondition_kf_kind = 
| PostLeaf
| PostBody
| PostUseSpec
type p_kind = 
| Precondition
| Postcondition of postcondition_kf_kind
| Assumes
val pp_p_kind : Format.formatter -> p_kind -> unit
val post_kind : Kernel_function.t -> postcondition_kf_kind
val ip_from_precondition : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior -> Cil_types.identified_predicate -> Property.t
val emit_message_and_status : Kernel_function.t ->
Cil_types.behavior ->
bool ->
Property.t ->
p_kind ->
Eval_terms.predicate_status ->
Cil_types.identified_predicate ->
Cil_types.predicate -> source:Lexing.position -> unit
val process_inactive_behavior : Kernel_function.t -> Cil_types.kinstr -> Cil_types.funbehavior -> unit
val process_inactive_behaviors : Kernel_function.t ->
Cil_types.kinstr -> ActiveBehaviors.t -> unit
val process_inactive_postconds : Kernel_function.t -> Cil_types.funbehavior list -> unit
val warn_inactive : Kernel_function.t ->
Cil_types.behavior ->
p_kind -> Cil_types.identified_predicate -> unit
val refine_active : ActiveBehaviors.t ->
Cil_types.funbehavior -> per_behavior:bool -> bool option
val eval_and_reduce_p_kind : Kernel_function.t ->
Cil_types.behavior ->
active:bool ->
p_kind ->
Cil_types.identified_predicate list ->
(Cil_types.identified_predicate -> Property.t) ->
(Cvalue.Model.t -> Eval_terms.eval_env) -> State_set.t -> State_set.t
val check_fct_postconditions_of_behavior : Kernel_function.t ->
ActiveBehaviors.t ->
Cil_types.funbehavior ->
Cil_types.termination_kind ->
per_behavior:bool ->
result:Cil_types.varinfo option ->
pre_state:Cvalue.Model.t -> post_states:State_set.t -> State_set.t
Check the postcondition of kf for a given behavior b. This may result in splitting post_states if the postconditions contain disjunctions.
val check_fct_postconditions_default_behavior : Kernel_function.t ->
ActiveBehaviors.t ->
Cil_types.termination_kind ->
result:Cil_types.varinfo option ->
pre_state:Cvalue.Model.t -> post_states:State_set.t -> State_set.t
val check_fct_postconditions_for_behavior : Kernel_function.t ->
ActiveBehaviors.t ->
Cil_types.funbehavior ->
Cil_types.termination_kind ->
result:Cil_types.varinfo option ->
per_behavior:bool -> pre_state:Cvalue.Model.t -> State_set.t -> State_set.t
Checks the postconditions of b and of the default behavior if it is not b
val check_fct_postconditions : Kernel_function.t ->
ActiveBehaviors.t ->
Cil_types.funbehavior list ->
Cil_types.termination_kind ->
result:Cil_types.varinfo option ->
per_behavior:bool -> pre_state:Cvalue.Model.t -> State_set.t -> State_set.t
Check the postcondition of kf for every behavior, treating them separately if per_behavior is true, merging them otherwise. The postcondition of the global behavior is applied for each behavior, to help reduce the final state. The default behavior is done once, at the end.
val eval_assigns_from : Cvalue.Model.t -> Cil_types.identified_term -> Locations.Zone.t
val check_from : Cvalue.Model.t ->
Cil_types.identified_term ->
Locations.Zone.t ->
Cil_types.identified_term list ->
Function_Froms.froms -> string * Eval_terms.predicate_status
Compute the validity status for from in pre_state, assuming the entire clause is assigns asgn \from from. The inferred dependencies are found_froms, while asgn evaluates to assigns_zone.
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_for_behavior : Kernel_function.t ->
ActiveBehaviors.t ->
per_behavior:bool ->
Cil_types.kinstr -> State_set.t -> Cil_types.funbehavior -> State_set.t
Check the precondition of kf for a given behavior b. This may result in splitting states if the precondition contains disjunctions.
val check_fct_preconditions : Kernel_function.t ->
ActiveBehaviors.t ->
Cil_types.kinstr -> Cvalue.Model.t -> State_set.t
val code_annotation_text : Cil_types.code_annotation -> string
val code_annotation_loc : Cil_datatype.Code_annotation.t -> Cil_datatype.Stmt.t -> Cil_types.location
val interp_annot : Cil_types.kernel_function ->
ActiveBehaviors.t ->
Cvalue.Model.t ->
int ->
State_set.t ->
Cil_datatype.Stmt.t -> Cil_datatype.Code_annotation.t -> bool -> State_set.t
val mark_unreachable : unit -> unit
val mark_rte : unit -> unit
val c_labels : Kernel_function.t ->
Value_types.Callstack.Hashtbl.key ->
Db.Value.state Cil_datatype.Logic_label.Map.t
val eval_by_callstack : Kernel_function.t ->
Cil_types.stmt -> Cil_types.predicate -> Eval_terms.predicate_status
class contains_c_at : object .. end
val contains_c_at : Cil_types.code_annotation -> bool
val mark_green_and_red : unit -> unit
val mark_invalid_initializers : unit -> unit