sig
val signal_abort : unit -> unit
module Computer :
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 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
type return = Domain.return
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 return :
with_alarms:CilE.warn_mode ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval option ->
state -> (state, return, value) Eval.return_state Eval.or_bottom
val enter_loop : Cil_types.stmt -> state -> state
val incr_loop_counter : Cil_types.stmt -> state -> state
val leave_loop : Cil_types.stmt -> state -> state
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 ->
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 res =
(state, return, value) Eval.call_result * Value_types.cacheable
val compute_call_ref :
(Cil_types.kinstr -> value Eval.call -> state -> res) ref
end) (Logic : sig
type state = Domain.t
type states = States.t
type active_behaviors
val create :
state ->
Cil_types.kernel_function -> active_behaviors
val check_fct_preconditions :
Cil_types.kernel_function ->
active_behaviors ->
Cil_types.kinstr -> state -> states Eval.or_bottom
val check_fct_postconditions :
Cil_types.kernel_function ->
active_behaviors ->
Cil_types.termination_kind ->
init_state:state ->
post_states:states ->
result:Cil_types.varinfo option ->
states Eval.or_bottom
val interp_annot :
limit:int ->
record:bool ->
Cil_types.kernel_function ->
active_behaviors ->
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, Domain.return, Domain.value) Eval.call_result *
Value_types.cacheable
end
end