package frama-c
Install
Dune 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
-
LLoïc Correnson
-
JJulien Crétin
-
PPascal Cuoq
-
ZZaynah Dargaye
-
BBasile Desloges
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
MMaxime Jacquemin
-
FFlorent Kirchner
-
AAlexander Kogtenkov
-
RRemi Lazarini
-
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
-
PPierre Nigron
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
DDario Pinto
-
VVirgile Prevosto
-
AArmand Puccetti
-
FFélix Ridoux
-
VVirgile Robles
-
JJan Rochel
-
MMuriel Roger
-
JJulien Signoles
-
NNicolas Stouls
-
KKostyantyn Vorobyov
-
BBoris Yakobowski
Maintainers
Sources
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493
doc/frama-c.kernel/Frama_c_kernel/Alpha/index.html
Module Frama_c_kernel.Alpha
Alpha conversion.
This is the type of the elements that are recorded by the alpha conversion functions in order to be able to undo changes to the tables they modify. Useful for implementing scoping
This is the type of the elements of the alpha renaming table. These elements can carry some data associated with each occurrence of the name.
type 'a alphaTable =
(string, (string, 'a alphaTableData ref) Hashtbl.t) Hashtbl.t
type for alpha conversion table. We split the lookup in two to avoid creating accidental collisions when converting x_0 into x_0_0 if the original code contains both.
val newAlphaName :
alphaTable:'a alphaTable ->
undolist:'a undoAlphaElement list ref option ->
lookupname:string ->
data:'a ->
string * 'a
Create a new name based on a given name. The new name is formed from a prefix (obtained from the given name by stripping a suffix consisting of _ followed by only digits), followed by a special separator and then by a positive integer suffix. The first argument is a table mapping name prefixes to some data that specifies what suffixes have been used and how to create the new one. This function updates the table with the new largest suffix generated. The "undolist" argument, when present, will be used by the function to record information that can be used by Alpha.undoAlphaChanges
to undo those changes. Note that the undo information will be in reverse order in which the action occurred. Returns the new name and, if different from the lookupname, the location of the previous occurrence. This function knows about the location implicitly from the (Current_loc.get ())
.
val registerAlphaName :
alphaTable:'a alphaTable ->
lookupname:string ->
data:'a ->
unit
Register a name with an alpha conversion table to ensure that when later we call newAlphaName we do not end up generating this one
Split the name in preparation for newAlphaName. Returns a pair (prefix, infix)
where prefix
is the index in the outer table, while infix is the index in the inner table.
val undoAlphaChanges :
alphaTable:'a alphaTable ->
undolist:'a undoAlphaElement list ->
unit
Undo the changes to a table