Package

ap

interpolants

Permalink

package interpolants

Visibility
  1. Public
  2. All

Type Members

  1. class ArraySimplifier extends Simplifier

    Permalink

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

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

    Permalink

    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

    Permalink
  4. class FrameworkVocabulary extends AnyRef

    Permalink
  5. class InterpolantSimplifier extends Simplifier

    Permalink

    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

  6. class InterpolationContext extends AnyRef

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

    Permalink
  8. class NonInterferenceChecker extends SoftwareInterpolationFramework

    Permalink
  9. class NonInterferenceChecker2 extends SoftwareInterpolationFramework

    Permalink
  10. class PartialInterpolant extends AnyRef

    Permalink

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

  11. class PredicateCollector extends CollectingVisitor[Unit, Unit]

    Permalink
  12. class PredicateReplace extends CollectingVisitor[Unit, IExpression]

    Permalink
  13. class SigTracker extends AnyRef

    Permalink
  14. abstract class SoftwareInterpolationFramework extends AnyRef

    Permalink

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

  15. class SymbolRangeEnvironment extends AnyRef

    Permalink

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

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

    Permalink

Value Members

  1. object InterpolationContext

    Permalink
  2. object Interpolator

    Permalink
  3. object InterpolatorQE

    Permalink
  4. object Interval extends Serializable

    Permalink
  5. object NonInterferenceChecker

    Permalink
  6. object NonInterferenceChecker2

    Permalink
  7. object PartialInterpolant

    Permalink
  8. object PredicateCollector

    Permalink
  9. object PredicateReplace

    Permalink
  10. object ProofSimplifier

    Permalink

    Module for simplifying a proof (certificate) by eliminating as many rounding steps as possible; this is currently done in a rather naive way

  11. object ResourceFiles

    Permalink
  12. object StructuredPrograms

    Permalink
  13. object WolverineInterfaceMain extends SoftwareInterpolationFramework

    Permalink

Ungrouped