package cbat-vsa

  1. Overview
  2. Docs

cbat-vsa 0.1

Libraries

This package provides the following libraries (via ocamlobjinfo):

cbat-value-set

Documentation:

  • Cbat_vsa_utils
  • Cbat_word_ops
  • Cbat_lattice_intf
  • Cbat_wordset_intf
  • Cbat_clp This module implements Circular Linear Progressions in the style of 1 "Executable Analysis using Abstract Interpretation with Circular Linear Progressions" (http://www.csa.iisc.ernet.in/~cplse/papers/srikant-memocode-2007.pdf). The poset of CLPs is a superset of the poset of strided intervals that more precicely handles overflow and underflow.
  • Cbat_fin_set
  • Cbat_clp_set_composite
  • Cbat_map_lattice
  • Cbat_ai_memmap Cbat_ai_memmap Represents memory as an interval tree from ranges of addresses to CLPs with an endianness. Note that, while BAP breaks up its memory into constant size (usually 8-bit) regions, this module does not. This is because n*k-bit CLPs cannot be well-represented as k n-bit CLPs. For example, take the set
  • Cbat_ai_representation
  • Cbat_back_edges
  • Cbat_contextual_fixpoint
  • Cbat_vsa

cbat-plugin-value-set

Documentation:

OCaml

Innovation. Community. Security.