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.1.tbz

sha256=ebc732ef78d3f6d94a0d179f8ef76a74dedd4d23f9783c3875091695c1ceee56

sha512=cf91afa2223681c9b50b71429d739fc37c792264e43f72212ac405088d3de5c9f04d40ef6ae92526c727569982d48d1678811341b5d9b4bbc596fbc55d45b79e

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.