sig
module ActiveBehaviors :
sig
type t
val is_active :
Transfer_logic.ActiveBehaviors.t ->
Cil_types.behavior -> Alarmset.status
val active_behaviors :
Transfer_logic.ActiveBehaviors.t -> Cil_types.behavior list
val create :
(Cil_types.predicate -> Alarmset.status) ->
Cil_types.spec -> Transfer_logic.ActiveBehaviors.t
end
val process_inactive_behaviors :
Cil_types.kinstr ->
Cil_types.kernel_function -> Cil_types.behavior list -> unit
module type S =
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_behaviors :
Cil_types.kinstr ->
Cil_types.kernel_function ->
Cil_types.behavior list ->
Alarmset.status -> Transfer_logic.S.states -> Transfer_logic.S.states
val check_fct_preconditions :
Cil_types.kinstr ->
Cil_types.kernel_function ->
Transfer_logic.ActiveBehaviors.t ->
Transfer_logic.S.state -> Transfer_logic.S.states Eval.or_bottom
val check_fct_postconditions_for_behaviors :
Cil_types.kernel_function ->
Cil_types.behavior list ->
Alarmset.status ->
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 evaluate_assumes_of_behavior :
Transfer_logic.S.state -> Cil_types.behavior -> Alarmset.status
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
module type LogicDomain =
sig
type t
val top : Transfer_logic.LogicDomain.t
val equal :
Transfer_logic.LogicDomain.t -> Transfer_logic.LogicDomain.t -> bool
val evaluate_predicate :
Transfer_logic.LogicDomain.t Abstract_domain.logic_environment ->
Transfer_logic.LogicDomain.t ->
Cil_types.predicate -> Alarmset.status
val reduce_by_predicate :
Transfer_logic.LogicDomain.t Abstract_domain.logic_environment ->
Transfer_logic.LogicDomain.t ->
Cil_types.predicate ->
bool -> Transfer_logic.LogicDomain.t Eval.or_bottom
end
module Make :
functor
(Domain : LogicDomain) (States : sig
type state = Domain.t
type t
val empty : t
val is_empty : t -> bool
val singleton : state -> t
val singleton' :
state Eval.or_bottom -> t
val uncheck_add : state -> t -> t
val add : state -> t -> t
val add' :
state Eval.or_bottom -> t -> t
val length : t -> int
val merge : into:t -> t -> t * bool
val join :
?into:state Eval.or_bottom ->
t -> state Eval.or_bottom
val fold :
(state -> 'a -> 'a) ->
t -> 'a -> 'a
val iter :
(state -> unit) -> t -> unit
val map : (state -> state) -> t -> t
val map_or_bottom :
(state -> state Eval.or_bottom) ->
t -> t
val reorder : t -> t
val of_list : state list -> t
val to_list : t -> state list
val pretty :
Format.formatter -> t -> unit
end) ->
sig
type state = Domain.t
type states = States.t
val create : state -> Cil_types.kernel_function -> ActiveBehaviors.t
val create_from_spec : state -> Cil_types.spec -> ActiveBehaviors.t
val check_fct_preconditions_for_behaviors :
Cil_types.kinstr ->
Cil_types.kernel_function ->
Cil_types.behavior list -> Alarmset.status -> states -> states
val check_fct_preconditions :
Cil_types.kinstr ->
Cil_types.kernel_function ->
ActiveBehaviors.t -> state -> states Eval.or_bottom
val check_fct_postconditions_for_behaviors :
Cil_types.kernel_function ->
Cil_types.behavior list ->
Alarmset.status ->
pre_state:state ->
post_states:states -> result:Cil_types.varinfo option -> states
val check_fct_postconditions :
Cil_types.kernel_function ->
ActiveBehaviors.t ->
Cil_types.termination_kind ->
pre_state:state ->
post_states:states ->
result:Cil_types.varinfo option -> states Eval.or_bottom
val evaluate_assumes_of_behavior :
state -> Cil_types.behavior -> Alarmset.status
val interp_annot :
limit:int ->
record:bool ->
Cil_types.kernel_function ->
ActiveBehaviors.t ->
Cil_types.stmt ->
Cil_types.code_annotation ->
initial_state:state -> states -> states
end
end