package binsec

  1. Overview
  2. Docs
Semantic analysis of binary executables

Install 

dune-project
 Dependency

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

Authors

  1. A
    Adel Djoudi
  2. B
    Benjamin Farinier
  3. C
    Chakib Foulani
  4. D
    Dorian Lesbre
  5. F
    Frédéric Recoules
  6. G
    Guillaume Girol
  7. J
    Josselin Feist
  8. L
    Lesly-Ann Daniel
  9. M
    Manh-Dung Nguyen
  10. M
    Mathéo Vergnolle
  11. M
    Mathilde Ollivier
  12. M
    Matthieu Lemerre
  13. O
    Olivier Nicole
  14. R
    Richard Bonichon
  15. R
    Robin David
  16. S
    Sébastien Bardin
  17. S
    Soline Ducousso
  18. T
    Ta Thanh Dinh
  19. Y
    Yaëlle Vinçont

Maintainers

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

Sources

binsec-0.8.2.tbz
sha256=b8e7b9c756245656c481e992549fb7b1864ee6eeb492e16488e7a9d962d39cdb
sha512=07a5e4105e5275751fcc6832743f5f9eedc72bd061273ec54c4466135032852120df3784ba571656c788e5f3cd971aad8a53f030336a364e77e940e26dff38d7

doc/binsec/Binsec/Dba/LValue/index.html

Module Dba.LValue

type t = private
  1. | Var of Var.t
  2. | Restrict of Var.t * int Interval.t
  3. | Store of size * Machine.endianness * Expr.t * string option
include Sigs.Eq with type t := t
val equal : t -> t -> bool
val size_of : t -> int

size_of lv yields the size of lv in bits *

val var : ?tag:Var.Tag.t -> bitsize:Size.Bit.t -> string -> t

var tag name ~size creates a DBA lvalue for a variable

val v : Var.t -> t
val flag : ?bitsize:Size.Bit.t -> string -> t

flag ~size fname creates a flag variable.

  • size defaults to 1
val temporary : string -> Size.Bit.t -> t
val _restrict : string -> Size.Bit.t -> int -> int -> t
val _bit_restrict : string -> Size.Bit.t -> int -> t

_restrict and _bit_restrict are deprecated. Use the other forms ** below.

val restrict : Var.t -> int -> int -> t
val bit_restrict : Var.t -> int -> t
val store : ?array:string -> Size.Byte.t -> Machine.endianness -> Expr.t -> t
val temp : Size.Bit.t -> t

temp n creates a lvalue representing a temporary of size n with name Format.sprintf "temp%d" n.

val is_expr_translatable : Expr.t -> bool

is_expr_translatable e returns true is the expression can have a valid lvalue translation

val of_expr : Expr.t -> t

of_expr e translates an expression to its lvalue equivalent if possible.

Use is_expr_translatable e to check the feasability of this translation.

  • raises Failure

    "LValue.of_expr ..." if it is not possible.

val to_expr : t -> Expr.t

to_expr e translates an lvalue to its equivalent rvalue.

val bitsize : t -> Size.Bit.t

bitsize lv returns the size in bits of lv.

val resize : Size.Bit.t -> t -> t

resize bitsize lv patches the lvalue lv and gives it a size of bitsize.