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 :
        ('-> Db.Slicing.Select.t -> '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