package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type struct_def = string * (string * ty) list
and ty =
  1. | Tvoid
  2. | Tsyntax of string * ty list
  3. | Tptr of ty
  4. | Tarray of ty * expr
  5. | Tstruct of struct_def
  6. | Tunion of Ident.ident * (Ident.ident * ty) list
  7. | Tnamed of Ident.ident
  8. | Tnosyntax
and names = ty * (Ident.ident * expr) list
and name = ty * Ident.ident * expr
and proto = ty * (ty * Ident.ident) list
and binop =
  1. | Band
  2. | Bor
  3. | Beq
  4. | Bne
  5. | Bassign
  6. | Blt
  7. | Ble
  8. | Bgt
  9. | Bge
and unop =
  1. | Unot
  2. | Ustar
  3. | Uaddr
  4. | Upreincr
  5. | Upostincr
  6. | Upredecr
  7. | Upostdecr
and expr =
  1. | Enothing
  2. | Eunop of unop * expr
  3. | Ebinop of binop * expr * expr
  4. | Equestion of expr * expr * expr
  5. | Ecast of ty * expr
  6. | Ecall of expr * expr list
  7. | Econst of constant
  8. | Evar of Ident.ident
  9. | Elikely of expr
  10. | Eunlikely of expr
  11. | Esize_expr of expr
  12. | Esize_type of ty
  13. | Eindex of expr * expr
  14. | Edot of expr * string
  15. | Earrow of expr * string
  16. | Esyntax of string * ty * ty array * (expr * ty) list * bool
and constant =
  1. | Cint of string
  2. | Cfloat of string
  3. | Cchar of string
  4. | Cstring of string
type stmt =
  1. | Snop
  2. | Sexpr of expr
  3. | Sblock of body
  4. | Sseq of stmt * stmt
  5. | Sif of expr * stmt * stmt
  6. | Swhile of expr * stmt
  7. | Sfor of expr * expr * expr * stmt
  8. | Sbreak
  9. | Sreturn of expr
and include_kind =
  1. | Sys
  2. | Proj
and definition =
  1. | Dfun of Ident.ident * proto * body
  2. | Dinclude of Ident.ident * include_kind
  3. | Dproto of Ident.ident * proto
  4. | Ddecl of names
  5. | Dstruct of struct_def
  6. | 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
OCaml

Innovation. Community. Security.