why3 1.3.0 · OCaml Package

type struct_def = string * (string * ty) list

and ty =

| Tvoid
| Tsyntax of string * ty list
| Tptr of ty
| Tarray of ty * expr
| Tstruct of struct_def
| Tunion of Ident.ident * (Ident.ident * ty) list
| Tnamed of Ident.ident
| Tmutable of ty
| Tnosyntax

and names = ty * (Ident.ident * expr) list

and name = ty * Ident.ident * expr

and proto = ty * (ty * Ident.ident) list

and binop =

| Band
| Bor
| Beq
| Bne
| Bassign
| Blt
| Ble
| Bgt
| Bge

and unop =

| Unot
| Ustar
| Uaddr
| Upreincr
| Upostincr
| Upredecr
| Upostdecr

and expr =

| Enothing
| Eunop of unop * expr
| Ebinop of binop * expr * expr
| Equestion of expr * expr * expr
| Ecast of ty * expr
| Ecall of expr * expr list
| Econst of constant
| Evar of Ident.ident
| Elikely of expr
| Eunlikely of expr
| Esize_expr of expr
| Esize_type of ty
| Eindex of expr * expr
| Edot of expr * string
| Earrow of expr * string
| Esyntaxrename of string * expr list
| Esyntax of string * ty * ty array * (expr * ty) list * int list

and constant =

| Cint of string
| Cfloat of string
| Cchar of string
| Cstring of string

type stmt =

| Snop
| Sexpr of expr
| Sblock of body
| Sseq of stmt * stmt
| Sif of expr * stmt * stmt
| Swhile of expr * stmt
| Sfor of expr * expr * expr * stmt
| Sbreak
| Sreturn of expr

and include_kind =

| Sys
| Proj

and definition =

| Dfun of Ident.ident * proto * body
| Dinclude of Ident.ident * include_kind
| Dproto of Ident.ident * proto
| Ddecl of names
| Dstruct of struct_def
| Dstruct_decl of string
| Dtypedef of ty * Ident.ident

and body = definition list * stmt

type file = definition list

exception NotAValue

val is_nop : stmt -> bool

val is_true : stmt -> bool

val is_false : stmt -> bool

val one_stmt : stmt -> bool

val assignify : expr -> stmt -> stmt

val get_last_expr : stmt -> stmt * expr

val propagate_in_expr : Ident.ident -> expr -> expr -> expr

val propagate_in_stmt : Ident.ident -> expr -> stmt -> stmt

val propagate_in_def : Ident.ident -> expr -> definition -> definition * bool

val propagate_in_block : Ident.ident -> expr -> body -> body

val is_empty_block : stmt -> bool

val block_of_expr : expr -> 'a list * stmt

val flatten_defs : definition list -> stmt -> definition list * stmt

val group_defs_by_type : definition list -> definition list

val elim_empty_blocks : stmt -> stmt

val elim_nop : stmt -> stmt

val add_to_last_call : expr list -> stmt -> stmt

val stmt_of_list : stmt list -> stmt

val is_expr : stmt -> bool

val simplify_expr : ('a list * stmt) -> expr

val simplify_cond : ('a list * stmt) -> 'a list * stmt

val prec_unop : unop -> int

val prec_binop : binop -> int

val is_const_unop : unop -> bool

val is_const_binop : binop -> bool

val is_const_expr : expr -> bool

val get_const_expr : (definition list * stmt) -> expr

val has_unboxed_struct : ty -> bool

val has_array : ty -> bool

val should_not_escape : ty -> bool

val left_assoc : binop -> bool

val right_assoc : binop -> bool

val min32 : BigInt.t

val max32 : BigInt.t

val maxu32 : BigInt.t

val min64 : BigInt.t

val max64 : BigInt.t

val maxu64 : BigInt.t

package why3