module Make: functor (
Domain
:
Domain
) ->
functor (
States
:
Powerset.S
with type state = Domain.t
) ->
S
with type state = Domain.t
and type states = States.t
type
state
type
states
val create : state ->
Cil_types.kernel_function -> Transfer_logic.ActiveBehaviors.t
val create_from_spec : 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 ->
states -> Cil_types.behavior -> states
val check_fct_preconditions : Cil_types.kernel_function ->
Transfer_logic.ActiveBehaviors.t ->
Cil_types.kinstr ->
state -> 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:state ->
post_states:states ->
result:Cil_types.varinfo option -> states
val check_fct_postconditions : Cil_types.kernel_function ->
Transfer_logic.ActiveBehaviors.t ->
Cil_types.termination_kind ->
pre_state:state ->
post_states:states ->
result:Cil_types.varinfo option -> states Eval.or_bottom
val reduce_by_assumes_of_behavior : Cil_types.kernel_function ->
Cil_types.behavior -> states -> 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:state ->
states -> states