module Split_return: sig
.. end
This module is used to merge together the final states of a function
according to a given strategy. Default is to merge all states together
module ReturnUsage: sig
.. end
module AutoStrategy: State_builder.Option_ref
(
ReturnUsage.RUDatatype
)
(
sig
val name : string
val dependencies : State.t list
end
)
module KfStrategy: Kernel_function.Make_Table
(
Split_strategy
)
(
sig
val size : int
val dependencies : State.t list
val name : string
end
)
val strategy : KfStrategy.key -> KfStrategy.data
val default : State_set.t -> Cvalue.Model.t list
val split_eq_aux : Kernel_function.t ->
Cil_types.lval ->
Abstract_interp.Int.t ->
Cvalue.Model.t list -> Cvalue.Model.t * Cvalue.Model.t list
val split_eq_multiple : Kernel_function.t ->
Cil_types.lval ->
Abstract_interp.Int.t list -> State_set.t -> Cvalue.Model.t list
val join_final_states : Kernel_function.t ->
return_lv:(Cil_types.lhost * Cil_types.offset) option ->
State_set.t -> Cvalue.Model.t list
Join the given state_set. The strategy is defined according to
the name of the function.