package soteria

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

Module Encoding.Make

Lowers the svalues of a built typed layer Typed (from Typed.Make) into SMT terms and sorts for the Z3 backend.

Parameters

module Typed : sig ... end

Signature

val pointers_not_supported : unit -> 'a
module Svalue = Typed.Svalue
type t = Svalue.t
type ty = Svalue.ty
val sort_of_ty : Svalue.ty -> Smt.sexp
val memo_encode_value_tbl : Smt.sexp Soteria.Soteria_std.Hashtbl.Hint.t
val smt_of_unop : Bv_values.Svalue.Unop.t -> Smt.sexp -> Smt.sexp
val encode_var : Soteria.Symex.Var.t -> Smt.sexp
val encode_value_memo : (Svalue.ghost, Svalue.ghost Typed.Ext.t, Svalue.ghost Typed.Ext.ty) Soteria__Bv_values__Svalue.t_node Hc.hash_consed -> Smt.sexp
val encode_value : Svalue.t -> Smt.sexp
val init_commands : 'a list