Module SpecificAbstract

module SpecificAbstract: sig .. end

Methods which depend of the abstract domain. Foundations of the static interpretation.

val lastStat : Types.generic_stat_loc Pervasives.ref

Last statement read. Is used to give an explicit error with the statement concerned.

val alpha : Types.realD -> Types.abstrD

Abstraction of a real element

real_elem The real element

Returns The abstract element which corresponds to the real one

val join : Types.abstrD -> Types.abstrD -> Types.abstrD

Joins two abstract domains

a1 The first abstract domain
a2 The second abstract domain

Returns The join of the two abstract domains

val meet : Types.abstrD -> Types.abstrD -> Types.abstrD

Meets two abstract domains

a1 The first abstract domain
a2 The second abstract domain

Returns The meet of the two abstract domains

val isInAbstractDomain : Z.t -> Types.abstrD -> bool

Return true iff n is the abstract domain p. The concretization function appears here.

n A number (not really a real domain which is a set of numbers)
p The abstract domain

Returns Is the number in the abstract domain

val faexpUna : Types.arithOpArithUna -> Types.abstrD -> Types.abstrD

Forward abstract semantics of arithmetic unary operators

op The arithmetic unary operator
a The abstract domain of the operand

Returns The abstract domain after the application of the operator on the abstract domain provided

val faexpBin : Types.abstrD -> Types.arithOpArithBin -> Types.abstrD -> Types.abstrD

Forward abstract semantics of arithmetic binary operators

a1 The abstract domain of the first operand
op The arithmetic binary operator
a2 The abstract domain of the second operand

Returns The abstract domain after the application of the operator on the two operands

val abexpArithBin : Types.abstrD ->
       Types.boolOpArithBin -> Types.abstrD -> Types.abstrD * Types.abstrD

Specific abstract interpretation of binary boolean operators with arithmetics operands

a1 The abstract domain of the first operand
op The arithmetic to boolean binary operator
a2 The abstract domain of the second operand

Returns The pair made of the abstract domain of both operand which respect the property, which is this boolean expression, or an over-approximation of that

val baexpUna : Types.arithOpArithUna -> Types.abstrD -> Types.abstrD -> Types.abstrD

Backward abstract semantics of arithmetic unary operators

op The arithmetic unary operator
a The abstract domain of the operand
p The abstract domain in which we want the result of the operation

Returns The abstract domain of the operand which satisfied the fact that op a is in p or an over-approximation of it

val baexpBin : Types.abstrD ->
       Types.arithOpArithBin ->
       Types.abstrD -> Types.abstrD -> Types.abstrD * Types.abstrD

Backward abstract semantics of arithmetic binary operators

a1 The abstract domain of the first operand
op The arithmetic to boolean binary operator
a2 The abstract domain of the second operand
p The abstract domain in which we want the result of the operation

Returns The pair made of the abstract domain for both operands which satistfied the fact that a1 op a2 is in p or an over-approximation of it

val widening : Types.abstrD -> Types.abstrD -> Types.abstrD

The widening function which ensure termination of lfp

a1 The first abstract domain
a2 The second abstract domain

Returns The abstract domain which is the application of the widening on the abstract domains provided