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

sha256=d959c2351b6cac10ffbdaf112769a676c9ad84bf6bc7fefa5cb1daa8d086cc97

sha512=1a3951896f05fb3a4cb05e81830373c75409a69c49323dc82e97c94889927b5f9561e704565a22c2a608842f67063d6c89a330477165b197a40d6ac231c09a7e

doc/libterm/Libterm/Api_solver/Context/argument-1-S/Bv/index.html

Module `S.Bv`

type t

val const : int -> string -> t

const size name creates the (first-order) constant of size bits named name .

val value : int -> Z.t -> t

value sz bv creates a constant from the bitvector value bv of size sz.

include Binsec.Sigs.COMPARISON with type t := t and type boolean := Bl.t

val equal : t -> t -> Bl.t

val diff : t -> t -> Bl.t

val ule : t -> t -> Bl.t

val uge : t -> t -> Bl.t

val ult : t -> t -> Bl.t

val ugt : t -> t -> Bl.t

val sle : t -> t -> Bl.t

val sge : t -> t -> Bl.t

val slt : t -> t -> Bl.t

val sgt : t -> t -> Bl.t

include Binsec.Sigs.ARITHMETIC with type t := t

val add : t -> t -> t

val sub : t -> t -> t

val mul : t -> t -> t

val neg : t -> t

val udiv : t -> t -> t

val umod : t -> t -> t

val urem : t -> t -> t

val sdiv : t -> t -> t

val smod : t -> t -> t

val srem : t -> t -> t

include Binsec.Sigs.EXTENDED_LOGICAL with type t := t

include Binsec.Sigs.LOGICAL with type t := t

val logand : t -> t -> t

val logor : t -> t -> t

val lognot : t -> t

val logxor : t -> t -> t

val lognand : t -> t -> t

lognand x y creates the nand bitvector operation between x and y.

val lognor : t -> t -> t

lognor x y creates the nor bitvector operation between x and y.

val logxnor : t -> t -> t

logxnor x y creates the xnor bitvector operation between x and y.

include Binsec.Sigs.SHIFT_ROT with type t := t and type index := t

val shift_left : t -> t -> t

val shift_right : t -> t -> t

val shift_right_signed : t -> t -> t

val rotate_left : t -> t -> t

val rotate_right : t -> t -> t

val rotate_lefti : t -> int -> t

rotate_lefti x i same as rotate_left but with a constant index.

val rotate_righti : t -> int -> t

rotate_righti x i same as rotate_right but with a constant index.

val append : t -> t -> t

append x y creates the concatenation of the two bitvectors x and y.

val extract : hi:int -> lo:int -> t -> t

extract ~hi ~lo x extracts the sub-bitvector of x starting from bit lo and ending at bit hi (included).

val uext : int -> t -> t

uext n x zero-extends the bitvector x by adding n bits.

val sext : int -> t -> t

sext n x sign extends the bitvector x copying n times the most significant bit.

val ite : Bl.t -> t -> t -> t

ite x y z creates the bitvector ite operation between y and z according to x.

val succ : t -> t

succ x creates the bitvector x + 1 operation.

val to_bl : t -> Bl.t

to_bl x cast the 1-bit bitvector x as a boolean.