functor (Abstract : Abstractions.Eva)
(States : sig
type state = Abstract.Dom.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)
(Transfer : sig
type state = Abstract.Dom.t
type value = Abstract.Val.t
type loc
val assign :
state ->
Cil_types.kinstr ->
Cil_types.lval -> Cil_types.exp -> state Eval.or_bottom
val assume :
state ->
Cil_types.stmt ->
Cil_types.exp -> bool -> state Eval.or_bottom
val call :
Cil_types.stmt ->
Cil_types.lval option ->
Cil_types.exp ->
Cil_types.exp list ->
state -> (Partition.key * state) list * Eval.cacheable
val check_unspecified_sequence :
Cil_types.stmt ->
state ->
(Cil_types.stmt * Cil_types.lval list *
Cil_types.lval list * Cil_types.lval list *
Cil_types.stmt ref list)
list -> unit Eval.or_bottom
val enter_scope :
Cil_types.kernel_function ->
Cil_types.varinfo list -> state -> state
type call_result = {
states : (Partition.key * state) list;
cacheable : Eval.cacheable;
builtin : bool;
}
val compute_call_ref :
(Cil_types.stmt ->
(loc, value) Eval.call ->
Eval.recursion option -> state -> call_result)
ref
end)
(Init : sig
val initial_state :
lib_entry:bool -> Abstract.Dom.t Bottom.Type.or_bottom
val initial_state_with_formals :
lib_entry:bool ->
Cil_types.kernel_function ->
Abstract.Dom.t Bottom.Type.or_bottom
val initialize_local_variable :
Cil_types.stmt ->
Cil_types.varinfo ->
Cil_types.init ->
Abstract.Dom.t -> Abstract.Dom.t Bottom.Type.or_bottom
end)
(Logic : sig
type state = Abstract.Dom.t
type states = States.t
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_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 ->
Transfer_logic.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 ->
Transfer_logic.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 ->
Transfer_logic.ActiveBehaviors.t ->
Cil_types.stmt ->
Cil_types.code_annotation ->
initial_state:state -> states -> states
end)
(Spec : sig
val treat_statement_assigns :
Cil_types.assigns -> Abstract.Dom.t -> Abstract.Dom.t
end)
->
sig
val compute :
Cil_types.kernel_function ->
Cil_types.kinstr ->
Abstract.Dom.t ->
(Partition.key * Abstract.Dom.t) list * Eval.cacheable
end