package libsail

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

Parameters

module Config : CONFIG

Signature

Convert a Jib IR cval into an SMT expression

val int_size : Jib.ctyp -> int
val 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.

val builtin : 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.