package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 : filename:string -> 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 : Format.formatter -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct