Basic integer arithmetic on N-bit integers

High level interface to libasmir.

Constants for asmir.ml.

Lift a program using recursive disassembly.

Asmir variables

The Abstract Syntax Tree.

Utility functions for ASTs.

Apply a mapping to all expressions in a program.

Convert AST programs to the Piqi serialization format, which can convert to protobuffers, xml, and json.

A module to perform chopping on ASTs

Visitor for AST programs and expressions.

Opening this module will put a more tail-recursive List module into scope.

Convenience functions for Big_ints

Control flow graphs.

Conversions from AST programs to AST CFGs and vice versa.

Pretty printing for CFGs.

Static Single Assignment translation

Sanity checks to provide more understandable error messages

Coalesce sequential basic blocks into a single basic block.

Dead code elimination for SSA graphs.

Debugging module.

Snippets of debugging code

Dependency graphs.

General disassembly stuff

Native lifter of x86 instructions to the BAP IL

Dominator module for use with the ocamlgraph library.

Break complicated memory write statements a series of flat ones of form Store(Var v, ...).

Printing formulas

Function boundary identification for x86

Forward weakest preconditions.

Dijkstra's Guarded Command Language

Define a Scope solely for the Parser and its helper functions.

Scope module for parsing.

Dataflow module for use with the ocamlgraph library

Dataflow module for use with the ocamlgraph library widening

Hacks

Use this to read in a program.

Convert Type.TMem memories to Type.Array memories.

Bap interface to the parser.

Pretty printing

Code for removing unreachable nodes in a CFG.

Reachability analysis

Strongly connected component based value numbering.

Interface for executing command line driven SMT solvers.

Output to SMTLIB1 format

Output to SMTLIB2 format

Primary interface to SMT solvers.

Static Single Assignment form.

SSA simplifications

Misc optimizations

A module to perform chopping on SSAs

Visitor for SSA programs and expressions.

Steensgard's loop nesting algorithm

Output to STP format (same as CVCL or CVC3)

Structural Analysis

A module to perform AST Symbolic Execution

A module to try out search strategies on symbolic execution

Statically identify obvious use of system call numbers on AST CFGs.

A module with IL models of system calls.

Functions used by BAP library and tests

C output.

A module to perform trace analysis

Backwards taint analysis on traces.

Functions for streaming processing of traces.

Transformations needed for traces.

Automatically tune Garbage collection parameters.

Type declarations for BAP.

Type checking and inference for AST programs.

Loop unrolling

Utility functions that are not BAP specific.

The type of variables.

Recognizing and creating temporary variables

Interface to verification generation procedures.

Value-Set Analysis / Value-Set Arithmetic

Functions for computing the weakest preconditions (WPs) of programs.