package libsail

You can search for identifiers within the package.

in-package search v0.2.0

package libsail

libsail
- Libsail
  - Anf
  - Ast
  - Ast_defs
  - Ast_util
    
    Bindings
    
    Id
    
    IdSet
    
    KBindings
    
    KOpt
    
    KOptMap
    
    KOptSet
    
    Kid
    
    KidSet
    
    Kind
    
    NC
    
    NCMap
    
    Nexp
    
    NexpMap
    
    NexpSet
    
    Scanner
    
    Loc
    
    Typ
    
    TypMap
  - Bitfield
  - Callgraph
    
    G
    
    Node
    
    NodeMap
    
    NodeSet
  - Chunk_ast
  - Constant_fold
    
    StringMap
  - Constant_propagation
  - Constant_propagation_mutrec
  - Constraint
  - Effects
    
    EffectSet
  - Elf_loader
  - Error_format
  - Format_sail
    
    CONFIG
    
    Make
    
    Config
  - Frontend
    
    FILE_HANDLER
  - Graph
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Infix_parser
    
    Incremental
    
    MenhirInterpreter
  - Initial_check
  - Interactive
    
    State
  - Interpreter
    
    Printer
  - Jib
  - Jib_compile
    
    CONFIG
    
    IdGraph
    
    Make
    
    C
  - Jib_optimize
  - Jib_ssa
    
    NameGraph
  - Jib_util
    
    CTListSet
    
    CTMap
    
    CTSet
    
    Name
    
    NameCTMap
    
    NameCTSet
    
    NameMap
    
    NameSet
  - Jib_visitor
    
    common_visitor
    
    empty_jib_visitor
    
    jib_visitor
  - Lexer
    
    M
  - Libsail_sites
    
    Sites
  - Mappings
  - Monad_params
  - Monomorphise
  - Nl_flow
  - Outcome_rewrites
  - Parse_ast
    
    Attribute_data
  - Parser
  - Parser_combinators
  - Pattern_completeness
    
    Config
    
    Make
    
    C
  - Preprocess
  - Pretty_print_common
  - Pretty_print_sail
    
    Default_print_config
    
    Document
    
    PRINT_CONFIG
    
    Printer
    
    Config
  - Profile
  - Project
    
    ModId
    
    ModSet
  - Project_lexer
    
    M
  - Project_parser
  - Property
    
    Event
  - Reporting
    
    Position
  - Rewriter
  - Rewrites
  - Sail2_instr_kinds
  - Sail2_operators
  - Sail2_operators_bitlists
  - Sail2_prompt
  - Sail2_prompt_monad
  - Sail2_values
  - Sail_file
    
    In_channel
  - Sail_lib
    
    BitType
    
    Mem
  - Scattered
  - Smt_exp
    
    COUNTEREXAMPLE_CONFIG
    
    Counterexample
    
    Config
  - Smt_gen
    
    CONFIG
    
    Make
    
    Config
    
    Primop_gen
    
    PRIMOP_GEN
  - Spec_analysis
  - Specialize
  - Splice
  - State
  - Target
  - Type_check
    
    Env
  - Type_env
  - Type_error
  - Type_internal
  - Util
    
    Duplicate
    
    Option_monad
    
    State_monad
    
    S
  - Value
    
    StringMap
  - Value2
  - Visitor

Legend:
Library
Module
Module type
Parameter
Class
Class type

val zencode_id : Ast.id -> string

val zencode_upper_id : Ast.id -> string

val zencode_name : Jib.name -> string

type smt_typ =

| Bitvec of int
| Bool
| String
| Real
| Datatype of string * (string * (string * smt_typ) list) list
| Array of smt_typ * smt_typ

val mk_enum : string -> string list -> smt_typ

val mk_record : string -> (string * smt_typ) list -> smt_typ

val mk_variant : string -> (string * smt_typ) list -> smt_typ

type smt_array_info =

| Fixed of int

type smt_exp =

| Bool_lit of bool
| Bitvec_lit of Sail2_values.bitU list
| Real_lit of string
| String_lit of string
| Var of Jib.name
| Unit
| Member of Ast.id
| Fn of string * smt_exp list
| Ite of smt_exp * smt_exp * smt_exp
| SignExtend of int * int * smt_exp
| ZeroExtend of int * int * smt_exp
| Extract of int * int * smt_exp
| Tester of string * smt_exp
| Unwrap of Ast.id * bool * smt_exp
| Field of Ast.id * Ast.id * smt_exp
| Store of smt_array_info * string * smt_exp * smt_exp * smt_exp
| Empty_list
| Hd of string * smt_exp
| Tl of string * smt_exp

val var_id : Ast.id -> smt_exp

val fold_smt_exp : (smt_exp -> smt_exp) -> smt_exp -> smt_exp

val extract : int -> int -> smt_exp -> smt_exp

val bvnot : smt_exp -> smt_exp

val bvand : smt_exp -> smt_exp -> smt_exp

val bvor : smt_exp -> smt_exp -> smt_exp

val bvneg : smt_exp -> smt_exp

val bvadd : smt_exp -> smt_exp -> smt_exp

val bvsub : smt_exp -> smt_exp -> smt_exp

val bvmul : smt_exp -> smt_exp -> smt_exp

val bvudiv : smt_exp -> smt_exp -> smt_exp

val bvurem : smt_exp -> smt_exp -> smt_exp

val bvshl : smt_exp -> smt_exp -> smt_exp

val bvlshr : smt_exp -> smt_exp -> smt_exp

val bvult : smt_exp -> smt_exp -> smt_exp

val bvzero : int -> smt_exp

val bvones : int -> smt_exp

val bvone : int -> smt_exp

val smt_conj : smt_exp list -> smt_exp

val smt_disj : smt_exp list -> smt_exp

val simp_and : smt_exp list -> smt_exp

val simp_or : smt_exp list -> smt_exp

val simp_eq : smt_exp -> smt_exp -> bool option

val simp_fn : string -> smt_exp list -> smt_exp

val simp : (Jib.name -> smt_exp option) -> smt_exp -> smt_exp

type smt_def =

| Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp
| Declare_fun of string * smt_typ list * smt_typ
| Declare_const of Jib.name * smt_typ
| Define_const of Jib.name * smt_typ * smt_exp
| Declare_datatypes of string * (string * (string * smt_typ) list) list
| Assert of smt_exp

val declare_datatypes : smt_typ -> smt_def

val pp_sfun : string -> PPrint.document list -> PPrint.document

val pp_smt_typ : smt_typ -> PPrint.document

val pp_str_smt_typ : (string * smt_typ) -> PPrint.document

val pp_smt_exp : smt_exp -> PPrint.document

val pp_smt_def : smt_def -> PPrint.document

val string_of_smt_def : smt_def -> string

type counterexample_solver =

| Cvc5
| Cvc4
| Z3

val counterexample_command : counterexample_solver -> string

val counterexample_solver_from_name : string -> counterexample_solver option

module type COUNTEREXAMPLE_CONFIG = sig ... end

module Counterexample (Config : COUNTEREXAMPLE_CONFIG) : sig ... end