sig
type level_option =
DontSlice
| DontSliceButComputeMarks
| MinNbSlice
| MaxNbSlice
type mark = Cav of PdgTypes.Dpd.t | Spare
val compare_mark : SlicingInternals.mark -> SlicingInternals.mark -> int
type pdg_mark = { m1 : SlicingInternals.mark; m2 : SlicingInternals.mark; }
val pdg_mark_packed_descr : Structural_descr.pack
val compare_pdg_mark :
SlicingInternals.pdg_mark -> SlicingInternals.pdg_mark -> int
type fct_info = {
fi_kf : Cil_types.kernel_function;
fi_def : Cil_types.fundec option;
mutable fi_top : SlicingInternals.pdg_mark option;
mutable fi_level_option : SlicingInternals.level_option;
mutable fi_init_marks : SlicingInternals.ff_marks option;
mutable fi_slices : SlicingInternals.fct_slice list;
mutable fi_next_ff_num : int;
mutable f_called_by : SlicingInternals.called_by;
}
and called_by = (SlicingInternals.fct_slice * Cil_types.stmt) list
and fct_slice = {
ff_fct : SlicingInternals.fct_info;
ff_id : int;
mutable ff_marks : SlicingInternals.ff_marks;
mutable ff_called_by : SlicingInternals.called_by;
}
and fct_id =
FctSrc of SlicingInternals.fct_info
| FctSliced of SlicingInternals.fct_slice
and called_fct =
CallSrc of SlicingInternals.fct_info option
| CallSlice of SlicingInternals.fct_slice
and call_info = SlicingInternals.called_fct option
and marks_index =
(SlicingInternals.pdg_mark, SlicingInternals.call_info)
PdgIndex.FctIndex.t
and ff_marks = PdgTypes.Pdg.t * SlicingInternals.marks_index
and project = {
functions : SlicingInternals.fct_info Cil_datatype.Varinfo.Hashtbl.t;
mutable actions : SlicingInternals.criterion list;
}
and appli_criterion =
CaGlobalData of Locations.Zone.t
| CaCall of SlicingInternals.fct_info
| CaOther
and fct_base_criterion = SlicingInternals.pdg_mark PdgMarks.select
and loc_point = Cil_types.stmt * Locations.Zone.t * bool
and node_or_dpds = CwNode | CwAddrDpds | CwDataDpds | CwCtrlDpds
and fct_user_crit =
CuSelect of SlicingInternals.pdg_mark PdgMarks.select
| CuTop of SlicingInternals.pdg_mark
and fct_crit =
CcUserMark of SlicingInternals.fct_user_crit
| CcChooseCall of Cil_types.stmt
| CcChangeCall of Cil_types.stmt * SlicingInternals.called_fct
| CcMissingOutputs of Cil_types.stmt *
SlicingInternals.pdg_mark PdgMarks.select * bool
| CcMissingInputs of Cil_types.stmt *
SlicingInternals.pdg_mark PdgMarks.select * bool
| CcPropagate of SlicingInternals.pdg_mark PdgMarks.select
| CcExamineCalls of
SlicingInternals.pdg_mark PdgMarks.info_called_outputs
and fct_criterion = {
cf_fct : SlicingInternals.fct_id;
cf_info : SlicingInternals.fct_crit;
}
and criterion =
CrAppli of SlicingInternals.appli_criterion
| CrFct of SlicingInternals.fct_criterion
val dummy_pdg_mark : SlicingInternals.pdg_mark
val dummy_fct_info : SlicingInternals.fct_info
val dummy_marks_index :
(SlicingInternals.pdg_mark, SlicingInternals.call_info)
PdgIndex.FctIndex.t
val dummy_ff_marks :
PdgTypes.Pdg.t *
(SlicingInternals.pdg_mark, SlicingInternals.call_info)
PdgIndex.FctIndex.t
val dummy_fct_slice : SlicingInternals.fct_slice
val dummy_fct_user_crit : SlicingInternals.fct_user_crit
val dummy_project : SlicingInternals.project
end