sig
val topologic_propagation : unit -> unit
val select_pdg_nodes :
Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
PdgTypes.Node.t list ->
Cil_types.kernel_function -> Db.Slicing.Select.set
val select_stmt :
Db.Slicing.Select.set ->
spare:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.set
val select_func_calls_to :
Db.Slicing.Select.set ->
spare:bool -> Kernel_function.t -> Db.Slicing.Select.set
val select_func_calls_into :
Db.Slicing.Select.set ->
spare:bool -> Kernel_function.t -> Db.Slicing.Select.set
val select_func_zone :
Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Locations.Zone.t -> Cil_types.kernel_function -> Db.Slicing.Select.set
val select_func_return :
Db.Slicing.Select.set ->
spare:bool -> Kernel_function.t -> Db.Slicing.Select.set
val select_stmt_ctrl :
Db.Slicing.Select.set ->
spare:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.set
val select_stmt_zone :
Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Locations.Zone.t ->
before:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.set
val select_stmt_lval :
Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Datatype.String.Set.t ->
before:bool ->
Cil_types.stmt ->
eval:Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.set
val select_stmt_lval_rw :
Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
rd:Datatype.String.Set.t ->
wr:Datatype.String.Set.t ->
Cil_types.stmt ->
eval:Cil_types.stmt -> Kernel_function.t -> Db.Slicing.Select.set
val select_stmt_pred :
Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Cil_types.predicate ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.set
val select_stmt_term :
Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Cil_types.term ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.set
val select_stmt_annot :
Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
spare:bool ->
Cil_types.code_annotation ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.set
val select_stmt_annots :
Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
spare:bool ->
threat:bool ->
user_assert:bool ->
slicing_pragma:bool ->
loop_inv:bool ->
loop_var:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.set
val select_func_annots :
Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
spare:bool ->
threat:bool ->
user_assert:bool ->
slicing_pragma:bool ->
loop_inv:bool ->
loop_var:bool -> Cil_types.kernel_function -> Db.Slicing.Select.set
val select_func_lval :
Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Datatype.String.Set.t -> Kernel_function.t -> Db.Slicing.Select.set
val select_func_lval_rw :
Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
rd:Datatype.String.Set.t ->
wr:Datatype.String.Set.t ->
eval:Cil_types.stmt -> Kernel_function.t -> Db.Slicing.Select.set
val add_selection : Db.Slicing.Select.set -> unit
val add_persistent_selection : Db.Slicing.Select.set -> unit
val add_persistent_cmdline : unit -> unit
val apply_all : propagate_to_callers:bool -> unit
end