functor
(Domain : Abstract_domain.External) (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) (Transfer : sig
type state =
Domain.t
type value =
Domain.value
val init :
with_alarms:
CilE.warn_mode ->
state ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.varinfo ->
Cil_types.init ->
state
Eval.or_bottom
val assign :
with_alarms:
CilE.warn_mode ->
state ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval ->
Cil_types.exp ->
state
Eval.or_bottom
val assume :
with_alarms:
CilE.warn_mode ->
state ->
Cil_types.stmt ->
Cil_types.exp ->
bool ->
state
Eval.or_bottom
val call :
with_alarms:
CilE.warn_mode ->
Cil_types.stmt ->
Cil_types.lval
option ->
Cil_types.exp ->
Cil_types.exp
list ->
state ->
state
list
Eval.or_bottom *
Value_types.cacheable
val split_final_states :
Cil_types.kernel_function ->
Cil_types.exp ->
Integer.t
list ->
state
list ->
state
list list
val check_unspecified_sequence :
with_alarms:
CilE.warn_mode ->
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
type call_result = {
states :
state
list
Eval.or_bottom;
cacheable :
Value_types.cacheable;
}
val compute_call_ref :
(Cil_types.kinstr ->
value
Eval.call ->
state ->
call_result)
ref
end) (Logic :
sig
type state = Domain.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_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
end) ->
sig
val compute :
Cil_types.kernel_function ->
Cil_types.kinstr ->
Domain.t -> Domain.t list Eval.or_bottom * Value_types.cacheable
end