package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c-slicing.core/Slicing/SlicingInternals/index.html

Module `Slicing.SlicingInternals`Source

Internals types

Internals type definitions should be hidden to the outside world.

About options

Sourcetype level_option =

| DontSlice
(*
don't build slice for the function : ie. always call the source function.
*)
| DontSliceButComputeMarks
(*
don't slice the called functions, but compute the marks for them
*)
| MinNbSlice
(*
try to use existing slices, create at most one
*)
| MaxNbSlice
(*
most precise slices (but merge slices with the same visibility, even if they don't have the same marks)
*)

associate a level to each function in order to control how it will be specialized. This is only a hint used when the tool has to make a choice, but it doesn't forbid to the user to do whatever he wants (like building slices for a DontSlice function).

About function slice

Sourcetype mark =

| Cav of Pdg_types.PdgTypes.Dpd.t
| Spare

Kinds of elementary marks.

Sourceval compare_mark : mark -> mark -> int

Sourcetype pdg_mark = {

m1 : mark;
m2 : mark;

}

Each PDG element has 2 marks to deal with interprocedural propagation

Sourceval pdg_mark_packed_descr : Frama_c_kernel.Structural_descr.pack

Sourceval compare_pdg_mark : pdg_mark -> pdg_mark -> int

Sourcetype fct_info = {

fi_kf : Frama_c_kernel.Cil_types.kernel_function;
fi_def : Frama_c_kernel.Cil_types.fundec option;
mutable fi_top : pdg_mark option;
(*
indicates if the function is marked top (=> src visible)
*)
mutable fi_level_option : level_option;
(*
level of specialisation for this function
*)
mutable fi_init_marks : ff_marks option;
(*
the marks that must be in every slices of that function
*)
mutable fi_slices : fct_slice list;
(*
the list of the slices already computed for this function.
*)
mutable fi_next_ff_num : int;
(*
the number to assign to the next slice.
*)
mutable f_called_by : called_by;
(*
calls in slices that call source fct
*)

}

Type for all the informations related to any function, even if we don't have its definition.

Sourceand called_by = (fct_slice * Frama_c_kernel.Cil_types.stmt) list

to represent where a function is called.

Sourceand fct_slice = {

ff_fct : fct_info;
ff_id : int;
mutable ff_marks : ff_marks;
mutable ff_called_by : called_by;

}

Function slice : created as soon as there is a criterion to compute it, even if the slice itself hasn't been computed yet.

Sourceand fct_id =

| FctSrc of fct_info
(*
source function
*)
| FctSliced of fct_slice
(*
sliced function
*)

fct_id is used to identify either a source function or a sliced one.

Sourceand called_fct =

| CallSrc of fct_info option
(*
call the source function (might be unknown if the call uses pointer)
*)
| CallSlice of fct_slice

Sourceand call_info = called_fct option

information about a call in a slice which gives the function to call

Sourceand marks_index = (pdg_mark, call_info) Pdg_types.PdgIndex.FctIndex.t

main part of a slice = mapping between the function elements and information about them in the slice.

Sourceand ff_marks = Pdg_types.PdgTypes.Pdg.t * marks_index

Sourceand project = {

functions : fct_info Frama_c_kernel.Cil_datatype.Varinfo.Hashtbl.t;
mutable actions : criterion list;

}

Sourceand appli_criterion =

| CaGlobalData of Frama_c_kernel.Locations.Zone.t
(*
select all that is necessary to compute the given location.
*)
| CaCall of fct_info
(*
select all that is necessary to call the given function. Its application generates requests to add persistent selection to all the function callers.
*)
| CaOther

Slicing criterion at the application level. When applied, they are translated into fct_criterion

Sourceand fct_base_criterion = pdg_mark Pdg_types.PdgMarks.select

Base criterion for the functions. These are the only one that can really generate function slices. All the other criteria are translated in more basic ones. Note that to build such a base criterion, the PDG has to be already computed.

Source

and loc_point =
  Frama_c_kernel.Cil_types.stmt * Frama_c_kernel.Locations.Zone.t * bool

Used to identify a location (zone) at a given program point. The boolean tell if the point is before (true) or after the statement

Sourceand node_or_dpds =

| CwNode
| CwAddrDpds
| CwDataDpds
| CwCtrlDpds

node_or_dpds tells how we want to select nodes, or some of their dependencies (see fct_user_crit).

Sourceand fct_user_crit =

| CuSelect of pdg_mark Pdg_types.PdgMarks.select
| CuTop of pdg_mark
(*
the function has probably no PDG, but we nonetheless give a mark to propagate
*)

Tells which marks we want to put in the slice of a function

Sourceand fct_crit =

| CcUserMark of fct_user_crit
(*
add marks to a slice
*)
| CcChooseCall of Frama_c_kernel.Cil_types.stmt
(*
have to choose what function to call here.
*)
| CcChangeCall of Frama_c_kernel.Cil_types.stmt * called_fct
(*
call the called_fct for the given call Cil_types.stmt
*)
| CcMissingOutputs of Frama_c_kernel.Cil_types.stmt * pdg_mark Pdg_types.PdgMarks.select * bool
(*
this call is affected to a function that doesn't compute enough outputs : we will have to choose between adding outputs to that slice, or call another one. The boolean tells if the modifications would change the visibility of some outputs.
*)
| CcMissingInputs of Frama_c_kernel.Cil_types.stmt * pdg_mark Pdg_types.PdgMarks.select * bool
(*
the function calls a slice that has been modified : and doesn't compute not enough inputs. We will have to choose between adding marks to this function, and call another slice. The boolean tells if the modifications would change the visibility of some inputs.
*)
| CcPropagate of pdg_mark Pdg_types.PdgMarks.select
(*
simply propagate the given marks
*)
| CcExamineCalls of pdg_mark Pdg_types.PdgMarks.info_called_outputs

kinds of actions that can be apply to a function

Sourceand fct_criterion = {

cf_fct : fct_id;
(*
Identification of the RESULT of this filter. When it a a slice, it might be an existing slice that will be modified, or a new one will be created during application. When it is the source function, it means what the criterion has to be applied on each existing slice, and stored into the initial marks of the function.
*)
cf_info : fct_crit;

}

Slicing criterion for a function.

Sourceand criterion =

| CrAppli of appli_criterion
| CrFct of fct_criterion

A slicing criterion is either an application level criterion, or a function level one.

Internals values

For the datatypes of these internals types

Sourceval dummy_pdg_mark : pdg_mark

Sourceval dummy_fct_info : fct_info

Sourceval dummy_marks_index : (pdg_mark, call_info) Pdg_types.PdgIndex.FctIndex.t