package frama-c
Install
dune-project
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
sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2
doc/frama-c.kernel/Frama_c_kernel/Cil/CurrentLoc/index.html
Module Cil.CurrentLoc
A reference to the current location. If you are careful to set this to * the current location then you can use some built-in logging functions that * will print the location.
include State_builder.S
val self : State.tThe kind of the registered state.
val mark_as_computed : ?project:Project.t -> unit -> unitIndicate that the registered state will not change again for the given project (default is current ()).
val is_computed : ?project:Project.t -> unit -> boolReturns true iff the registered state will not change again for the given project (default is current ()).
Exportation of some inputs (easier use of State_builder.Register).
module Datatype : Datatype.Sval add_hook_on_update : (Datatype.t -> unit) -> unitAdd an hook which is applied each time (just before) the project library changes the local value of the state.
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unithowto_marshal marshal unmarshal registers a custom couple of functions (marshal, unmarshal) to be used for serialization. Default functions are identities. In particular, this function must be used if Datatype.t is not marshallable and do_not_save is not called.
type data = Cil_types.locationType of the referenced value.
val set : data -> unitChange the referenced value.
val get : unit -> dataGet the referenced value.