package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Smt_gen.MakeSource

Parameters

module Config : CONFIG

Signature

Convert a Jib IR cval into an SMT expression

Sourceval int_size : Jib.ctyp -> int
Sourceval bv_size : Jib.ctyp -> int
Sourceval generic_vector_length : Jib.ctyp -> int
Sourceval smt_conversion : into:Jib.ctyp -> from:Jib.ctyp -> Smt_exp.smt_exp -> Smt_exp.smt_exp check_writer

Create an SMT expression that converts an expression of the jib type from into an SMT expression for the jib type into. Note that this function assumes that the input is of the correct type.

Sourceval builtin : ?allow_io:bool -> ?undefined:undefined_mode -> string -> (Jib.cval list -> Jib.ctyp -> Smt_exp.smt_exp check_writer) option

Compile a call to a Sail builtin function into an SMT expression implementing that call. Returns None if that builtin is unsupported by this module.