sig
type state
type states
val create :
Transfer_logic.S.state ->
Cil_types.kernel_function -> Transfer_logic.ActiveBehaviors.t
val create_from_spec :
Transfer_logic.S.state ->
Cil_types.spec -> Transfer_logic.ActiveBehaviors.t
val check_fct_preconditions_for_behavior :
Cil_types.kernel_function ->
Transfer_logic.ActiveBehaviors.t ->
per_behavior:bool ->
Cil_types.kinstr ->
Transfer_logic.S.states -> Cil_types.behavior -> Transfer_logic.S.states
val check_fct_preconditions :
Cil_types.kernel_function ->
Transfer_logic.ActiveBehaviors.t ->
Cil_types.kinstr ->
Transfer_logic.S.state -> Transfer_logic.S.states Eval.or_bottom
val check_fct_postconditions_for_behaviors :
Cil_types.kernel_function ->
Transfer_logic.ActiveBehaviors.t ->
Cil_types.behavior list ->
Cil_types.termination_kind ->
per_behavior:bool ->
pre_state:Transfer_logic.S.state ->
post_states:Transfer_logic.S.states ->
result:Cil_types.varinfo option -> Transfer_logic.S.states
val check_fct_postconditions :
Cil_types.kernel_function ->
Transfer_logic.ActiveBehaviors.t ->
Cil_types.termination_kind ->
pre_state:Transfer_logic.S.state ->
post_states:Transfer_logic.S.states ->
result:Cil_types.varinfo option -> Transfer_logic.S.states Eval.or_bottom
val reduce_by_assumes_of_behavior :
Cil_types.kernel_function ->
Cil_types.behavior -> Transfer_logic.S.states -> Transfer_logic.S.states
val interp_annot :
limit:int ->
record:bool ->
Cil_types.kernel_function ->
Transfer_logic.ActiveBehaviors.t ->
Cil_types.stmt ->
Cil_types.code_annotation ->
initial_state:Transfer_logic.S.state ->
Transfer_logic.S.states -> Transfer_logic.S.states
end