package why3

  1. Overview
  2. Docs
package why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
val field : int -> string
val aliases : C.ty Ident.Hid.t
val array : Ident.attribute
val array_mk : Ident.attribute
val likely : Ident.attribute
val unlikely : Ident.attribute
val decl_attribute : Ident.attribute
val ty_of_ty : info -> Ty.ty -> C.ty
val ty_of_mlty : info -> Mltree.ty -> C.ty
val struct_of_rs : info -> Expr.Wrs.key -> C.struct_def
val ity_of_expr : Mltree.expr -> Ity.ity
val pv_name : Ity.pvsymbol -> Ident.ident
val is_constructor : Expr.rsymbol -> Pdecl.its_defn -> bool
val is_struct_constructor : info -> Expr.rsymbol -> bool
val struct_of_constructor : info -> Expr.rsymbol -> C.struct_def
type syntax_env = {
  1. in_unguarded_loop : bool;
  2. computes_return_value : bool;
  3. current_function : Expr.rsymbol;
  4. ret_regs : Ity.Sreg.t;
  5. breaks : Ident.Sid.t;
  6. returns : Ident.Sid.t;
  7. array_sizes : C.expr Ident.Mid.t;
  8. boxed : unit Ity.Hreg.t;
}
val is_true : Mltree.expr -> bool
val is_false : Mltree.expr -> bool
val is_unit : Mltree.ity -> bool
val handle_likely : Ident.Sattr.t -> C.expr -> C.expr
val reverse_likely : C.expr -> C.expr
val expr_or_return : syntax_env -> C.expr -> C.stmt
val ity_escapes_from_expr : syntax_env -> Ity.ity -> Mltree.expr -> bool
val var_escapes_from_expr : syntax_env -> Ity.pvsymbol -> Mltree.expr -> bool
val expr : info -> syntax_env -> Mltree.expr -> C.body
val translate_decl : info -> Mltree.decl -> header:bool -> C.definition list
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct