package binsec
Semantic analysis of binary executables
Install
Dune Dependency
Authors
-
AAdel Djoudi
-
BBenjamin Farinier
-
CChakib Foulani
-
DDorian Lesbre
-
FFrédéric Recoules
-
GGuillaume Girol
-
JJosselin Feist
-
LLesly-Ann Daniel
-
MMahmudul Faisal Al Ameen
-
MManh-Dung Nguyen
-
MMathéo Vergnolle
-
MMathilde Ollivier
-
MMatthieu Lemerre
-
NNicolas Bellec
-
OOlivier Nicole
-
RRichard Bonichon
-
RRobin David
-
SSébastien Bardin
-
SSoline Ducousso
-
TTa Thanh Dinh
-
YYaëlle Vinçont
-
YYanis Sellami
Maintainers
Sources
binsec-0.10.1.tbz
sha256=87d4048c9a90c8a14ee029e77d31032a15427f06416a31938cec8a68394234c4
sha512=6a023d2a5c87c56b0aac489874431d8dcccee1451a072a826190be3a7f75a961688bab95f193f494231744abc3bc9733ab5c809057d36a5e4d24c6c29c369144
doc/libsolver/Libsolver/module-type-F/index.html
Module type Libsolver.F
Source
A solver instance factory.
An incremental solver instance.
Parameters
Signature
val assert_formula : Bl.t -> unit
assert_formula bl
assert the boolean entry in the solver instance.
pop ()
discard all the assertions since the last backup point, restoring the solver context in the same state as before the push ()
. Invalid uses may fail in an unpredictable fashion.
val check_sat : ?timeout:float -> unit -> status
check_sat ()
checks if the current formula is satisfiable.
check_sat_assuming e
checks if the current formula is satisfiable with the assumtion e
.
val get_bv_value : Bv.t -> Z.t
get_bv_value expr
returns the assignment of the expression expr
if check_sat
returned Sat
. Invalid uses may fail in an unpredictable fashion.
val fold_ax_values : (Z.t -> Z.t -> 'a -> 'a) -> Ax.t -> 'a -> 'a
fold_ax_values f ax v
iter through the assignment of the array ax
if check_sat
returned Sat
. Invalid uses may fail in an unpredictable fashion.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page