functor
(SliceName : sig
val get : Cil_types.kernel_function -> bool -> int -> string
end) ->
sig
exception EraseAssigns
exception EraseAllocation
type proj = SlicingInternals.project
type transform = {
slice : SlicingInternals.fct_slice;
src_visible : bool;
keep_body : bool;
}
type fct =
Iff of SlicingTransform.Visibility.transform
| Isrc of bool
| Iproto
val keep_body : Kernel_function.t -> bool
val fct_info :
SlicingInternals.project ->
Kernel_function.t -> SlicingTransform.Visibility.fct list
val fct_name :
Cil_datatype.Varinfo.t -> SlicingTransform.Visibility.fct -> string
val visible_mark : Db.Slicing.Mark.t -> bool
val param_visible : SlicingTransform.Visibility.fct -> int -> bool
val body_visible : SlicingTransform.Visibility.fct -> bool
val inst_visible :
SlicingTransform.Visibility.fct -> Cil_types.stmt -> bool
val label_visible :
SlicingTransform.Visibility.fct ->
Cil_types.stmt -> Cil_types.label -> bool
val data_in_visible :
SlicingInternals.fct_slice -> Locations.Zone.t option -> bool
val all_nodes_visible :
SlicingInternals.fct_slice -> PdgTypes.Node.t list -> bool
exception NoDataInfo
val data_nodes_visible :
SlicingInternals.fct_slice ->
PdgTypes.Node.t list *
((PdgTypes.Node.t * Locations.Zone.t option) list *
Locations.Zone.t option)
option -> bool
val all_logic_var_visible :
SlicingInternals.fct_slice -> Cil_types.predicate -> bool
val all_logic_var_visible_identified_term :
SlicingInternals.fct_slice -> Cil_types.identified_term -> bool
val all_logic_var_visible_term :
SlicingInternals.fct_slice -> Cil_types.term -> bool
val all_logic_var_visible_assigns :
SlicingInternals.fct_slice ->
Cil_types.identified_term * Cil_types.identified_term Cil_types.deps ->
bool
val all_logic_var_visible_deps :
SlicingInternals.fct_slice -> Cil_types.identified_term -> bool
val annotation_visible :
SlicingTransform.Visibility.fct ->
Cil_types.stmt -> Cil_types.code_annotation -> bool
val fun_precond_visible :
SlicingTransform.Visibility.fct -> Cil_types.predicate -> bool
val fun_postcond_visible :
SlicingTransform.Visibility.fct -> Cil_types.predicate -> bool
val fun_variant_visible :
SlicingTransform.Visibility.fct -> Cil_types.term -> bool
val fun_frees_visible :
SlicingTransform.Visibility.fct -> Cil_types.identified_term -> bool
val fun_allocates_visible :
SlicingTransform.Visibility.fct -> Cil_types.identified_term -> bool
val fun_assign_visible :
SlicingTransform.Visibility.fct ->
Cil_types.identified_term * Cil_types.identified_term Cil_types.deps ->
bool
val fun_deps_visible :
SlicingTransform.Visibility.fct -> Cil_types.identified_term -> bool
val loc_var_visible :
SlicingTransform.Visibility.fct -> Cil_types.varinfo -> bool
val res_call_visible :
SlicingTransform.Visibility.fct -> Cil_types.stmt -> bool
val result_visible : 'a -> SlicingTransform.Visibility.fct -> bool
val called_info :
SlicingInternals.project * SlicingTransform.Visibility.fct ->
Cil_types.stmt ->
(Cil_types.kernel_function * SlicingTransform.Visibility.fct) option
val cond_edge_visible : 'a -> Cil_types.stmt -> bool * bool
end