sig
module Make :
functor
(Abstract : Abstractions.Eva) (Transfer : sig
type state = Abstract.Dom.t
type value
type location
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 ->
state list Eval.or_bottom *
Value_types.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 :
state list
Eval.or_bottom;
cacheable :
Value_types.cacheable;
builtin : bool;
}
val compute_call_ref :
(Cil_types.stmt ->
(location, value)
Eval.call ->
state -> call_result)
ref
end) (Kf : sig
val kf :
Cil_types.kernel_function
end) ->
sig
type state = Abstract.Dom.t
type store
type tank
type flow
type widening
val empty_store :
stmt:Cil_types.stmt option -> Trace_partitioning.Make.store
val empty_flow : Trace_partitioning.Make.flow
val empty_tank : unit -> Trace_partitioning.Make.tank
val empty_widening :
stmt:Cil_types.stmt option -> Trace_partitioning.Make.widening
val initial_tank :
Trace_partitioning.Make.state list -> Trace_partitioning.Make.tank
val pretty_store :
Stdlib.Format.formatter -> Trace_partitioning.Make.store -> unit
val pretty_flow :
Stdlib.Format.formatter -> Trace_partitioning.Make.flow -> unit
val expanded :
Trace_partitioning.Make.store -> Trace_partitioning.Make.state list
val smashed :
Trace_partitioning.Make.store ->
Trace_partitioning.Make.state Bottom.Type.or_bottom
val contents :
Trace_partitioning.Make.flow -> Trace_partitioning.Make.state list
val is_empty_store : Trace_partitioning.Make.store -> bool
val is_empty_flow : Trace_partitioning.Make.flow -> bool
val is_empty_tank : Trace_partitioning.Make.tank -> bool
val store_size : Trace_partitioning.Make.store -> int
val flow_size : Trace_partitioning.Make.flow -> int
val tank_size : Trace_partitioning.Make.tank -> int
val reset_store : Trace_partitioning.Make.store -> unit
val reset_tank : Trace_partitioning.Make.tank -> unit
val reset_widening : Trace_partitioning.Make.widening -> unit
val reset_widening_counter : Trace_partitioning.Make.widening -> unit
val enter_loop :
Trace_partitioning.Make.flow ->
Cil_types.stmt -> Trace_partitioning.Make.flow
val leave_loop :
Trace_partitioning.Make.flow ->
Cil_types.stmt -> Trace_partitioning.Make.flow
val next_loop_iteration :
Trace_partitioning.Make.flow ->
Cil_types.stmt -> Trace_partitioning.Make.flow
val split_return :
Trace_partitioning.Make.flow ->
Cil_types.exp option -> Trace_partitioning.Make.flow
val drain :
Trace_partitioning.Make.tank -> Trace_partitioning.Make.flow
val fill :
into:Trace_partitioning.Make.tank ->
Trace_partitioning.Make.flow -> unit
val transfer :
(Trace_partitioning.Make.state ->
Trace_partitioning.Make.state list) ->
Trace_partitioning.Make.flow -> Trace_partitioning.Make.flow
val join :
(Partition.branch * Trace_partitioning.Make.flow) list ->
Trace_partitioning.Make.store -> Trace_partitioning.Make.flow
val widen :
Trace_partitioning.Make.widening ->
Trace_partitioning.Make.flow -> Trace_partitioning.Make.flow
end
end