Slicing.SlicingCmds
val get_select_kf :
SlicingTypes.sl_select ->
Frama_c_kernel.Cil_types.kernel_function
val select_pdg_nodes :
set ->
SlicingTypes.sl_mark ->
Pdg_types.PdgTypes.Node.t list ->
Frama_c_kernel.Cil_types.kernel_function ->
set
val select_stmt :
set ->
spare:bool ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.kernel_function ->
set
val select_func_calls_to :
set ->
spare:bool ->
Frama_c_kernel.Kernel_function.t ->
set
val select_func_calls_into :
set ->
spare:bool ->
Frama_c_kernel.Kernel_function.t ->
set
val select_func_zone :
set ->
SlicingTypes.sl_mark ->
Frama_c_kernel.Locations.Zone.t ->
Frama_c_kernel.Cil_types.kernel_function ->
set
val select_func_return :
set ->
spare:bool ->
Frama_c_kernel.Kernel_function.t ->
set
val select_stmt_ctrl :
set ->
spare:bool ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.kernel_function ->
set
val select_stmt_zone :
set ->
SlicingTypes.sl_mark ->
Frama_c_kernel.Locations.Zone.t ->
before:bool ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.kernel_function ->
set
val select_stmt_lval :
set ->
SlicingTypes.sl_mark ->
Frama_c_kernel.Datatype.String.Set.t ->
before:bool ->
Frama_c_kernel.Cil_types.stmt ->
eval:Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.kernel_function ->
set
val select_stmt_lval_rw :
set ->
SlicingTypes.sl_mark ->
rd:Frama_c_kernel.Datatype.String.Set.t ->
wr:Frama_c_kernel.Datatype.String.Set.t ->
Frama_c_kernel.Cil_types.stmt ->
eval:Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Kernel_function.t ->
set
val select_stmt_pred :
set ->
SlicingTypes.sl_mark ->
Frama_c_kernel.Cil_types.predicate ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.kernel_function ->
set
val select_stmt_term :
set ->
SlicingTypes.sl_mark ->
Frama_c_kernel.Cil_types.term ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.kernel_function ->
set
val select_stmt_annot :
set ->
SlicingTypes.sl_mark ->
spare:bool ->
Frama_c_kernel.Cil_types.code_annotation ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.kernel_function ->
set
val select_stmt_annots :
set ->
SlicingTypes.sl_mark ->
spare:bool ->
threat:bool ->
user_assert:bool ->
slicing_pragma:bool ->
loop_inv:bool ->
loop_var:bool ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.kernel_function ->
set
val select_func_annots :
set ->
SlicingTypes.sl_mark ->
spare:bool ->
threat:bool ->
user_assert:bool ->
slicing_pragma:bool ->
loop_inv:bool ->
loop_var:bool ->
Frama_c_kernel.Cil_types.kernel_function ->
set
val select_func_lval :
set ->
SlicingTypes.sl_mark ->
Frama_c_kernel.Datatype.String.Set.t ->
Frama_c_kernel.Kernel_function.t ->
set
val select_func_lval_rw :
set ->
SlicingTypes.sl_mark ->
rd:Frama_c_kernel.Datatype.String.Set.t ->
wr:Frama_c_kernel.Datatype.String.Set.t ->
eval:Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Kernel_function.t ->
set
val add_selection : set -> unit
val add_persistent_selection : set -> unit