package frama-c

  1. Overview
  2. Docs

doc/frama-c-e-acsl.core/E_ACSL/Gmp/index.html

Module E_ACSL.Gmp

Calls to the GMP's API.

build stmt mpz_init(v) or mpq_init(v) depending on typ of v

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

build stmt mpz_clear(v) or mpq_clear(v) depending on typ of v

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
OCaml

Innovation. Community. Security.