package binsec

You can search for identifiers within the package.

in-package search v0.2.0

Semantic analysis of binary executables

Install

Dune Dependency

binsec.github.io Readme Changelog LGPL-2.1-or-later License Edit opam file Versions (18)

Authors

Maintainers

B

BINSEC <binsec@saxifrage.saclay.cea.fr>

Sources

binsec-0.6.0.tbz

sha256=e9101e68d317c837d5cff9608c6fba2127dd31ef6373b9b90806780c1d80bb52

sha512=c01af277239b8cc84fb904c301897f7d2388a8c850c7cb6a53acb8a4f8d51115c8a595c5517843d076421a76f4b2becb16e722b4c90f19a8fa208cce5f3ba274

doc/binsec.smt/Smt/Smt_bitwuzla/index.html

Module `Smt.Smt_bitwuzla`Source

Sourceval available : bool

available is true if Bitwuzla binding is available.

include Smt_sig.Solver

Sourcetype t

Sourceval open_session : unit -> t

open_session () creates a new incremental solver instance.

returns
A new stateful solver instance.

Sourceval 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.

Sourceval 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.

Sourceval get_bv_value : t -> Binsec.Formula.bv_term -> Binsec.Bitvector.t

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.

Source

val get_ax_values : 
  t ->
  Binsec.Formula.ax_term ->
  (Binsec.Bitvector.t * Binsec.Bitvector.t) array

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.

Sourceval 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.

Sourceval 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.

Sourceval query_stat : unit -> int

query_stat () returns the cumulated number of check_sat issued.

returns
The total number of satisfiability queries.

Sourceval 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.