de.uka.ilkd.key.rule.conditions

Class DropEffectlessStoresCondition

java.lang.Object

de.uka.ilkd.key.rule.conditions.DropEffectlessStoresCondition

All Implemented Interfaces:

VariableCondition

public final class DropEffectlessStoresCondition
extends java.lang.Object
implements VariableCondition

Field Summary

Fields

Modifier and Type	Field and Description
private TermSV	f
private TermSV	h
private TermSV	o
private TermSV	result
private TermSV	x

Constructor Summary

Constructors

Constructor and Description
DropEffectlessStoresCondition(TermSV h, TermSV o, TermSV f, TermSV x, TermSV result)

Method Summary

Modifier and Type	Method and Description
MatchConditions	check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc, Services services) checks if the condition for a correct instantiation is fulfilled
private static Term	dropEffectlessStores(Term t, Services services)
private static Term	dropEffectlessStoresHelper(Term heapTerm, TermServices services, ImmutableSet<Pair<Term,Term>> overwrittenLocs, Function store)
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

h

private final TermSV h

o

private final TermSV o

f

private final TermSV f

x

private final TermSV x

result

private final TermSV result

Constructor Detail

DropEffectlessStoresCondition

public DropEffectlessStoresCondition(TermSV h,
                                     TermSV o,
                                     TermSV f,
                                     TermSV x,
                                     TermSV result)

Method Detail

dropEffectlessStoresHelper

private static Term dropEffectlessStoresHelper(Term heapTerm,
                                               TermServices services,
                                               ImmutableSet<Pair<Term,Term>> overwrittenLocs,
                                               Function store)

dropEffectlessStores

private static Term dropEffectlessStores(Term t,
                                         Services services)

check

public MatchConditions check(SchemaVariable var,
                             SVSubstitute instCandidate,
                             MatchConditions mc,
                             Services services)

Description copied from interface: VariableCondition

checks if the condition for a correct instantiation is fulfilled

Specified by:

check in interface VariableCondition

Parameters:

var - the SchemaVariable to be instantiated

instCandidate - the SVSubstitute (e.g. Term, ProgramElement) to be mapped to var

mc - the MatchCondition with the current matching state and in particular the SVInstantiations that are already known to be needed

services - the program information object

Returns:

modified match results if the condition can be satisfied, or null otherwise

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object