package sail

You can search for identifiers within the package.

in-package search v0.2.0

package sail

sail
- Anf
- Ast
- Ast_util
  - BE
  - BESet
  - Bindings
  - Id
  - IdSet
  - KBindings
  - KOpt
  - KOptMap
  - KOptSet
  - Kid
  - KidSet
  - Kind
  - NC
  - NCMap
  - Nexp
  - NexpMap
  - NexpSet
  - Typ
  - TypMap
- Bitfield
- C_backend
- Cgen_backend
- Constant_fold
  - StringMap
- Constant_propagation
- Constant_propagation_mutrec
- Constraint
- Elf_loader
- Error_format
- Graph
  - Make
    
    Ord
  - OrderedType
  - S
- Initial_check
- Interactive
- Interpreter
- Jib
- Jib_compile
  - Config
  - Make
    
    C
- Jib_interactive
- Jib_ir
  - Flat_ir_config
  - Flat_ir_formatter
  - Ir_formatter
    
    Config
    
    Make
    
    C
  - StringMap
- Jib_optimize
- Jib_smt
  - EventMap
  - IntSet
  - Make_optimizer
    
    S
  - Sequence
- Jib_ssa
  - IntSet
- Jib_util
  - CT
  - CTMap
  - CTSet
  - Name
  - NameCT
  - NameCTMap
  - NameCTSet
  - NameMap
  - NameSet
  - UBindings
  - UId
- Latex
  - StringSet
- Lexer
  - M
- Manifest
- Monomorphise
- Nl_flow
- Ocaml_backend
- Optimize
- Parse_ast
- Parser
- Parser_combinators
- Pattern_completeness
- Pretty_print
- Pretty_print_common
- Pretty_print_coq
  - StringSet
- Pretty_print_lem
  - StringSet
- Pretty_print_sail
- Process_file
- Profile
- Property
  - Event
- Reporting
- Rewriter
- Rewrites
- Sail2_values
- Sail_lib
  - BitType
  - Mem
- Scattered
- Smtlib
- Spec_analysis
- Specialize
- State
- ToFromInterp_backend
- ToFromInterp_lib_bitlist
  - Make
    
    BitT
- ToFromInterp_lib_mword
- Type_check
  - Env
- Type_error
- Util
- Value
  - StringMap

Legend:
Library
Module
Module type
Parameter
Class
Class type

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 = {

lbits_index : int;
lint_size : int;
vector_index : int;
register_map : Ast.id list Jib_util.CTMap.t;
tuple_sizes : IntSet.t Stdlib.ref;
tc_env : Type_check.Env.t;
pragma_l : Ast.l;
arg_stack : (int * string) Stdlib.Stack.t;
ast : Type_check.tannot Ast.defs;
shared : Jib.ctyp Ast_util.Bindings.t;
preserved : Ast_util.IdSet.t;
events : Smtlib.smt_exp Stdlib.Stack.t EventMap.t Stdlib.ref;
node : int;
pathcond : Smtlib.smt_exp Stdlib.Lazy.t;
use_string : bool Stdlib.ref;
use_real : bool Stdlib.ref;

}

val compile : 
  Type_check.Env.t ->
  Type_check.tannot Ast.defs ->
  Jib.cdef list * Jib_compile.ctx * ctx

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