package sail

  1. Overview
  2. Docs
val opt_ignore_overflow : bool Stdlib.ref
val opt_auto : bool Stdlib.ref
val opt_debug_graphs : bool Stdlib.ref
val opt_propagate_vars : bool Stdlib.ref
val zencode_name : Jib.name -> string
module IntSet : sig ... end
module EventMap : sig ... end
val opt_default_lint_size : int Stdlib.ref
val opt_default_lbits_index : int Stdlib.ref
val opt_default_vector_index : int Stdlib.ref
type ctx = {
  1. lbits_index : int;
  2. lint_size : int;
  3. vector_index : int;
  4. register_map : Ast.id list Jib_util.CTMap.t;
  5. tuple_sizes : IntSet.t Stdlib.ref;
  6. tc_env : Type_check.Env.t;
  7. pragma_l : Ast.l;
  8. arg_stack : (int * string) Stdlib.Stack.t;
  9. ast : Type_check.tannot Ast.defs;
  10. shared : Jib.ctyp Ast_util.Bindings.t;
  11. preserved : Ast_util.IdSet.t;
  12. events : Smtlib.smt_exp Stdlib.Stack.t EventMap.t Stdlib.ref;
  13. node : int;
  14. pathcond : Smtlib.smt_exp Stdlib.Lazy.t;
  15. use_string : bool Stdlib.ref;
  16. use_real : bool Stdlib.ref;
}
val smt_header : ctx -> Jib.cdef list -> Smtlib.smt_def list
val smt_query : ctx -> Property.query -> Smtlib.smt_exp
val smt_instr_list : string -> ctx -> Jib.cdef list -> Jib.instr list -> Smtlib.smt_def Stdlib.Stack.t * int * (Jib_ssa.ssa_elem list * Jib_ssa.cf_node) Jib_ssa.array_graph
module type Sequence = sig ... end
module Make_optimizer (S : Sequence) : sig ... end
val serialize_smt_model : string -> Type_check.Env.t -> Type_check.tannot Ast.defs -> unit
val deserialize_smt_model : string -> Jib.cdef list * ctx
val generate_smt : (string * string * Ast.l * 'a Ast.val_spec) Ast_util.Bindings.t -> (string -> string) -> Type_check.Env.t -> Type_check.tannot Ast.defs -> unit
OCaml

Innovation. Community. Security.