package frama-c
Platform dedicated to the analysis of source code written in C
Install
Dune Dependency
Authors
-
MMichele Alberti
-
TThibaud Antignac
-
GGergö Barany
-
PPatrick Baudin
-
TThibaut Benjamin
-
AAllan Blanchard
-
LLionel Blatter
-
FFrançois Bobot
-
RRichard Bonichon
-
QQuentin Bouillaguet
-
DDavid Bühler
-
ZZakaria Chihani
-
LLoïc Correnson
-
JJulien Crétin
-
PPascal Cuoq
-
ZZaynah Dargaye
-
BBasile Desloges
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
MMaxime Jacquemin
-
FFlorent Kirchner
-
AAlexander Kogtenkov
-
TTristan Le Gall
-
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
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
DDario Pinto
-
VVirgile Prevosto
-
AArmand Puccetti
-
FFélix Ridoux
-
VVirgile Robles
-
MMuriel Roger
-
JJulien Signoles
-
NNicolas Stouls
-
KKostyantyn Vorobyov
-
BBoris Yakobowski
Maintainers
Sources
frama-c-27.1-Cobalt.tar.gz
sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2
doc/frama-c-slicing.core/Slicing/Fct_slice/index.html
Module Slicing.Fct_slice
Source
Return true
if the source function is called * (even indirectly via transitivity) from a Slice.t
.
Return true
if the source function is visible * (even indirectly via transitivity) from a Slice.t
.
Source
val make_new_ff :
SlicingInternals.fct_info ->
bool ->
SlicingInternals.fct_slice * SlicingInternals.criterion list
Source
val merge_slices :
SlicingInternals.fct_slice ->
SlicingInternals.fct_slice ->
SlicingInternals.fct_slice * SlicingInternals.criterion list
Source
val filter_already_in :
SlicingInternals.fct_slice ->
SlicingInternals.fct_base_criterion ->
SlicingInternals.fct_base_criterion
Source
val apply_add_marks :
SlicingInternals.fct_slice ->
SlicingInternals.fct_base_criterion ->
SlicingInternals.criterion list
Source
val add_marks_to_fi :
SlicingInternals.fct_info ->
SlicingInternals.fct_base_criterion ->
bool ->
SlicingInternals.criterion list ->
bool * SlicingInternals.criterion list
Source
val add_top_mark_to_fi :
SlicingInternals.fct_info ->
SlicingInternals.pdg_mark ->
bool ->
SlicingInternals.criterion list ->
SlicingInternals.criterion list
Source
val check_outputs_before_change_call :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
SlicingInternals.fct_slice ->
SlicingInternals.criterion list
Source
val apply_change_call :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
SlicingInternals.called_fct ->
SlicingInternals.criterion list
Source
val apply_choose_call :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
SlicingInternals.criterion list
Source
val apply_missing_inputs :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
(SlicingInternals.fct_base_criterion * bool) ->
SlicingInternals.criterion list
Source
val apply_missing_outputs :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
SlicingInternals.fct_base_criterion ->
bool ->
SlicingInternals.criterion list
Source
val apply_examine_calls :
SlicingInternals.fct_slice ->
SlicingInternals.pdg_mark Pdg_types.PdgMarks.info_called_outputs ->
SlicingInternals.criterion list
Source
val get_called_slice :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
SlicingInternals.fct_slice option * bool
Source
val get_node_mark :
SlicingInternals.fct_slice ->
Pdg_types.PdgTypes.Node.t ->
SlicingInternals.pdg_mark
Source
val get_node_key_mark :
SlicingInternals.fct_slice ->
Pdg_types.PdgIndex.Key.t ->
SlicingInternals.pdg_mark
Source
val get_stmt_mark :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
SlicingInternals.pdg_mark
Source
val get_label_mark :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.label ->
SlicingInternals.pdg_mark
Source
val get_local_var_mark :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.varinfo ->
SlicingInternals.pdg_mark
Source
val get_input_loc_under_mark :
SlicingInternals.fct_slice ->
Frama_c_kernel.Locations.Zone.t ->
SlicingInternals.pdg_mark
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>