Skip to content
Snippets Groups Projects
Commit c28d06b8 authored by Patrick Baudin's avatar Patrick Baudin Committed by Allan Blanchard
Browse files

[Slicing] extracts comments of the Slicing API from an older db.ml

parent 4130bab7
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/slicing/api.ml
+ 0
− 1
View file @ c28d06b8
......@@ -164,7 +164,6 @@ module Select = struct
let dyn_t = SlicingTypes.Sl_select.ty
type set = SlicingCmds.set
module S = Cil_datatype.Varinfo.Map.Make(SlicingTypes.Fct_user_crit)
type selections = S.t
let dyn_set = S.ty
(** {2 Journalized selectors } *)
......
src/plugins/slicing/api.mli
+ 308
− 243
View file @ c28d06b8
......@@ -21,62 +21,72 @@
(**************************************************************************)
(* ---------------------------------------------------------------------- *)
(** Global data management *)
val split_slice :
SlicingInternals.fct_slice -> SlicingInternals.fct_slice list
val merge_slices :
SlicingInternals.fct_slice ->
SlicingInternals.fct_slice -> replace:bool -> SlicingInternals.fct_slice
val copy_slice : SlicingInternals.fct_slice -> SlicingInternals.fct_slice
(* ---------------------------------------------------------------------- *)
(** {1 Global setting } *)
(** {1 Global setting.} *)
(** Internal state of the slicing tool from project viewpoints. *)
val self : State.t
(* ---------------------------------------------------------------------- *)
(** {2 Functions with journalized side effects } *)
(** Set the used slicing modes. *)
val set_modes :
?calls:SlicingParameters.Mode.Calls.t ->
?callers:SlicingParameters.Mode.Callers.t ->
?sliceUndef:SlicingParameters.Mode.SliceUndef.t ->
?keepAnnotations:SlicingParameters.Mode.KeepAnnotations.t -> unit -> unit
(* ---------------------------------------------------------------------- *)
(** {1 Slicing project } *)
(** {1 Slicing project management.} *)
module Project : sig
(** {2 Values } *)
val default_slice_names :
Cil_types.kernel_function -> bool -> int -> string
(** {2 Functions with journalized side effects } *)
(** Init/reset a slicing project. *)
val reset_slicing : unit -> unit
(** Change the slicing level of this function
(see the [-slicing-level] option documentation to know the meaning of
the number)
@raise SlicingTypes.ExternalFunction if [kf] has no definition.
@raise SlicingTypes.WrongSlicingLevel if [n] is not valid. *)
val change_slicing_level : Cil_types.kernel_function -> int -> unit
(** Build a new [Db.Project.t] from all [Slice.t] of a project.
Can optionally specify how to name the sliced functions
by defining [f_slice_names].
[f_slice_names kf src_visi num_slice] has to return the name
of the exported functions based on the source function [kf].
- [src_visi] tells if the source function name is used
(if not, it can be used for a slice)
- [num_slice] gives the number of the slice to name.
The entry point function is only exported once :
it is VERY recommended to give to it its original name,
even if it is sliced. *)
val extract :
?f_slice_names:(Kernel_function.t -> bool -> int -> string) ->
?f_slice_names:(Cil_types.kernel_function -> bool -> int -> string) ->
string -> Project.t
(** Print a representation of the slicing project (call graph)
in a dot file which name is the given string. *)
val print_dot : filename:string -> title:string -> unit
val change_slicing_level : Kernel_function.t -> int -> unit
(** {2 No needs of Journalization} *)
val is_directly_called_internal : Kernel_function.t -> bool
val default_slice_names : Cil_types.kernel_function -> bool -> int -> string
(** Return [true] iff the source function is called (even indirectly via
transitivity) from a [Slice.t]. *)
val is_called : Cil_types.kernel_function -> bool
val has_persistent_selection : Kernel_function.t -> bool
(** Return [true] iff the source function has persistent selection *)
val has_persistent_selection : Cil_types.kernel_function -> bool
(** Return [true] if the source function is directly (even via pointer
function) called from a [Slice.t]. *)
val is_directly_called_internal : Cil_types.kernel_function -> bool
(** {2 Debug} *)
......@@ -86,257 +96,330 @@ end
(* ---------------------------------------------------------------------- *)
(** {1 Mark} *)
(** {1 Access to slicing results.} *)
module Mark : sig
(** Abstract data type for mark value. *)
type t = SlicingTypes.sl_mark
val dyn_t : SlicingTypes.Sl_mark.t Type.t
(** For dynamic type checking and journalization. *)
val dyn_t : t Type.t
(** {2 No needs of Journalization} *)
val compare : SlicingTypes.sl_mark -> SlicingTypes.sl_mark -> int
(** To construct a mark such as
[(is_ctrl result, is_data result, isaddr result) = (~ctrl, ~data, ~addr)],
[(is_bottom result) = false] and
[(is_spare result) = not (~ctrl || ~data || ~addr)]. *)
val make : data:bool -> addr:bool -> ctrl:bool -> t
val pretty : Format.formatter -> SlicingTypes.sl_mark -> unit
(** A total ordering function similar to the generic structural
comparison function [compare].
Can be used to build a map from [t] marks to, for example, colors for
the GUI. *)
val compare : t -> t -> int
val make : data:bool -> addr:bool -> ctrl:bool -> SlicingTypes.sl_mark
(** [true] iff the mark is empty: it is the only case where the associated
element is invisible. *)
val is_bottom : t -> bool
val is_bottom : SlicingTypes.sl_mark -> bool
(** Smallest visible mark. Usually used to mark element that need to be
visible for compilation purpose, not really for the selected computations.
That mark is related to transparent selection. *)
val is_spare : t -> bool
val is_spare : SlicingTypes.sl_mark -> bool
(** The element is used to control the program point of a selected data. *)
val is_ctrl : t -> bool
val is_ctrl : SlicingTypes.sl_mark -> bool
(** The element is used to compute selected data.
Notice that a mark can be [is_data] and/or [is_ctrl] and/or [is_addr]
at the same time. *)
val is_data : t -> bool
val is_data : SlicingTypes.sl_mark -> bool
(** The element is used to compute the address of a selected data. *)
val is_addr : t -> bool
val is_addr : SlicingTypes.sl_mark -> bool
(** The mark [m] related to all statements of a source function [kf].
Property : [is_bottom (get_from_func proj kf) =
not (Project.is_called proj kf) ] *)
val get_from_src_func : Cil_types.kernel_function -> t
val get_from_src_func : Kernel_function.t -> SlicingInternals.pdg_mark
(** {2 Debug} *)
val pretty : Format.formatter -> t -> unit
end
(* ---------------------------------------------------------------------- *)
(** {1 Selection} *)
(** {1 Slicing selections.} *)
module Select : sig
(** Internal selection. *)
type t = SlicingTypes.sl_select
val dyn_t : SlicingTypes.Sl_select.t Type.t
(** For dynamic type checking and journalization. *)
val dyn_t : t Type.t
(** Set of colored selections. *)
type set = SlicingCmds.set
type selections = SlicingTypes.Fct_user_crit.t Cil_datatype.Varinfo.Map.t
(** For dynamic type checking and journalization. *)
val dyn_set : set Type.t
val dyn_set : selections Type.t
(** {2 Selectors.} *)
(** {2 Journalized selectors } *)
(** Empty selection. *)
val empty_selects : set
val empty_selects : selections
(** {3 Statement selectors.} *)
(** To select a statement. *)
val select_stmt :
selections -> spare:bool -> Cil_datatype.Stmt.t -> Kernel_function.t -> selections
set -> spare:bool -> Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
(** To select a statement reachability.
Note: add also a transparent selection on the whole statement. *)
val select_stmt_ctrl :
selections -> spare:bool -> Cil_datatype.Stmt.t -> Kernel_function.t -> selections
set -> spare:bool -> Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
(** To select rw accesses to lvalues (given as string) related to a statement.
Variables of [~rd] and [~wr] string are bounded relatively to the whole
scope of the function.
The interpretation of the address of the lvalues is done just before the
execution of the statement [~eval].
The selection preserve the [~rd] and ~[wr] accesses contained into the
statement [ki].
Note: add also a transparent selection on the whole statement.
@modify Magnesium-20151001 argument [~scope] removed. *)
val select_stmt_lval_rw :
selections ->
SlicingTypes.Sl_mark.t ->
set ->
Mark.t ->
rd:Datatype.String.Set.t ->
wr:Datatype.String.Set.t ->
Cil_datatype.Stmt.t ->
eval:Cil_datatype.Stmt.t -> Kernel_function.t -> selections
eval:Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
(** To select lvalues (given as string) related to a statement.
Variables of [lval_str] string are bounded relatively to the whole scope
of the function.
The interpretation of the address of the lvalue is done just before the
execution of the statement [~eval].
The selection preserve the value of these lvalues before or after (c.f.
boolean [~before]) the statement [ki].
Note: add also a transparent selection on the whole statement.
@modify Magnesium-20151001 argument [~scope] removed. *)
val select_stmt_lval :
selections ->
SlicingTypes.Sl_mark.t ->
set ->
Mark.t ->
Datatype.String.Set.t ->
before:bool ->
Cil_datatype.Stmt.t ->
eval:Cil_datatype.Stmt.t -> Kernel_function.t -> selections
eval:Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
(** To select a zone value related to a statement.
Note: add also a transparent selection on the whole statement. *)
val select_stmt_zone :
set ->
Mark.t ->
Locations.Zone.t ->
before:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> set
(** To select a predicate value related to a statement.
Note: add also a transparent selection on the whole statement. *)
val select_stmt_term :
set ->
Mark.t ->
Cil_types.term ->
Cil_types.stmt -> Cil_types.kernel_function -> set
(** To select a predicate value related to a statement.
Note: add also a transparent selection on the whole statement. *)
val select_stmt_pred :
set ->
Mark.t ->
Cil_types.predicate ->
Cil_types.stmt -> Cil_types.kernel_function -> set
(** To select the annotations related to a statement.
Note: add also a transparent selection on the whole statement. *)
val select_stmt_annot :
set ->
Mark.t ->
spare:bool ->
Cil_types.code_annotation ->
Cil_types.stmt -> Cil_types.kernel_function -> set
(** To select the annotations related to a statement.
Note: add also a transparent selection on the whole statement. *)
val select_stmt_annots :
selections ->
SlicingTypes.Sl_mark.t ->
set ->
Mark.t ->
spare:bool ->
threat:bool ->
user_assert:bool ->
slicing_pragma:bool ->
loop_inv:bool ->
loop_var:bool -> Cil_datatype.Stmt.t -> Kernel_function.t -> selections
loop_var:bool -> Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
(** {3 Function selectors.} *)
(** To select rw accesses to lvalues (given as a string) related to a
function.
Variables of [~rd] and [~wr] string are bounded relatively to the whole
scope of the function.
The interpretation of the address of the lvalues is done just before the
execution of the statement [~eval].
The selection preserve the value of these lvalues into the whole project.
@modify Magnesium-20151001 argument [~scope] removed. *)
val select_func_lval_rw :
set -> Mark.t -> rd:Datatype.String.Set.t -> wr:Datatype.String.Set.t ->
eval:Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
(** To select lvalues (given as a string) related to a function.
Variables of [lval_str] string are bounded relatively to the scope of the
first statement of [kf].
The interpretation of the address of the lvalues is done just before the
execution of the first statement [kf].
The selection preserve the value of these lvalues before execution of the
return statement. *)
val select_func_lval :
selections ->
SlicingTypes.Sl_mark.t ->
Datatype.String.Set.t -> Kernel_function.t -> selections
set -> Mark.t -> Datatype.String.Set.t -> Cil_types.kernel_function -> set
val select_func_lval_rw :
selections ->
SlicingTypes.Sl_mark.t ->
rd:Datatype.String.Set.t ->
wr:Datatype.String.Set.t ->
eval:Cil_datatype.Stmt.t -> Kernel_function.t -> selections
(** To select an output zone related to a function. *)
val select_func_zone :
set -> Mark.t -> Locations.Zone.t -> Cil_types.kernel_function -> set
val select_func_return : selections -> spare:bool -> Kernel_function.t -> selections
(** To select the function result (returned value). *)
val select_func_return : set -> spare:bool -> Cil_types.kernel_function -> set
(** To select every calls to the given function, i.e. the call keeps its
semantics in the slice. *)
val select_func_calls_to :
selections -> spare:bool -> Kernel_function.t -> selections
set -> spare:bool -> Cil_types.kernel_function -> set
(** To select every calls to the given function without the selection of its
inputs/outputs. *)
val select_func_calls_into :
selections -> spare:bool -> Kernel_function.t -> selections
set -> spare:bool -> Cil_types.kernel_function -> set
(** To select the annotations related to a function. *)
val select_func_annots :
selections ->
SlicingTypes.Sl_mark.t ->
spare:bool ->
threat:bool ->
user_assert:bool ->
slicing_pragma:bool ->
loop_inv:bool -> loop_var:bool -> Kernel_function.t -> selections
val select_func_zone :
SlicingCmds.set ->
SlicingTypes.sl_mark ->
Locations.Zone.t -> Cil_types.kernel_function -> SlicingCmds.set
val select_stmt_term :
SlicingCmds.set ->
SlicingTypes.sl_mark ->
Cil_types.term ->
Cil_types.stmt -> Cil_types.kernel_function -> SlicingCmds.set
set -> Mark.t -> spare:bool -> threat:bool -> user_assert:bool ->
slicing_pragma:bool -> loop_inv:bool -> loop_var:bool ->
Cil_types.kernel_function -> set
val select_stmt_pred :
SlicingCmds.set ->
SlicingTypes.sl_mark ->
Cil_types.predicate ->
Cil_types.stmt -> Cil_types.kernel_function -> SlicingCmds.set
val select_stmt_annot :
SlicingCmds.set ->
SlicingTypes.sl_mark ->
spare:bool ->
Cil_types.code_annotation ->
Cil_types.stmt -> Cil_types.kernel_function -> SlicingCmds.set
val select_stmt_zone :
SlicingCmds.set ->
SlicingTypes.sl_mark ->
Locations.Zone.t ->
before:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> SlicingCmds.set
(** {3 Pdg selectors.} *)
val select_pdg_nodes :
SlicingCmds.set ->
SlicingTypes.sl_mark ->
PdgTypes.Node.t list -> Cil_types.kernel_function -> SlicingCmds.set
set -> Mark.t -> PdgTypes.Node.t list -> Cil_types.kernel_function -> set
(** {3 Internal use only} *)
val get_function : SlicingTypes.sl_select -> Cil_types.kernel_function
(** The function related to an internal selection. *)
val get_function : t -> Cil_types.kernel_function
val merge_internal :
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
(** The function related to an internal selection. *)
val merge_internal : t -> t -> t
val add_to_selects_internal :
Cil_datatype.Varinfo.Map.key * SlicingInternals.fct_user_crit ->
SlicingInternals.fct_user_crit Cil_datatype.Varinfo.Map.t ->
SlicingInternals.fct_user_crit Cil_datatype.Varinfo.Map.t
val add_to_selects_internal : t -> set -> set
val iter_selects_internal :
(Cil_datatype.Varinfo.Map.key * 'a -> unit) ->
'a Cil_datatype.Varinfo.Map.t -> unit
val iter_selects_internal : (t -> unit) -> set -> unit
val fold_selects_internal :
('a -> Cil_datatype.Varinfo.Map.key * 'b -> 'a) ->
'a -> 'b Cil_datatype.Varinfo.Map.t -> 'a
val fold_selects_internal : (('a -> t -> 'a) -> 'a -> set -> 'a)
(** Internally used to select a statement :
- if [is_ctrl_mark m],
propagate ctrl_mark on ctrl dependencies of the statement
- if [is_addr_mark m],
propagate addr_mark on addr dependencies of the statement
- if [is_data_mark m],
propagate data_mark on data dependencies of the statement
Marks the node with a spare_mark and propagate so that the dependencies
that were not selected yet will be marked spare.
When the statement is a call, its functional inputs/outputs are also
selected (The call is still selected even it has no output).
When the statement is a composed one (block, if, etc...),
all the sub-statements are selected.
@raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_stmt_internal :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_types.stmt ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
Cil_types.kernel_function -> ?select:t -> Cil_types.stmt -> Mark.t -> t
val select_label_internal :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_types.logic_label ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
Cil_types.kernel_function ->
?select:t -> Cil_types.logic_label -> Mark.t -> t
(** Internally used to select a statement call without its
inputs/outputs so that it doesn't select the statements computing the
inputs of the called function as [select_stmt_internal] would do.
Raise [Invalid_argument] when the [stmt] isn't a call.
@raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_min_call_internal :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_types.stmt ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
Cil_types.kernel_function -> ?select:t -> Cil_types.stmt -> Mark.t -> t
(** Internally used to select a zone value at a program point.
@raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_stmt_zone_internal :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_types.stmt ->
before:bool ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
Cil_types.kernel_function ->
?select:t ->
Cil_types.stmt -> before:bool -> Locations.Zone.t -> Mark.t -> t
(** Internally used to select a zone value at the beginning of a function.
For a defined function, it is similar to [select_stmt_zone_internal]
with the initial statement, but it can also be used for undefined
functions.
@raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_zone_at_entry_point_internal :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
Cil_types.kernel_function -> ?select:t -> Locations.Zone.t -> Mark.t -> t
(** Internally used to select a zone value at the end of a function.
For a defined function, it is similar to [select_stmt_zone_internal]
with the return statement, but it can also be used for undefined
functions.
@raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_zone_at_end_internal :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
Cil_types.kernel_function -> ?select:t -> Locations.Zone.t -> Mark.t -> t
(** Internally used to select the statements that modify the
given zone considered as in output.
Be careful that it is NOT the same as selecting the zone at the end!
The 'undef' zone is not propagated...
@raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_modified_output_zone_internal :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
Cil_types.kernel_function -> ?select:t -> Locations.Zone.t -> Mark.t -> t
(** Internally used to select a statement reachability :
Only propagate a ctrl_mark on the statement control dependencies.
@raise SlicingTypes.NoPdg when the Pdg cannot be computed. *)
val select_stmt_ctrl_internal :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_types.stmt ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
Cil_types.kernel_function -> ?select:t -> Cil_types.stmt -> t
val select_entry_point_internal :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
Cil_types.kernel_function -> ?select:t -> Mark.t -> t
val select_return_internal :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
Cil_types.kernel_function -> ?select:t -> Mark.t -> t
val select_decl_var_internal :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_types.varinfo ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
Cil_types.kernel_function -> ?select:t -> Cil_types.varinfo -> Mark.t -> t
(** Internally used to select PDG nodes :
- if [is_ctrl_mark m],
propagate ctrl_mark on ctrl dependencies of the statement
- if [is_addr_mark m],
propagate addr_mark on addr dependencies of the statement
- if [is_data_mark m],
propagate data_mark on data dependencies of the statement
Marks the node with a spare_mark and propagate so that
the dependencies that were not selected yet will be marked spare. *)
val select_pdg_nodes_internal :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
PdgTypes.Node.t list ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
Cil_types.kernel_function ->
?select:t -> PdgTypes.Node.t list -> Mark.t -> t
(** {2 Debug} *)
val pretty :
Format.formatter ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
val pretty : Format.formatter -> t -> unit
end
......@@ -346,61 +429,45 @@ end
module Slice : sig
type t = SlicingTypes.sl_fct_slice
val dyn_t : SlicingTypes.Sl_fct_slice.t Type.t
val dyn_t : t Type.t
(** {2 Functions with journalized side effects } *)
val create : Kernel_function.t -> SlicingTypes.Sl_fct_slice.t
val create : Cil_types.kernel_function -> t
val remove : SlicingTypes.Sl_fct_slice.t -> unit
val remove : t -> unit
val remove_uncalled : unit -> unit
(** {2 No needs of Journalization} *)
val get_all : Kernel_function.t -> SlicingInternals.fct_slice list
val get_all : Cil_types.kernel_function -> t list
val get_function :
SlicingInternals.fct_slice -> Cil_types.kernel_function
val get_function : t -> Cil_types.kernel_function
val get_callers :
SlicingInternals.fct_slice -> SlicingInternals.fct_slice list
val get_callers : t -> t list
val get_called_slice :
SlicingInternals.fct_slice ->
Cil_types.stmt -> SlicingInternals.fct_slice option
val get_called_slice : t -> Cil_types.stmt -> t option
val get_called_funcs :
SlicingInternals.fct_slice ->
Cil_types.stmt -> Kernel_function.Hptset.elt list
val get_called_funcs : t -> Cil_types.stmt -> Cil_types.kernel_function list
val get_mark_from_stmt :
SlicingInternals.fct_slice ->
Cil_types.stmt -> SlicingInternals.pdg_mark
val get_mark_from_stmt : t -> Cil_types.stmt -> Mark.t
val get_mark_from_label :
SlicingInternals.fct_slice ->
Cil_types.stmt -> Cil_types.label -> SlicingInternals.pdg_mark
val get_mark_from_label : t -> Cil_types.stmt -> Cil_types.label -> Mark.t
val get_mark_from_local_var :
SlicingInternals.fct_slice ->
Cil_types.varinfo -> SlicingInternals.pdg_mark
val get_mark_from_local_var : t -> Cil_types.varinfo -> Mark.t
val get_mark_from_formal :
SlicingInternals.fct_slice ->
Cil_datatype.Varinfo.t -> SlicingInternals.pdg_mark
val get_mark_from_formal : t -> Cil_datatype.Varinfo.t -> Mark.t
val get_user_mark_from_inputs :
SlicingInternals.fct_slice -> SlicingInternals.pdg_mark
val get_user_mark_from_inputs : t -> Mark.t
val get_num_id : SlicingInternals.fct_slice -> int
val get_num_id : t -> int
val from_num_id :
Kernel_function.t -> int -> SlicingInternals.fct_slice
val from_num_id : Cil_types.kernel_function -> int -> t
(** {2 Debug} *)
val pretty : Format.formatter -> SlicingInternals.fct_slice -> unit
val pretty : Format.formatter -> t -> unit
end
......@@ -419,32 +486,22 @@ module Request : sig
val propagate_user_marks : unit -> unit
val copy_slice :
SlicingTypes.Sl_fct_slice.t -> SlicingTypes.Sl_fct_slice.t
val copy_slice : Slice.t -> Slice.t
val split_slice :
SlicingTypes.Sl_fct_slice.t -> SlicingTypes.Sl_fct_slice.t list
val split_slice : Slice.t -> Slice.t list
val merge_slices :
SlicingTypes.Sl_fct_slice.t ->
SlicingTypes.Sl_fct_slice.t ->
replace:bool -> SlicingTypes.Sl_fct_slice.t
val merge_slices : Slice.t -> Slice.t -> replace:bool -> Slice.t
val add_call_slice :
caller:SlicingTypes.Sl_fct_slice.t ->
to_call:SlicingTypes.Sl_fct_slice.t -> unit
val add_call_slice : caller:Slice.t -> to_call:Slice.t -> unit
val add_call_fun :
caller:SlicingTypes.Sl_fct_slice.t ->
to_call:Kernel_function.t -> unit
val add_call_fun : caller:Slice.t -> to_call:Cil_types.kernel_function -> unit
val add_call_min_fun :
caller:SlicingTypes.Sl_fct_slice.t ->
to_call:Kernel_function.t -> unit
caller:Slice.t -> to_call:Cil_types.kernel_function -> unit
val add_selection : Select.selections -> unit
val add_selection : Select.set -> unit
val add_persistent_selection : Select.selections -> unit
val add_persistent_selection : Select.set -> unit
val add_persistent_cmdline : unit -> unit
......@@ -452,15 +509,23 @@ module Request : sig
val is_request_empty_internal : unit -> bool
val add_slice_selection_internal :
SlicingInternals.fct_slice ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
val add_slice_selection_internal : Slice.t -> Select.t -> unit
val add_selection_internal :
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
val add_selection_internal : Select.t -> unit
(** {2 Debug} *)
val pretty : Format.formatter -> unit
end
(* ---------------------------------------------------------------------- *)
(** {1 Global data management} *)
val split_slice : Slice.t -> Slice.t list
val merge_slices : Slice.t -> Slice.t -> replace:bool -> Slice.t
val copy_slice : Slice.t -> Slice.t
(* -- end -------------------------------------------------------------- *)
src/plugins/slicing/slicingSelect.mli
+ 41
− 41
View file @ c28d06b8
......@@ -24,14 +24,14 @@ val check_call : Cil_types.stmt -> bool -> Cil_types.stmt
val print_select :
Format.formatter ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
SlicingTypes.sl_select -> unit
val get_select_kf : Cil_types.varinfo * 'a -> Cil_types.kernel_function
val check_db_select :
Cil_datatype.Varinfo.t ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select ->
SlicingTypes.sl_select
val empty_db_select :
Kernel_function.t -> Cil_types.varinfo * SlicingInternals.fct_user_crit
......@@ -43,30 +43,30 @@ val top_db_select :
val check_kf_db_select :
Kernel_function.t ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select ->
SlicingTypes.sl_select
val check_ff_db_select :
SlicingInternals.fct_slice ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
SlicingTypes.sl_select ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
val bottom_msg : Kernel_function.t -> unit
val basic_add_select :
Kernel_function.t ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
SlicingTypes.sl_select ->
PdgTypes.Node.t list ->
?undef:Locations.Zone.t option * SlicingTypes.sl_mark ->
SlicingActions.n_or_d_marks ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
val select_pdg_nodes :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
?select:SlicingTypes.sl_select ->
PdgTypes.Node.t list ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
val mk_select :
Db.Pdg.t ->
......@@ -77,12 +77,12 @@ val mk_select :
val select_stmt_zone :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
?select:SlicingTypes.sl_select ->
Cil_types.stmt ->
before:bool ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
(** this one is similar to [select_stmt_zone] with the return statement
* when the function is defined, but it can also be used for undefined functions. *)
......@@ -90,91 +90,91 @@ val select_in_out_zone :
at_end:bool ->
use_undef:bool ->
Kernel_function.t ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
SlicingTypes.sl_select ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
val select_zone_at_end :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
?select:SlicingTypes.sl_select ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
val select_modified_output_zone :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
?select:SlicingTypes.sl_select ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
val select_zone_at_entry :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
?select:SlicingTypes.sl_select ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
val stmt_nodes_to_select :
Db.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t list
val select_stmt_computation :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
?select:SlicingTypes.sl_select ->
Cil_types.stmt ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
val select_label :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
?select:SlicingTypes.sl_select ->
Cil_types.logic_label ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
(** marking a call node means that a [choose_call] will have to decide that to
* call according to the slicing-level, but anyway, the call will be visible.
*)
val select_minimal_call :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
?select:SlicingTypes.sl_select ->
Cil_types.stmt ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
val select_stmt_ctrl :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_types.stmt -> Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
?select:SlicingTypes.sl_select ->
Cil_types.stmt -> SlicingTypes.sl_select
val select_entry_point :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
?select:SlicingTypes.sl_select ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
val select_return :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
?select:SlicingTypes.sl_select ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
val select_decl_var :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
?select:SlicingTypes.sl_select ->
Cil_types.varinfo ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select
val merge_select :
SlicingInternals.fct_user_crit ->
SlicingInternals.fct_user_crit -> SlicingInternals.fct_user_crit
val merge_db_select :
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
SlicingTypes.sl_select ->
SlicingTypes.sl_select ->
SlicingTypes.sl_select
module Selections : sig
......@@ -214,13 +214,13 @@ val call_min_f_in_caller :
val is_already_selected :
SlicingInternals.fct_slice ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> bool
SlicingTypes.sl_select -> bool
val add_ff_selection :
SlicingInternals.fct_slice ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
SlicingTypes.sl_select -> unit
(** add a persistent selection to the function.
* This might change its slicing level in order to call slices later on. *)
val add_fi_selection :
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
SlicingTypes.sl_select -> unit
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment