package binsec

  1. Overview
  2. Docs
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

  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
    Mahmudul Faisal Al Ameen
  10. M
    Manh-Dung Nguyen
  11. M
    Mathéo Vergnolle
  12. M
    Mathilde Ollivier
  13. M
    Matthieu Lemerre
  14. N
    Nicolas Bellec
  15. O
    Olivier Nicole
  16. R
    Richard Bonichon
  17. R
    Robin David
  18. S
    Sébastien Bardin
  19. S
    Soline Ducousso
  20. T
    Ta Thanh Dinh
  21. Y
    Yaëlle Vinçont
  22. Y
    Yanis Sellami

Maintainers

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

Sources

binsec-0.9.1.tbz
sha256=a6ccc9c0a756f6056a5bf6a2f602d59690944f4164cc180d0082c36f081e7e94
sha512=cd85654f94da9ce8fedab746c557c326821cc7932005337303607e0c52d7caf403655fc1000b34d32f1f2606ab1b3d079b9057346ef0a2f88057e0dd7b412cce

doc/binsec.domains/Domains/Interval/index.html

Module Domains.Interval

type t = private {
  1. min : Z.t;
  2. max : Z.t;
  3. stride : int;
}

Represents the unsigned fixed-width integer interval between min and max, with stride fixed bits.

include S with type t := t
val pp : Format.formatter -> t -> unit
val included : size:int -> t -> t -> bool

included ~size t t' tests if all values in t are in t'.

val disjoint : size:int -> t -> t -> bool

disjoint ~size t t' returns true if the intersection between t and t' is empty.

val union : size:int -> t -> t -> t
val inter : size:int -> t -> t -> t

inter ~size t t' returns the intersection of the intervals t and t'.

  • raises [Empty]

    If there is no intersection.

val is_zero : t -> trilean

is_zero t checks if t is the least significant bit is 0

val project : size:int -> t -> projection
val top : int -> t
val constant : size:int -> Z.t -> t
val zero : t
val one : t
val uminus : size:int -> t -> t
val uminus_feedback : size:int -> t -> t -> t
val add : size:int -> t -> t -> t
val add_feedback : size:int -> t -> t -> t -> t * t
val sub : size:int -> t -> t -> t
val sub_feedback : size:int -> t -> t -> t -> t * t
val mul : size:int -> t -> t -> t
val mul_feedback : size:int -> t -> t -> t -> t * t
val smod : size:int -> t -> t -> t
val smod_feedback : size:int -> t -> t -> t -> t * t
val umod : size:int -> t -> t -> t
val umod_feedback : size:int -> t -> t -> t -> t * t
val udiv : size:int -> t -> t -> t
val udiv_feedback : size:int -> t -> t -> t -> t * t
val sdiv : size:int -> t -> t -> t
val sdiv_feedback : size:int -> t -> t -> t -> t * t
val append : size1:int -> t -> size2:int -> t -> t
val append_feedback : size1:int -> t -> size2:int -> t -> t -> t * t
val equal : size:int -> t -> t -> t
val equal_feedback : size:int -> t -> t -> t -> t * t
val diff : size:int -> t -> t -> t
val diff_feedback : size:int -> t -> t -> t -> t * t
val ule : size:int -> t -> t -> t
val ule_feedback : size:int -> t -> t -> t -> t * t
val uge : size:int -> t -> t -> t
val uge_feedback : size:int -> t -> t -> t -> t * t
val ult : size:int -> t -> t -> t
val ult_feedback : size:int -> t -> t -> t -> t * t
val ugt : size:int -> t -> t -> t
val ugt_feedback : size:int -> t -> t -> t -> t * t
val sle : size:int -> t -> t -> t
val sle_feedback : size:int -> t -> t -> t -> t * t
val sge : size:int -> t -> t -> t
val sge_feedback : size:int -> t -> t -> t -> t * t
val slt : size:int -> t -> t -> t
val slt_feedback : size:int -> t -> t -> t -> t * t
val sgt : size:int -> t -> t -> t
val sgt_feedback : size:int -> t -> t -> t -> t * t
val logand : size:int -> t -> t -> t
val logand_feedback : size:int -> t -> t -> t -> t * t
val logor : size:int -> t -> t -> t
val logor_feedback : size:int -> t -> t -> t -> t * t
val lognot : size:int -> t -> t
val lognot_feedback : size:int -> t -> t -> t
val logxor : size:int -> t -> t -> t
val logxor_feedback : size:int -> t -> t -> t -> t * t
val shift_left : size:int -> t -> t -> t
val shift_left_feedback : size:int -> t -> t -> t -> t * t
val shift_right : size:int -> t -> t -> t
val shift_right_feedback : size:int -> t -> t -> t -> t * t
val shift_right_signed : size:int -> t -> t -> t
val shift_right_signed_feedback : size:int -> t -> t -> t -> t * t
val rotate_left : size:int -> t -> t -> t
val rotate_left_feedback : size:int -> t -> t -> t -> t * t
val rotate_right : size:int -> t -> t -> t
val rotate_right_feedback : size:int -> t -> t -> t -> t * t
val uext : int -> size:int -> t -> t
val uext_feedback : int -> size:int -> t -> t -> t
val sext : int -> size:int -> t -> t
val sext_feedback : int -> size:int -> t -> t -> t
val restrict : lo:int -> hi:int -> size:int -> t -> t
val restrict_feedback : lo:int -> hi:int -> size:int -> t -> t -> t
val zeros : int -> t
val ones : int -> t
val create : size:int -> min:Z.t -> max:Z.t -> stride:int -> t
val mem : Z.t -> size:int -> t -> bool
val iter : (Z.t -> unit) -> size:int -> t -> unit
val fold : (Z.t -> 'a -> 'a) -> 'a -> size:int -> t -> 'a
val for_all : (Z.t -> bool) -> size:int -> t -> bool
val sum : size:int -> t -> Z.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct