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:

• Cbat_value_set_plugin