Module Bddapron

module Bddapron: sig .. end
Finite \& numerical expressions/properties on top of CUDD \& APRON


Expressions and abstract domains combining finite-type and numerical types.

Bddapron extends Bdd (manipulation of finite-type formula using BDDs) and Apron (numerical abstract domain library). It enables formula of numerical type, and it allows decisions on numerical constraints in formula.

It can be seen as an extension of the APRON abstract domain for dealing with Boolean and finite-type variables, in addition to numerical variables.

Module Apronexpr: Purely arithmetic expressions (internal)

module Apronexpr: sig .. end

Module Env: Normalized variable managers/environments

module Env: sig .. end

Module Cond: Normalized condition environments

module Cond: sig .. end

Module ApronexprDD: DDs on top of arithmetic expressions (internal)

module ApronexprDD: sig .. end

Module Common: Functions common to the two implementations of Combined Boolean/Numerical domain

module Common: sig .. end

Module ApronDD: DDs on top of Apron abstract values (internal)

module ApronDD: sig .. end

Module Expr0: Finite-type and arithmetical expressions

module Expr0: sig .. end

Module Expr1: Finite-type and arithmetical expressions with normalized environments

module Expr1: sig .. end

Module Expr2: Finite-type and arithmetical expressions with variable and condition environments

module Expr2: sig .. end

Module Descend: Recursive descend on sets of diagrams (internal)

module Descend: sig .. end

Module Mtbdddomain0: Boolean/Numerical domain, with MTBDDs over APRON values

module Mtbdddomain0: sig .. end

Module Bddleaf: Manipulation of lists of guards and leafs (internal)

module Bddleaf: sig .. end

Module Bdddomain0: Combined Boolean/Numerical domain, with lists of BDDs and APRON values

module Bdddomain0: sig .. end

Module Domain0: Boolean/Numerical domain: generic interface

module Domain0: sig .. end

Module Domainlevel1: Functor to transform an abstract domain interface from level 0 to level 1 (internal)

module Domainlevel1: sig .. end

Module Mtbdddomain1: Boolean/Numerical domain with normalized environment

module Mtbdddomain1: sig .. end

Module Bdddomain1: Boolean/Numerical domain with normalized environment

module Bdddomain1: sig .. end

Module Domain1: Boolean/Numerical domain with normalized environment

module Domain1: sig .. end

Module Formula: Extra-operations on formula

module Formula: sig .. end

Module Policy: Policies for BDDAPRON abstract values

module Policy: sig .. end

Module Syntax: Building BDDAPRON expressions from Abstract Syntax Trees

module Syntax: sig .. end

Module Yacc

module Yacc: sig .. end

Module Lex

module Lex: sig .. end

Module Parser: Parsing BDDAPRON expressions from strings (or lexing buffers)

module Parser: sig .. end