Modifier and Type | Method and Description |
---|---|
AbstractDomainElement |
AbstractDomainLattice.abstractFrom(SymbolicExecutionState state,
Term term,
Services services)
Abstracts from a given element of the concrete domain by returning a
suitable abstract element.
|
AbstractDomainElement |
AbstractDomainLattice.fromString(java.lang.String s,
Services services)
Constructs an Abstract Domain Element from the given String
representation.
|
abstract AbstractDomainElement |
AbstractDomainLattice.join(AbstractDomainElement a,
AbstractDomainElement b)
A lattice join operation; finds an abstract element that is the least
upper bound of the set consisting of the elements a and b.
|
Modifier and Type | Method and Description |
---|---|
abstract java.util.Iterator<AbstractDomainElement> |
AbstractDomainLattice.iterator()
Iterates through the abstract domain elements of this abstract domain
starting by the smallest element; if an element b is returned by the
iterator after an element a, then either compare(a,b) == LTE, or
compare(a,b) == UNDEF must hold (i.e., b may not be smaller than a).
|
Modifier and Type | Method and Description |
---|---|
PartialComparator.PartialComparisonResult |
AbstractDomainLattice.compare(AbstractDomainElement a,
AbstractDomainElement b) |
static Term |
AbstractDomainLattice.getSideConditionForAxiom(SymbolicExecutionState state,
Term term,
AbstractDomainElement elem,
Services services)
Returns a side condition which has to hold if elem is a correct
abstraction for term.
|
abstract AbstractDomainElement |
AbstractDomainLattice.join(AbstractDomainElement a,
AbstractDomainElement b)
A lattice join operation; finds an abstract element that is the least
upper bound of the set consisting of the elements a and b.
|
Modifier and Type | Class and Description |
---|---|
class |
BooleanDomainElem
A domain element of the simple boolean lattice.
|
class |
Bottom
The Bottom element of the boolean lattice, representing
no boolean at all.
|
class |
False
The False element of the boolean lattice, representing
exactly the boolean false.
|
class |
Top
The Top element of the boolean lattice, representing
all booleans (i.e., true and false).
|
class |
True
The True element of the boolean lattice, representing
exactly the boolean true.
|
Modifier and Type | Field and Description |
---|---|
static AbstractDomainElement[] |
BooleanLattice.ABSTRACT_DOMAIN_ELEMS
All elements of this abstract domain.
|
Modifier and Type | Method and Description |
---|---|
AbstractDomainElement |
BooleanLattice.join(AbstractDomainElement elem1,
AbstractDomainElement elem2) |
Modifier and Type | Method and Description |
---|---|
java.util.Iterator<AbstractDomainElement> |
BooleanLattice.iterator() |
Modifier and Type | Method and Description |
---|---|
AbstractDomainElement |
BooleanLattice.join(AbstractDomainElement elem1,
AbstractDomainElement elem2) |
Modifier and Type | Class and Description |
---|---|
class |
AbstractPredicateAbstractionDomainElement
A base class for abstract domain elements in a predicate abstraction lattice.
|
class |
ConjunctivePredicateAbstractionDomainElement
An abstract domain element for a predicate abstraction lattice based on the
conjunction of predicates.
|
class |
DisjunctivePredicateAbstractionDomainElement
An abstract domain element for a predicate abstraction lattice based on the
disjunction of predicates.
|
class |
SimplePredicateAbstractionDomainElement
An abstract domain element for a predicate abstraction lattice encapsulating
exactly one abstraction predicate.
|
Modifier and Type | Method and Description |
---|---|
AbstractDomainElement |
DisjunctivePredicateAbstractionLattice.join(AbstractDomainElement a,
AbstractDomainElement b) |
AbstractDomainElement |
ConjunctivePredicateAbstractionLattice.join(AbstractDomainElement a,
AbstractDomainElement b) |
AbstractDomainElement |
SimplePredicateAbstractionLattice.join(AbstractDomainElement a,
AbstractDomainElement b) |
Modifier and Type | Method and Description |
---|---|
java.util.Iterator<AbstractDomainElement> |
DisjunctivePredicateAbstractionLattice.iterator()
The iterator for this lattice will first return the bottom element, then
all conjunctions of length n of the predicates, then all conjunctions of
length n-1, and so on, until finally the top element is returned.
|
java.util.Iterator<AbstractDomainElement> |
ConjunctivePredicateAbstractionLattice.iterator()
The iterator for this lattice will first return the bottom element, then
all conjunctions of length n of the predicates, then all conjunctions of
length n-1, and so on, until finally the top element is returned.
|
java.util.Iterator<AbstractDomainElement> |
SimplePredicateAbstractionLattice.iterator()
The iterator for this lattice will first return the bottom element, then
the given predicates in the order in which they have been initially
supplied, and finally the top element.
|
Modifier and Type | Method and Description |
---|---|
AbstractDomainElement |
DisjunctivePredicateAbstractionLattice.join(AbstractDomainElement a,
AbstractDomainElement b) |
AbstractDomainElement |
ConjunctivePredicateAbstractionLattice.join(AbstractDomainElement a,
AbstractDomainElement b) |
AbstractDomainElement |
SimplePredicateAbstractionLattice.join(AbstractDomainElement a,
AbstractDomainElement b) |
protected AbstractPredicateAbstractionDomainElement |
AbstractPredicateAbstractionLattice.join(AbstractDomainElement a,
AbstractDomainElement b,
java.util.function.BiFunction<ImmutableSet<AbstractionPredicate>,ImmutableSet<AbstractionPredicate>,ImmutableSet<AbstractionPredicate>> combiner,
java.util.function.Function<ImmutableSet<AbstractionPredicate>,AbstractPredicateAbstractionDomainElement> abstrElemConstructor)
Joins to abstract elements in the lattice.
|
Modifier and Type | Class and Description |
---|---|
class |
Geq
The Geq element of the sign lattice, representing
all positive integers and zero.
|
class |
Leq
The Leq element of the sign lattice, representing
all negative numbers and zero.
|
class |
Neg
The Neg element of the sign lattice, representing
all strictly negative integers.
|
class |
Pos
The Pos element of the sign lattice, representing
all strictly positive numbers.
|
class |
SignAnalysisDomainElem
A domain element for sign analysis.
|
class |
Zero
The Zero element of the sign lattice, representing
only the number 0.
|
Modifier and Type | Field and Description |
---|---|
static AbstractDomainElement[] |
SignAnalysisLattice.ABSTRACT_DOMAIN_ELEMS
All elements of this abstract domain.
|
Modifier and Type | Method and Description |
---|---|
AbstractDomainElement |
SignAnalysisLattice.join(AbstractDomainElement elem1,
AbstractDomainElement elem2) |
Modifier and Type | Method and Description |
---|---|
java.util.Iterator<AbstractDomainElement> |
SignAnalysisLattice.iterator() |
Modifier and Type | Method and Description |
---|---|
AbstractDomainElement |
SignAnalysisLattice.join(AbstractDomainElement elem1,
AbstractDomainElement elem2) |
Modifier and Type | Method and Description |
---|---|
abstract java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> |
MergeWithLatticeAbstraction.getUserChoices() |
java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> |
MergeWithPredicateAbstraction.getUserChoices() |
Modifier and Type | Method and Description |
---|---|
MergeWithPredicateAbstraction |
MergeWithPredicateAbstractionFactory.instantiate(java.lang.Iterable<AbstractionPredicate> predicates,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> userChoices)
Creates a complete instance of
MergeWithPredicateAbstraction . |
Constructor and Description |
---|
MergeWithPredicateAbstraction(java.lang.Iterable<AbstractionPredicate> predicates,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
java.util.Map<ProgramVariable,AbstractDomainElement> userChoices)
Creates a new instance of
MergeWithPredicateAbstraction . |
Copyright © 2003-2019 The KeY-Project.