AbstrDomElem
- public abstract class AbstractDomainLattice extends java.lang.Object implements PartialComparator<AbstractDomainElement>, java.lang.Iterable<AbstractDomainElement>
PartialComparator.PartialComparisonResult
Modifier and Type | Field and Description |
---|---|
private static int |
AXIOM_PROVE_TIMEOUT_MS
Time in milliseconds after which a proof attempt of a defining axiom
times out.
|
Constructor and Description |
---|
AbstractDomainLattice() |
Modifier and Type | Method and Description |
---|---|
AbstractDomainElement |
abstractFrom(SymbolicExecutionState state,
Term term,
Services services)
Abstracts from a given element of the concrete domain by returning a
suitable abstract element.
|
PartialComparator.PartialComparisonResult |
compare(AbstractDomainElement a,
AbstractDomainElement b)
Compares its two arguments for order.
|
AbstractDomainElement |
fromString(java.lang.String s,
Services services)
Constructs an Abstract Domain Element from the given String
representation.
|
static Term |
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 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).
|
abstract AbstractDomainElement |
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.
|
private static final int AXIOM_PROVE_TIMEOUT_MS
public AbstractDomainElement abstractFrom(SymbolicExecutionState state, Term term, Services services)
state
- The state in which the abstraction should hold.term
- Element to abstract from.services
- The services object.public static Term getSideConditionForAxiom(SymbolicExecutionState state, Term term, AbstractDomainElement elem, Services services)
state
- The state in which the abstraction should hold.term
- Element to abstract from.elem
- Abstract domain element to check.services
- The services object.public abstract AbstractDomainElement join(AbstractDomainElement a, AbstractDomainElement b)
a
- First element to find the least upper bound for.b
- Second element to find the least upper bound for.public PartialComparator.PartialComparisonResult compare(AbstractDomainElement a, AbstractDomainElement b)
PartialComparator
compare
in interface PartialComparator<AbstractDomainElement>
a
- the first object to be compared.b
- the second object to be compared.public abstract java.util.Iterator<AbstractDomainElement> iterator()
iterator
in interface java.lang.Iterable<AbstractDomainElement>
public AbstractDomainElement fromString(java.lang.String s, Services services)
AbstractDomainElement
e, that
fromString(e.toParseableString(),
services).equals(e)
.s
- String to parse.services
- The services object.AbstractDomainElement
.java.lang.RuntimeException
- if s cannot be parsed.