E_ACSL.Gmp
Calls to the GMP's API.
val init :
loc:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.stmt
build stmt mpz_init(v)
or mpq_init(v)
depending on typ of v
val init_set :
loc:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.lval ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.stmt
init_set x_as_lv x_as_exp e
builds stmt x = e
or mpz_init_set*(v, e)
or mpq_init_set*(v, e)
with the good function 'set' according to the type of e
val clear :
Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.stmt
build stmt mpz_clear(v)
or mpq_clear(v)
depending on typ of v
val assign :
loc:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.lval ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.stmt
assign x_as_lv x_as_exp e
builds stmt x = e
or mpz_set*(e)
or mpq_set*(e)
with the good function 'set' according to the type of e
module Z : sig ... end
module Q : sig ... end