sig
module Nat :
sig
type t = string
val zero : Newspeak.Nat.t
val one : Newspeak.Nat.t
val of_string : string -> Newspeak.Nat.t
val of_int : int -> Newspeak.Nat.t
val of_big_int : Big_int.big_int -> Newspeak.Nat.t
val to_big_int : Newspeak.Nat.t -> Big_int.big_int
val add : Newspeak.Nat.t -> Newspeak.Nat.t -> Newspeak.Nat.t
val mul : Newspeak.Nat.t -> Newspeak.Nat.t -> Newspeak.Nat.t
val sub : Newspeak.Nat.t -> Newspeak.Nat.t -> Newspeak.Nat.t
val div : Newspeak.Nat.t -> Newspeak.Nat.t -> Newspeak.Nat.t
val neg : Newspeak.Nat.t -> Newspeak.Nat.t
val add_int : int -> Newspeak.Nat.t -> Newspeak.Nat.t
val mul_int : int -> Newspeak.Nat.t -> Newspeak.Nat.t
val compare : Newspeak.Nat.t -> Newspeak.Nat.t -> int
end
type t = Newspeak.file list * Newspeak.prog * Newspeak.size_t
and prog =
Newspeak.globals * (Newspeak.fid, Newspeak.fundec) Hashtbl.t *
Newspeak.specs
and globals = (string, Newspeak.gdecl) Hashtbl.t
and gdecl = Newspeak.typ * Newspeak.init_t
and fundec = Newspeak.ftyp * Newspeak.blk
and specs = Newspeak.assertion list
and assertion = Newspeak.spec_token list
and spec_token =
SymbolToken of char
| IdentToken of string
| VarToken of string
| CstToken of Newspeak.cte
and stmtkind =
Set of (Newspeak.lval * Newspeak.exp * Newspeak.scalar_t)
| Copy of (Newspeak.lval * Newspeak.lval * Newspeak.size_t)
| Decl of (string * Newspeak.typ * Newspeak.blk)
| ChooseAssert of (Newspeak.exp list * Newspeak.blk) list
| InfLoop of Newspeak.blk
| DoWith of (Newspeak.blk * Newspeak.lbl * Newspeak.blk)
| Goto of Newspeak.lbl
| Call of Newspeak.fn
and stmt = Newspeak.stmtkind * Newspeak.location
and blk = Newspeak.stmt list
and lval =
Local of Newspeak.vid
| Global of string
| Deref of (Newspeak.exp * Newspeak.size_t)
| Shift of (Newspeak.lval * Newspeak.exp)
and exp =
Const of Newspeak.cte
| Lval of (Newspeak.lval * Newspeak.scalar_t)
| AddrOf of (Newspeak.lval * Newspeak.size_t)
| AddrOfFun of (Newspeak.fid * Newspeak.ftyp)
| UnOp of (Newspeak.unop * Newspeak.exp)
| BinOp of (Newspeak.binop * Newspeak.exp * Newspeak.exp)
and cte = CInt of Newspeak.Nat.t | CFloat of (float * string) | Nil
and unop =
Belongs of Newspeak.bounds
| Coerce of Newspeak.bounds
| Not
| BNot of Newspeak.bounds
| PtrToInt of Newspeak.ikind
| IntToPtr of Newspeak.ikind
| Cast of (Newspeak.scalar_t * Newspeak.scalar_t)
and binop =
PlusI
| MinusI
| MultI
| DivI
| Mod
| PlusF of Newspeak.size_t
| MinusF of Newspeak.size_t
| MultF of Newspeak.size_t
| DivF of Newspeak.size_t
| BOr of Newspeak.bounds
| BAnd of Newspeak.bounds
| BXor of Newspeak.bounds
| Shiftlt
| Shiftrt
| PlusPI
| MinusPP
| Gt of Newspeak.scalar_t
| Eq of Newspeak.scalar_t
and fn = FunId of Newspeak.fid | FunDeref of (Newspeak.exp * Newspeak.ftyp)
and typ =
Scalar of Newspeak.scalar_t
| Array of (Newspeak.typ * Newspeak.length)
| Region of (Newspeak.field list * Newspeak.size_t)
and field = Newspeak.offset * Newspeak.typ
and scalar_t =
Int of Newspeak.ikind
| Float of Newspeak.size_t
| Ptr
| FunPtr
and init_t =
Zero
| Init of (Newspeak.offset * Newspeak.scalar_t * Newspeak.exp) list
and ftyp = Newspeak.typ list * Newspeak.typ option
and lbl = int
and vid = int
and fid = string
and file = string
and ikind = Newspeak.sign_t * Newspeak.size_t
and sign_t = Signed | Unsigned
and size_t = int
and offset = int
and length = int
and bounds = Newspeak.Nat.t * Newspeak.Nat.t
and location = string * int * int
val zero : Newspeak.exp
val one : Newspeak.exp
val zero_f : Newspeak.exp
val unknown_loc : Newspeak.location
val dummy_loc : string -> Newspeak.location
val domain_of_typ : Newspeak.sign_t * Newspeak.size_t -> Newspeak.bounds
val belongs : Newspeak.Nat.t -> Newspeak.bounds -> bool
val contains : Newspeak.bounds -> Newspeak.bounds -> bool
val negate : Newspeak.exp -> Newspeak.exp
val exp_of_int : int -> Newspeak.exp
val simplify_gotos : Newspeak.blk -> Newspeak.blk
val normalize_loops : Newspeak.blk -> Newspeak.blk
val simplify : Newspeak.blk -> Newspeak.blk
val simplify_exp : Newspeak.exp -> Newspeak.exp
val string_of_loc : Newspeak.location -> string
val string_of_bounds : Newspeak.bounds -> string
val string_of_cte : Newspeak.cte -> string
val string_of_scalar : Newspeak.scalar_t -> string
val string_of_typ : Newspeak.typ -> string
val string_of_ftyp : Newspeak.ftyp -> string
val string_of_exp : Newspeak.exp -> string
val string_of_lval : Newspeak.lval -> string
val string_of_stmt : Newspeak.stmt -> string
val string_of_blk : Newspeak.blk -> string
val dump : Newspeak.t -> unit
val dump_prog : Newspeak.prog -> unit
val dump_globals : Newspeak.globals -> unit
val dump_fundec : string -> Newspeak.fundec -> unit
val string_of_binop : Newspeak.binop -> string
class visitor :
object
method get_loc : unit -> Newspeak.location
method print_warning : string -> unit
method process_binop : Newspeak.binop -> unit
method process_exp : Newspeak.exp -> bool
method process_fn : Newspeak.fn -> bool
method process_fun : Newspeak.fid -> Newspeak.fundec -> bool
method process_fun_after : unit -> unit
method process_gdecl : string -> Newspeak.gdecl -> bool
method process_length : Newspeak.length -> unit
method process_lval : Newspeak.lval -> bool
method process_size_t : Newspeak.size_t -> unit
method process_stmt : Newspeak.stmt -> bool
method process_unop : Newspeak.unop -> unit
method raise_error : string -> unit
method set_loc : Newspeak.location -> unit
end
val visit_fun : Newspeak.visitor -> Newspeak.fid -> Newspeak.fundec -> unit
val visit_glb : Newspeak.visitor -> string -> Newspeak.gdecl -> unit
val visit : Newspeak.visitor -> Newspeak.prog -> unit
class builder :
object
method curloc : Newspeak.location
method process_blk : Newspeak.blk -> Newspeak.blk
method process_exp : Newspeak.exp -> Newspeak.exp
method process_global : string -> Newspeak.gdecl -> Newspeak.gdecl
method process_lval : Newspeak.lval -> Newspeak.lval
method process_offset : Newspeak.offset -> Newspeak.offset
method process_size_t : Newspeak.size_t -> Newspeak.size_t
method set_curloc : Newspeak.location -> unit
end
val build : Newspeak.builder -> Newspeak.prog -> Newspeak.prog
val build_gdecl : Newspeak.builder -> Newspeak.gdecl -> Newspeak.gdecl
val write : string -> Newspeak.t -> unit
val read : string -> Newspeak.t
val write_hdr :
Pervasives.out_channel ->
string list * (string, Newspeak.gdecl) Hashtbl.t * Newspeak.specs *
Newspeak.size_t -> unit
val write_fun :
Pervasives.out_channel -> Newspeak.fid -> Newspeak.fundec -> unit
val size_of_scalar :
Newspeak.size_t -> Newspeak.scalar_t -> Newspeak.size_t
val size_of : Newspeak.size_t -> Newspeak.typ -> Newspeak.size_t
val bind_var : string -> Newspeak.typ -> Newspeak.blk -> Newspeak.stmtkind
val build_call :
Newspeak.fid -> Newspeak.ftyp -> Newspeak.exp list -> Newspeak.blk
val build_main_call :
Newspeak.size_t -> Newspeak.ftyp -> string list -> Newspeak.blk
val create_cstr : string -> string -> string * Newspeak.gdecl
type alt_stmtkind =
While of (Newspeak.exp list * Newspeak.blk)
| Npk of Newspeak.stmtkind
type alt_blk = (Newspeak.alt_stmtkind * Newspeak.location) list
val convert_loops : Newspeak.blk -> Newspeak.alt_blk
val max_ikind : Newspeak.ikind -> Newspeak.ikind -> Newspeak.ikind
val collect_fid_addrof : Newspeak.prog -> Newspeak.fid list
end