Module Bddapron

module Bddapron: sig .. end

Finite \& numerical expressions/properties on top of CUDD \& APRON

Introduction

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

Bddapron.Env: environment defining finite-type variables and user-defined enumerated types, and mapping them to BDDs indices;
Bddapron.Cond: environment defining numerical conditions, and mapping them to BDDs indices;
Bddapron.Expr0: general finite-type and numerical expressions;
Bddapron.Domain0: abstract domains combining Cudd BDDs and Apron numerical abstract domains; two implemented combinations: Bddapron.Bdddomain0, Bddapron.Mtbdddomain0;
Bddapron.Expr1, Bddapron.Domain1, Bddapron.Bdddomain1, Bddapron.Mtbdddomain1: incorporate normalized environments;
Bddapron.Expr2: incorporates in addition normalized condition environment
Bddapron.Syntax: Abstract Syntax Tree for expressions
Bddapron.Parser: converting strings to expressions

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

Module Bddapron

Introduction

Module Apronexpr: Purely arithmetic expressions (internal)

Module Env: Normalized variable managers/environments

Module Cond: Normalized condition environments

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

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

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

Module Expr0: Finite-type and arithmetical expressions

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

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

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

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

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

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

Module Domain0: Boolean/Numerical domain: generic interface

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

Module Mtbdddomain1: Boolean/Numerical domain with normalized environment

Module Bdddomain1: Boolean/Numerical domain with normalized environment

Module Domain1: Boolean/Numerical domain with normalized environment

Module Formula: Extra-operations on formula

Module Policy: Policies for BDDAPRON abstract values

Module Syntax: Building BDDAPRON expressions from Abstract Syntax Trees

Module Yacc

Module Lex

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