package frama-c

  1. Overview
  2. Docs
On This Page
  1. Public types
Legend:
Library
Module
Module type
Parameter
Class
Class type

Slicing module types.

exception Slicing_Internal_Error of string
exception ChangeCallErr of string
exception PtrCallExpr
exception CantRemoveCalledFf
exception WrongSlicingLevel
exception OnlyOneEntryPointSlice

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

exception 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.

type 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.

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

type sl_fct_slice = SlicingInternals.fct_slice

Function slice

Marks : used to put 'colors' in the result

val pp_sl_project : Frama_c_kernel.Type.precedence -> Stdlib.Format.formatter -> 'a -> unit
val pp_sl_fct_slice : Frama_c_kernel.Type.precedence -> Stdlib.Format.formatter -> SlicingInternals.fct_slice -> unit
val dyn_sl_fct_slice : Sl_fct_slice.t Frama_c_kernel.Type.t