package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Public types

Module `Slicing.SlicingTypes`Source

Slicing module types.

Sourceexception Slicing_Internal_Error of string

Sourceexception ChangeCallErr of string

Sourceexception PtrCallExpr

Sourceexception CantRemoveCalledFf

Sourceexception WrongSlicingLevel

Sourceexception OnlyOneEntryPointSlice

raised when someone tries to build more than one slice for the entry point. *

Sourceexception NoPdg

raised when one tries to select something in a function where we are not * able to compute the Pdg.

Public types

* These types are the only one that should be used by the API functions. * Public type definitions should be hidden to the outside world, * but it is not really possible to have abstract types since Slicing has to * use Db.Slicing functions... So, it is up to the user of this module to use * only this public part.

Sourcetype sl_project = SlicingInternals.project

contains global things that has been computed so far for the slicing project. This includes :

the slices of the functions,
and the queue of actions to be applied.

Source

type sl_select =
  Frama_c_kernel.Cil_types.varinfo * SlicingInternals.fct_user_crit

Type of the selections * (we store the varinfo because we cannot use the kernel_function in this file) *

module Fct_user_crit : 
  Frama_c_kernel.Datatype.S with type t = SlicingInternals.fct_user_crit

Sourcetype sl_fct_slice = SlicingInternals.fct_slice

Function slice

Sourcetype sl_mark = SlicingInternals.pdg_mark

Marks : used to put 'colors' in the result

Source

val pp_sl_project : 
  Frama_c_kernel.Type.precedence ->
  Format.formatter ->
  'a ->
  unit

module Sl_project : Frama_c_kernel.Datatype.S with type t = sl_project

module Sl_select : Frama_c_kernel.Datatype.S with type t = sl_select

Source

val pp_sl_fct_slice : 
  Frama_c_kernel.Type.precedence ->
  Format.formatter ->
  SlicingInternals.fct_slice ->
  unit

module Sl_fct_slice : 
  Frama_c_kernel.Datatype.S with type t = SlicingInternals.fct_slice

Sourceval dyn_sl_fct_slice : Sl_fct_slice.t Frama_c_kernel.Type.t

module Sl_mark : 
  Frama_c_kernel.Datatype.S_with_collections
    with type t = SlicingInternals.pdg_mark

Sourceval dyn_sl_mark : Sl_mark.t Frama_c_kernel.Type.t

package frama-c

Module Slicing.SlicingTypesSource

Public types

Module `Slicing.SlicingTypes`Source