package frama-c
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
Platform dedicated to the analysis of source code written in C
Install
dune-project
Dependency
Authors
-
MMichele Alberti
-
TThibaud Antignac
-
GGergö Barany
-
PPatrick Baudin
-
NNicolas Bellec
-
TThibaut Benjamin
-
AAllan Blanchard
-
LLionel Blatter
-
FFrançois Bobot
-
RRichard Bonichon
-
VVincent Botbol
-
QQuentin Bouillaguet
-
DDavid Bühler
-
ZZakaria Chihani
-
SSylvain Chiron
-
LLoïc Correnson
-
JJulien Crétin
-
PPascal Cuoq
-
ZZaynah Dargaye
-
BBasile Desloges
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
MMaxime Jacquemin
-
BBenjamin Jorge
-
FFlorent Kirchner
-
AAlexander Kogtenkov
-
RRemi Lazarini
-
TTristan Le Gall
-
KKilyan Le Gallic
-
JJean-Christophe Léchenet
-
MMatthieu Lemerre
-
DDara Ly
-
DDavid Maison
-
CClaude Marché
-
AAndré Maroneze
-
TThibault Martin
-
FFonenantsoa Maurica
-
MMelody Méaulle
-
BBenjamin Monate
-
YYannick Moy
-
PPierre Nigron
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
DDario Pinto
-
VVirgile Prevosto
-
AArmand Puccetti
-
FFélix Ridoux
-
VVirgile Robles
-
JJan Rochel
-
MMuriel Roger
-
CCécile Ruet-Cros
-
JJulien Signoles
-
FFabien Siron
-
NNicolas Stouls
-
HHugo Thievenaz
-
KKostyantyn Vorobyov
-
BBoris Yakobowski
Maintainers
Sources
frama-c-32.0-beta-Germanium.tar.gz
sha256=868d57ef8007fe6c0836cd151d8c294003af34aa678285eff9547662cad36aa3
doc/src/frama-c-slicing.core/register.ml.html
Source file register.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150(**************************************************************************) (* *) (* SPDX-License-Identifier LGPL-2.1 *) (* Copyright (C) *) (* CEA (Commissariat à l'énergie atomique et aux énergies alternatives) *) (* *) (**************************************************************************) (* Basic plug-in internal documentation at the end of this file. *) (** Find a unique name to export the sliced project into. The name is derived from the given [project_name] and the [ExportedProjectPostfix] parameter. *) let get_sliced_project_name project_name = let sliced_project_name = project_name ^ (SlicingParameters.ExportedProjectPostfix.get ()) in let rec aux s idx = match Project.find_all s with | [] -> s | _ :: _ -> let idx = succ idx in let s = Format.asprintf "%s %d" s idx in aux s idx in aux sliced_project_name 1 let main () = if SlicingParameters.is_on () then begin SlicingParameters.feedback ~level:1 "slicing requests in progress..."; (* have to do the value analysis before the selections * because some functions use its results, * and the value analysis is not launched automatically. *) Eva.Analysis.compute (); let project_name = SlicingParameters.ProjectName.get () in Api.Project.reset_slicing (); Api.Request.add_persistent_cmdline (); (* Apply all pending requests. *) if Api.Request.is_request_empty_internal () then begin SlicingParameters.warning "No internal slicing request from the command line." ; if SlicingParameters.Mode.Callers.get () then let kf_entry, _library = Globals.entry_point () in SlicingParameters.warning "Adding an extra request on the entry point of function: %a." Kernel_function.pretty kf_entry; let set = Api.Select.empty_selects in let set = Api.Select.select_func_calls_into set ~spare:true kf_entry in Api.Request.add_persistent_selection set end; Api.Request.apply_all_internal (); if SlicingParameters.Mode.Callers.get () then Api.Slice.remove_uncalled (); let sliced_project_name = get_sliced_project_name project_name in SlicingParameters.set_off (); let sliced_project = Api.Project.extract sliced_project_name in Project.on sliced_project SlicingParameters.clear (); SlicingParameters.feedback ~level:2 "done (slicing requests in progress)."; end (** Register the function [main] as a main entry point. *) let () = Boot.Main.extend main (* {2 Overview} To have more details about what we are trying to do, you may have a look to the specification report (in French). The internal types module ({!module:SlicingTypes.Internals}) can give a pretty good idea of the kind of objects that we deal with in this module. You can also find some general information below. {3 Project} The project was the global repository of the results obtained so far. If is mainly composed of a list of actions waiting to be applied, and the already computed slices. More precisely, see its type definition {!type:SlicingTypes.Internals.t_project} if you want to know what it is composed of, and the module {!module:SlicingProject} of the functions to handle it. {3 Program Dependence Graph} This computation is not part of this module anymore. See the {{:../html/Db.Pdg.html}API of Pdg module}. It is enough to know that the PDG of a function is a graph composed of nodes that represent the elements of a function (declarations, statements, and so on) and of edges that represent the dependencies relations between those elements. {3 Sliced function} A sliced function contains a mapping between the PDG nodes of a function and the some marks that are computed by the application of the actions. It also has a mapping between the function calls and the function called by the slice that can be either some other slices, or the source function (or nothing if the call is invisible in that slice). There can be more than one slice for a source function. See their type {!type:SlicingTypes.Internals.t_fct_slice}, and the associated functions in {!module:Fct_slice}. See also {!module:SlicingMarks} for more information about the low level marks computation. {3 Actions} The actions are the way of giving an order to modify the current application. There are many kinds of actions, but only one is really used to build the slice which is a list of nodes from the PDG of a function, and their associated marks. All the other actions dealing with the marks are first decomposed before being applied. Some other actions are can be used to manage the interprocedural part, ie. which slice to call where. See the top type {!type:SlicingTypes.Internals.t_criterion} or the functions in {!module:SlicingActions}. {3 Options} The propagation of the marks to the function call depend on a {!type:SlicingTypes.Internals.t_call_option}. Choosing this level makes it possible to obtain a more or less precise result. {3 High level commands} The module {!module:SlicingCmds} is a bit external because it only uses the {{:../html/Db.Pdg.html}slicing API} to define higher level function that are only a composition of the basic functions. {3 Producing a result } When there are non more actions in the task list, the project can be exported. This is done in {!module:SlicingTransform} module by building a new CIL application. *)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>