package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val ty_of_mlty : info -> Mltree.ty -> C.ty
val ty_of_ty : info -> Ty.ty -> C.ty
val ity_of_expr : Mltree.expr -> Ity.ity
val pv_name : Ity.pvsymbol -> Ident.ident
type syntax_env = {
  1. in_unguarded_loop : bool;
  2. computes_return_value : bool;
  3. current_function : Expr.rsymbol;
  4. breaks : Ident.Sid.t;
  5. returns : Ident.Sid.t;
}
val is_true : Mltree.expr -> bool
val is_false : Mltree.expr -> bool
val is_unit : Mltree.ity -> bool
val return_or_expr : syntax_env -> C.expr -> C.stmt
val likely : Ident.attribute
val unlikely : Ident.attribute
val handle_likely : Ident.Sattr.t -> C.expr -> C.expr
val reverse_likely : C.expr -> C.expr
val field : int -> string
val struct_of_rs : info -> Expr.Wrs.key -> string * (string * C.ty) list
val expr : info -> syntax_env -> Mltree.expr -> C.body
val translate_decl : info -> Mltree.decl -> C.definition list
OCaml

Innovation. Community. Security.