package libsail

  1. Overview
  2. Docs


module Config : CONFIG


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.


Innovation. Community. Security.