sig
exception No_Project
exception Existing_Project
val self : State.t Pervasives.ref
val set_modes :
(?calls:int ->
?callers:bool ->
?sliceUndef:bool -> ?keepAnnotations:bool -> ?print:bool -> unit -> unit)
Pervasives.ref
module Project :
sig
type t = SlicingTypes.sl_project
val dyn_t : Db.Slicing.Project.t Type.t
val mk_project : (string -> Db.Slicing.Project.t) Pervasives.ref
val from_unique_name : (string -> Db.Slicing.Project.t) Pervasives.ref
val get_all : (unit -> Db.Slicing.Project.t list) Pervasives.ref
val set_project : (Db.Slicing.Project.t option -> unit) Pervasives.ref
val get_project : (unit -> Db.Slicing.Project.t option) Pervasives.ref
val get_name : (Db.Slicing.Project.t -> string) Pervasives.ref
val is_called :
(Db.Slicing.Project.t -> Cil_types.kernel_function -> bool)
Pervasives.ref
val has_persistent_selection :
(Db.Slicing.Project.t -> Cil_types.kernel_function -> bool)
Pervasives.ref
val change_slicing_level :
(Db.Slicing.Project.t -> Cil_types.kernel_function -> int -> unit)
Pervasives.ref
val default_slice_names :
(Cil_types.kernel_function -> bool -> int -> string) Pervasives.ref
val extract :
(string ->
?f_slice_names:(Cil_types.kernel_function -> bool -> int -> string) ->
Db.Slicing.Project.t -> Project.t)
Pervasives.ref
val print_extracted_project :
(?fmt:Format.formatter -> extracted_prj:Project.t -> unit)
Pervasives.ref
val print_dot :
(filename:string -> title:string -> Db.Slicing.Project.t -> unit)
Pervasives.ref
val pretty :
(Format.formatter -> Db.Slicing.Project.t -> unit) Pervasives.ref
val is_directly_called_internal :
(Db.Slicing.Project.t -> Cil_types.kernel_function -> bool)
Pervasives.ref
end
module Mark :
sig
type t = SlicingTypes.sl_mark
val dyn_t : Db.Slicing.Mark.t Type.t
val make :
(data:bool -> addr:bool -> ctrl:bool -> Db.Slicing.Mark.t)
Pervasives.ref
val compare :
(Db.Slicing.Mark.t -> Db.Slicing.Mark.t -> int) Pervasives.ref
val is_bottom : (Db.Slicing.Mark.t -> bool) Pervasives.ref
val is_spare : (Db.Slicing.Mark.t -> bool) Pervasives.ref
val is_data : (Db.Slicing.Mark.t -> bool) Pervasives.ref
val is_ctrl : (Db.Slicing.Mark.t -> bool) Pervasives.ref
val is_addr : (Db.Slicing.Mark.t -> bool) Pervasives.ref
val get_from_src_func :
(Db.Slicing.Project.t ->
Cil_types.kernel_function -> Db.Slicing.Mark.t)
Pervasives.ref
val pretty :
(Format.formatter -> Db.Slicing.Mark.t -> unit) Pervasives.ref
end
module Select :
sig
type t = SlicingTypes.sl_select
val dyn_t : Db.Slicing.Select.t Type.t
type set = SlicingTypes.Fct_user_crit.t Cil_datatype.Varinfo.Map.t
val dyn_set : Db.Slicing.Select.set Type.t
val empty_selects : Db.Slicing.Select.set
val select_stmt :
(Db.Slicing.Select.set ->
spare:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.set)
Pervasives.ref
val select_stmt_ctrl :
(Db.Slicing.Select.set ->
spare:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.set)
Pervasives.ref
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 ->
Cil_types.kernel_function -> Db.Slicing.Select.set)
Pervasives.ref
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)
Pervasives.ref
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)
Pervasives.ref
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)
Pervasives.ref
val select_stmt_pred :
(Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Cil_types.predicate Cil_types.named ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.set)
Pervasives.ref
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)
Pervasives.ref
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)
Pervasives.ref
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 ->
Cil_types.kernel_function -> Db.Slicing.Select.set)
Pervasives.ref
val select_func_lval :
(Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Datatype.String.Set.t ->
Cil_types.kernel_function -> Db.Slicing.Select.set)
Pervasives.ref
val select_func_zone :
(Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Locations.Zone.t ->
Cil_types.kernel_function -> Db.Slicing.Select.set)
Pervasives.ref
val select_func_return :
(Db.Slicing.Select.set ->
spare:bool -> Cil_types.kernel_function -> Db.Slicing.Select.set)
Pervasives.ref
val select_func_calls_to :
(Db.Slicing.Select.set ->
spare:bool -> Cil_types.kernel_function -> Db.Slicing.Select.set)
Pervasives.ref
val select_func_calls_into :
(Db.Slicing.Select.set ->
spare:bool -> Cil_types.kernel_function -> Db.Slicing.Select.set)
Pervasives.ref
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)
Pervasives.ref
val pretty :
(Format.formatter -> Db.Slicing.Select.t -> unit) Pervasives.ref
val get_function :
(Db.Slicing.Select.t -> Cil_types.kernel_function) Pervasives.ref
val merge_internal :
(Db.Slicing.Select.t -> Db.Slicing.Select.t -> Db.Slicing.Select.t)
Pervasives.ref
val add_to_selects_internal :
(Db.Slicing.Select.t ->
Db.Slicing.Select.set -> Db.Slicing.Select.set)
Pervasives.ref
val iter_selects_internal :
((Db.Slicing.Select.t -> unit) -> Db.Slicing.Select.set -> unit)
Pervasives.ref
val fold_selects_internal :
('a -> Db.Slicing.Select.t -> 'a) ->
'a -> Db.Slicing.Select.set -> 'a
val select_stmt_internal :
(Cil_types.kernel_function ->
?select:Db.Slicing.Select.t ->
Cil_types.stmt -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)
Pervasives.ref
val select_label_internal :
(Cil_types.kernel_function ->
?select:Db.Slicing.Select.t ->
Cil_datatype.Logic_label.t ->
Db.Slicing.Mark.t -> Db.Slicing.Select.t)
Pervasives.ref
val select_min_call_internal :
(Cil_types.kernel_function ->
?select:Db.Slicing.Select.t ->
Cil_types.stmt -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)
Pervasives.ref
val select_stmt_zone_internal :
(Cil_types.kernel_function ->
?select:Db.Slicing.Select.t ->
Cil_types.stmt ->
before:bool ->
Locations.Zone.t -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)
Pervasives.ref
val select_zone_at_entry_point_internal :
(Cil_types.kernel_function ->
?select:Db.Slicing.Select.t ->
Locations.Zone.t -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)
Pervasives.ref
val select_zone_at_end_internal :
(Cil_types.kernel_function ->
?select:Db.Slicing.Select.t ->
Locations.Zone.t -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)
Pervasives.ref
val select_modified_output_zone_internal :
(Cil_types.kernel_function ->
?select:Db.Slicing.Select.t ->
Locations.Zone.t -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)
Pervasives.ref
val select_stmt_ctrl_internal :
(Cil_types.kernel_function ->
?select:Db.Slicing.Select.t -> Cil_types.stmt -> Db.Slicing.Select.t)
Pervasives.ref
val select_pdg_nodes_internal :
(Cil_types.kernel_function ->
?select:Db.Slicing.Select.t ->
PdgTypes.Node.t list -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)
Pervasives.ref
val select_entry_point_internal :
(Cil_types.kernel_function ->
?select:Db.Slicing.Select.t ->
Db.Slicing.Mark.t -> Db.Slicing.Select.t)
Pervasives.ref
val select_return_internal :
(Cil_types.kernel_function ->
?select:Db.Slicing.Select.t ->
Db.Slicing.Mark.t -> Db.Slicing.Select.t)
Pervasives.ref
val select_decl_var_internal :
(Cil_types.kernel_function ->
?select:Db.Slicing.Select.t ->
Cil_types.varinfo -> Db.Slicing.Mark.t -> Db.Slicing.Select.t)
Pervasives.ref
val select_pdg_nodes :
(Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
PdgTypes.Node.t list ->
Cil_types.kernel_function -> Db.Slicing.Select.set)
Pervasives.ref
end
module Slice :
sig
type t = SlicingTypes.sl_fct_slice
val dyn_t : Db.Slicing.Slice.t Type.t
val create :
(Db.Slicing.Project.t ->
Cil_types.kernel_function -> Db.Slicing.Slice.t)
Pervasives.ref
val remove :
(Db.Slicing.Project.t -> Db.Slicing.Slice.t -> unit) Pervasives.ref
val remove_uncalled : (Db.Slicing.Project.t -> unit) Pervasives.ref
val get_all :
(Db.Slicing.Project.t ->
Cil_types.kernel_function -> Db.Slicing.Slice.t list)
Pervasives.ref
val get_function :
(Db.Slicing.Slice.t -> Cil_types.kernel_function) Pervasives.ref
val get_callers :
(Db.Slicing.Slice.t -> Db.Slicing.Slice.t list) Pervasives.ref
val get_called_slice :
(Db.Slicing.Slice.t -> Cil_types.stmt -> Db.Slicing.Slice.t option)
Pervasives.ref
val get_called_funcs :
(Db.Slicing.Slice.t ->
Cil_types.stmt -> Cil_types.kernel_function list)
Pervasives.ref
val get_mark_from_stmt :
(Db.Slicing.Slice.t -> Cil_types.stmt -> Db.Slicing.Mark.t)
Pervasives.ref
val get_mark_from_label :
(Db.Slicing.Slice.t ->
Cil_types.stmt -> Cil_types.label -> Db.Slicing.Mark.t)
Pervasives.ref
val get_mark_from_local_var :
(Db.Slicing.Slice.t -> Cil_types.varinfo -> Db.Slicing.Mark.t)
Pervasives.ref
val get_mark_from_formal :
(Db.Slicing.Slice.t -> Cil_types.varinfo -> Db.Slicing.Mark.t)
Pervasives.ref
val get_user_mark_from_inputs :
(Db.Slicing.Slice.t -> Db.Slicing.Mark.t) Pervasives.ref
val get_num_id : (Db.Slicing.Slice.t -> int) Pervasives.ref
val from_num_id :
(Db.Slicing.Project.t ->
Cil_types.kernel_function -> int -> Db.Slicing.Slice.t)
Pervasives.ref
val pretty :
(Format.formatter -> Db.Slicing.Slice.t -> unit) Pervasives.ref
end
module Request :
sig
val apply_all :
(Db.Slicing.Project.t -> propagate_to_callers:bool -> unit)
Pervasives.ref
val add_selection :
(Db.Slicing.Project.t -> Db.Slicing.Select.set -> unit)
Pervasives.ref
val add_persistent_selection :
(Db.Slicing.Project.t -> Db.Slicing.Select.set -> unit)
Pervasives.ref
val add_persistent_cmdline :
(Db.Slicing.Project.t -> unit) Pervasives.ref
val is_already_selected_internal :
(Db.Slicing.Slice.t -> Db.Slicing.Select.t -> bool) Pervasives.ref
val add_slice_selection_internal :
(Db.Slicing.Project.t ->
Db.Slicing.Slice.t -> Db.Slicing.Select.t -> unit)
Pervasives.ref
val add_selection_internal :
(Db.Slicing.Project.t -> Db.Slicing.Select.t -> unit) Pervasives.ref
val add_call_slice :
(Db.Slicing.Project.t ->
caller:Db.Slicing.Slice.t -> to_call:Db.Slicing.Slice.t -> unit)
Pervasives.ref
val add_call_fun :
(Db.Slicing.Project.t ->
caller:Db.Slicing.Slice.t ->
to_call:Cil_types.kernel_function -> unit)
Pervasives.ref
val add_call_min_fun :
(Db.Slicing.Project.t ->
caller:Db.Slicing.Slice.t ->
to_call:Cil_types.kernel_function -> unit)
Pervasives.ref
val apply_all_internal : (Db.Slicing.Project.t -> unit) Pervasives.ref
val apply_next_internal : (Db.Slicing.Project.t -> unit) Pervasives.ref
val is_request_empty_internal :
(Db.Slicing.Project.t -> bool) Pervasives.ref
val merge_slices :
(Db.Slicing.Project.t ->
Db.Slicing.Slice.t ->
Db.Slicing.Slice.t -> replace:bool -> Db.Slicing.Slice.t)
Pervasives.ref
val copy_slice :
(Db.Slicing.Project.t -> Db.Slicing.Slice.t -> Db.Slicing.Slice.t)
Pervasives.ref
val split_slice :
(Db.Slicing.Project.t ->
Db.Slicing.Slice.t -> Db.Slicing.Slice.t list)
Pervasives.ref
val propagate_user_marks :
(Db.Slicing.Project.t -> unit) Pervasives.ref
val pretty :
(Format.formatter -> Db.Slicing.Project.t -> unit) Pervasives.ref
end
end