sail

Sail is a language for describing the instruction semantics of processors
IN THIS PACKAGE
Module Jib_smt
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 = {
lbits_index : int;
lint_size : int;
vector_index : int;
register_map : Ast.id list Jib_util.CTMap.t;
tuple_sizes : IntSet.t ref;
tc_env : Type_check.Env.t;
pragma_l : Ast.l;
arg_stack : (int * string) Stack.t;
ast : Type_check.tannot Ast_defs.ast;
shared : Jib.ctyp Ast_util.Bindings.t;
preserved : Ast_util.IdSet.t;
events : Smtlib.smt_exp Stack.t EventMap.t ref;
node : int;
pathcond : Smtlib.smt_exp Lazy.t;
use_string : bool ref;
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