interpolants

Type Members

1. class ArraySimplifier extends Simplifier

   

   Even more extended version of the InputAbsy simplifier that also rewrites certain array expression.

2. class BitvectorSimplifier extends CollectingVisitor[Unit, (IExpression, Option[Interval])]

   

   Class to simplify bit-vector expressions using information about the range of operands.

   Class to simplify bit-vector expressions using information about the range of operands. In particular, bit-vector operations are replaced with simple Presburger operations if it is guaranteed that no overflows can occur

3. abstract class ConcurrentProgram extends AnyRef

   

4. class ExtArraySimplifier extends Simplifier

   

   Even more extended version of the InputAbsy simplifier that also rewrites certain array expression.

5. class FrameworkVocabulary extends AnyRef

   

6. class InterpolantSimplifier extends Simplifier

   

   Extended version of the InputAbsy simplifier that also rewrites certain array expressions: \exists int a; x = store(a, b, c) is replaced with select(x, b) = c

7. class InterpolationContext extends AnyRef

   

8. case class Interval(lower: IdealInt, upper: IdealInt) extends Product with Serializable

   

9. class NonInterferenceChecker extends SoftwareInterpolationFramework

   

10. class NonInterferenceChecker2 extends SoftwareInterpolationFramework

    

11. class PartialInterpolant extends AnyRef

    

    Class representing the different kinds of partial interpolants that are used to annotate arithmetic literals.

    Class representing the different kinds of partial interpolants that are used to annotate arithmetic literals. A partial interpolant carries a "denominator", which represents a factor that the annotated arithmetic literal has to be multiplied with to make the partial interpolant valid. E.g. x = 0 [y = 0, 2] can be interpreted as equivalent to 2*x = 0 [y = 0, 1].

12. class PredicateCollector extends CollectingVisitor[Unit, Unit]

    

13. class PredicateReplace extends CollectingVisitor[Unit, IExpression]

    

14. class SigTracker extends AnyRef

    

15. abstract class SoftwareInterpolationFramework extends AnyRef

    

    Abstract class providing some functionality commonly needed for interpolation-based software verification, e.g., axioms and prover for bitvector arithmetic, arrays, etc.

16. class SymbolRangeEnvironment extends AnyRef

    

    Class to store information about the value range of constants; this information is later used to simplify expressions

17. class WolverineInterpolantLineariser extends CollectingVisitor[List[String], Unit]