package binsec

  1. Overview
  2. Docs
package binsec
Legend:
Library
Module
Module type
Parameter
Class
Class type
val available : bool

available is true if Bitwuzla binding is available.

include Smt_sig.Solver
type t
val open_session : unit -> t

open_session () creates a new incremental solver instance.

  • returns

    A new stateful solver instance.

val put : t -> Binsec.Formula.entry -> unit

put solver entry sends the entry to the solver.

  • parameter solver

    The solver instance.

  • parameter entry

    The formula entry to send.

val check_sat : t -> Binsec.Formula.status

check_sat solver checks if the current formula is satisfiable.

  • parameter solver

    The solver instance.

  • returns

    SAT, UNSAT or UNKNOWN.

get_bv_value solver expr returns the assignment of the expression expr if check_sat returned SAT. Invalid uses may fail in an unpredictable fashion.

  • parameter solver

    The solver instance that returned SAT.

  • parameter expr

    The expression to get the assignment.

  • returns

    The bitvector assignment of expr.

get_ax_values solver expr returns the assignment of the array expr if check_sat returned SAT. Invalid uses may fail in an unpredictable fashion.

  • parameter solver

    The solver instance that returned SAT.

  • parameter expr

    The expression to get the assignment.

  • returns

    The pair address/value assignments of expr.

val close_session : t -> unit

close_session solver will destroy the solver instance and release its ressources. Calling any function on this instance afterward is invalid and may fail in an unpredictable fashion.

  • parameter solver

    The solver instance to destroy.

val check_sat_and_close : t -> Binsec.Formula.status

check_sat_and_close solver is the same as caching the result of check_sat before calling close_session.

  • parameter solver

    The solver instance.

val query_stat : unit -> int

query_stat () returns the cumulated number of check_sat issued.

  • returns

    The total number of satisfiability queries.

val time_stat : unit -> float

time_stat () return the cumulated elapsed time with an open solver session.

  • returns

    The total number of second passed with an open solver session.

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