Frama-C API - 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.stmtbuild 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.stmtinit_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.stmtbuild 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.stmtassign 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 ... endmodule Q : sig ... end