package frama-c
Platform dedicated to the analysis of source code written in 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
frama-c-27.0-beta-Cobalt.tar.gz
sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2
doc/frama-c-e-acsl.core/E_ACSL/Gmp/Z/index.html
Module Gmp.Z
val name_arith_bop : Frama_c_kernel.Cil_types.binop -> stringname_of_mpz_arith_bop bop returns the name of the GMP integer function corresponding to the bop arithmetic operation.
val new_var :
loc:Frama_c_kernel.Cil_types.location ->
?scope:Varname.scope ->
?name:string ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.term option ->
(Frama_c_kernel.Cil_types.varinfo ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.stmt list) ->
Frama_c_kernel.Cil_types.varinfo * Frama_c_kernel.Cil_types.exp * Env.tSame as Env.new_var, but dedicated to mpz_t variables initialized by Mpz.init.
val create :
loc:Frama_c_kernel.Cil_types.location ->
?name:string ->
Frama_c_kernel.Cil_types.term option ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp * Env.tCreate an integer number.
val add_cast :
loc:Frama_c_kernel.Cil_types.location ->
?name:string ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.typ ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp * Env.tAssumes that the given exp is of integer type and casts it into the given typ
val binop :
loc:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.term option ->
Frama_c_kernel.Cil_types.binop ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp * Env.tApplies binop to the given expressions. The optional term indicates whether the comparison has a correspondance in the logic.
val cmp :
loc:Frama_c_kernel.Cil_types.location ->
string ->
Frama_c_kernel.Cil_types.term option ->
Frama_c_kernel.Cil_types.binop ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp * Env.tCompares two expressions according to the given binop. The optional term indicates whether the comparison has a correspondance in the logic.