Module Biabduction

module Abs : sig ... end

Implementation of Abstraction Functions

module Absarray : sig ... end
module Attribute : sig ... end

Attribute manipulation in Propositions (i.e., Symbolic Heaps)

module BiabductionConfig : sig ... end
module BiabductionReporting : sig ... end
module BiabductionSummary : sig ... end
module Buckets : sig ... end

Classify bugs into buckets

module Builtin : sig ... end

Module for builtin functions with their symbolic execution handler

module BuiltinDefn : sig ... end
module Dom : sig ... end

Join and Meet Operators

module DotBiabduction : sig ... end
module Errdesc : sig ... end

Create descriptions of analysis errors

module Exceptions : sig ... end
module Interproc : sig ... end

Interprocedural Analysis

module JoinState : sig ... end

Object representing the status of the join operation

module Match : sig ... end

Implementation of "Smart" Pattern Matching for higher order singly-linked list predicate.

module Paths : sig ... end

Execution Paths

module Predicates : sig ... end
module Prop : sig ... end

Functions for Propositions (i.e., Symbolic Heaps)

module PropUtil : sig ... end
module Propgraph : sig ... end

Propositions seen as graphs

module Propset : sig ... end

Functions for Sets of Propositions with and without sharing

module Prover : sig ... end

Functions for Theorem Proving

module Rearrange : sig ... end

Re-arrangement and extension of structures with fresh variables

module RetainCycles : sig ... end
module RetainCyclesType : sig ... end
module State : sig ... end

State of symbolic execution

module SymExec : sig ... end

Symbolic Execution

module SymOp : sig ... end

Symbolic Operations and Failures: the units in which analysis work is measured

module Tabulation : sig ... end

Interprocedural footprint analysis

module Timeout : sig ... end

Handle timeout events