sail
  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
val opt_ignore_overflow : bool ref
val opt_auto : bool ref
val opt_debug_graphs : bool ref
val opt_propagate_vars : bool ref
val zencode_name : Jib.name -> string
module IntSet : sig ... end
module EventMap : sig ... end
val opt_default_lint_size : int ref
val opt_default_lbits_index : int ref
val opt_default_vector_index : int 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 ref;
  6. tc_env : Type_check.Env.t;
  7. pragma_l : Ast.l;
  8. arg_stack : (int * string) Stack.t;
  9. ast : Type_check.tannot Ast_defs.ast;
  10. shared : Jib.ctyp Ast_util.Bindings.t;
  11. preserved : Ast_util.IdSet.t;
  12. events : Smtlib.smt_exp Stack.t EventMap.t ref;
  13. node : int;
  14. pathcond : Smtlib.smt_exp Lazy.t;
  15. use_string : bool ref;
  16. use_real : bool 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 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.ast -> 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.ast -> unit