Frama-C:
Plug-ins:
Libraries:

Frama-C API - Project

Slicing project management.

val reset_slicing : unit -> unit

Init/reset a slicing project.

val change_slicing_level : Frama_c_kernel.Cil_types.kernel_function -> int -> unit

Change the slicing level of this function (see the -slicing-level option documentation to know the meaning of the number)

  • raises SlicingTypes.ExternalFunction

    if kf has no definition.

val extract : ?f_slice_names: (Frama_c_kernel.Cil_types.kernel_function -> bool -> int -> string) -> string -> Frama_c_kernel.Project.t

Build a new 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 print_dot : filepath:Frama_c_kernel.Filepath.t -> title:string -> unit

Print a representation of the slicing project (call graph) in a dot file which name is the given string.

No needs of Journalization

val default_slice_names : Frama_c_kernel.Cil_types.kernel_function -> bool -> int -> string

Return true iff the source function is called (even indirectly via transitivity) from a Slice.t.

val has_persistent_selection : Frama_c_kernel.Cil_types.kernel_function -> bool

Return true iff the source function has persistent selection

val is_directly_called_internal : Frama_c_kernel.Cil_types.kernel_function -> bool

Return true if the source function is directly (even via pointer function) called from a Slice.t.

Debug

val pretty : Stdlib.Format.formatter -> unit