package cbat-vsa

  1. Overview
  2. Docs

cbat-vsa 0.1


This package provides the following libraries (via ocamlobjinfo):



  • 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" ( 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




Innovation. Community. Security.