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 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