package binsec

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

Module Binsec.Dba_to_formula

Convert some DBA structure to Smtlib

exception NoSmtEquivalent

Raised if trying to convert DBA operators that don't have equivalent in smtlib2. The two operators that don't have equivalent are: Dba.LeftRotate and Dba.RightRotate that can take a variable shift value while smtlib2 only support constant

convert a DBA unary operator to a Smtlib unary operator

val binary : Dba.Binary_op.t -> [ `Unop of Formula.bv_unop | `Bnop of Formula.bv_bnop | `Comp of Formula.bv_comp ]

convert a DBA binary operator to a Smtlib binary operator

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct