package frama-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
sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2
doc/frama-c-wp.core/Wp/MemMemory/index.html
Module Wp.MemMemorySource
Theory
allocation tables
initialization tables
t_addr indexed array
Null address. Same as a_addr 0 0
Zero-offset base. Same as a_addr base 0
Constructor for { base ; offset }
Shift: a_shift a k adds k to a.offset
Returns the base
Returns the offset
Returns the offset in bytes from the logic offset (which is a memory cell index, actually)
Addr Producer Registration
Register simplifiers for functions producing addr terms:
~base esis the simplifier for(f es).base~offset esis the simplifier for(f es).offset~linear:trueregister simplifierf(f(p,i),k)=f(p,i+j)onf~equal a bis theset_eq_builtinforf
The equality builtin is wrapped inside a default builtin that compares f es by computing base and offset.
val register :
?base:(Lang.F.term list -> Lang.F.term) ->
?offset:(Lang.F.term list -> Lang.F.term) ->
?equal:(Lang.F.term -> Lang.F.term -> Lang.F.pred) ->
?linear:bool ->
Lang.lfun ->
unitFrame Conditions
frames ~addr are frame conditions for reading a value at address addr from a chunk of memory. The value read at addr have length offset, while individual element in memory chunk have type tau and offset length sizeof.
Memory variables use ~basename or "mem" by default.
val frames :
addr:Lang.F.term ->
offset:Lang.F.term ->
sizeof:Lang.F.term ->
?basename:string ->
Lang.F.tau ->
Sigs.frame listRange of Address
val separated :
shift:('a -> Ctypes.c_object -> Lang.F.term -> 'a) ->
addrof:('a -> Lang.F.term) ->
sizeof:(Ctypes.c_object -> Lang.F.term) ->
'a Sigs.rloc ->
'a Sigs.rloc ->
Lang.F.predval included :
shift:('a -> Ctypes.c_object -> Lang.F.term -> 'a) ->
addrof:('a -> Lang.F.term) ->
sizeof:(Ctypes.c_object -> Lang.F.term) ->
'a Sigs.rloc ->
'a Sigs.rloc ->
Lang.F.pred