public class SignAnalysisLattice extends AbstractDomainLattice
PartialComparator.PartialComparisonResult
Modifier and Type | Field and Description |
---|---|
static AbstractDomainElement[] |
ABSTRACT_DOMAIN_ELEMS
All elements of this abstract domain.
|
private static SignAnalysisLattice |
INSTANCE
The singleton instance of this lattice.
|
Modifier | Constructor and Description |
---|---|
private |
SignAnalysisLattice()
Private constructor (singleton!).
|
Modifier and Type | Method and Description |
---|---|
static SignAnalysisLattice |
getInstance() |
java.util.Iterator<AbstractDomainElement> |
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).
|
AbstractDomainElement |
join(AbstractDomainElement elem1,
AbstractDomainElement elem2)
A lattice join operation; finds an abstract element that is the least
upper bound of the set consisting of the elements a and b.
|
abstractFrom, compare, fromString, getSideConditionForAxiom
public static final AbstractDomainElement[] ABSTRACT_DOMAIN_ELEMS
private static final SignAnalysisLattice INSTANCE
private SignAnalysisLattice()
public static SignAnalysisLattice getInstance()
public AbstractDomainElement join(AbstractDomainElement elem1, AbstractDomainElement elem2)
AbstractDomainLattice
join
in class AbstractDomainLattice
elem1
- First element to find the least upper bound for.elem2
- Second element to find the least upper bound for.public java.util.Iterator<AbstractDomainElement> iterator()
AbstractDomainLattice
iterator
in interface java.lang.Iterable<AbstractDomainElement>
iterator
in class AbstractDomainLattice