org.jmlspecs.jml4.esc.vc.lang
Class VcFieldStore

java.lang.Object
  org.jmlspecs.jml4.esc.vc.lang.VC
      org.jmlspecs.jml4.esc.vc.lang.VcFieldStore

All Implemented Interfaces:

java.lang.Comparable

public class VcFieldStore
extends VC

Field Summary

VcFieldReference	field
int	newIncarnation
int	oldIncarnation
VC	value

Fields inherited from class org.jmlspecs.jml4.esc.vc.lang.VC

EMPTY, NEGLBL, NO_LBL, sourceEnd, sourceStart, type

Constructor Summary

VcFieldStore(VcFieldReference field, int oldIncarnation, int newIncarnation, VC value)

VcFieldStore(VcFieldReference field, int oldIncarnation, int newIncarnation, VC value, KindOfAssertion kindOfAssertion, int kindOfLabel, int labelStart)

Method Summary

java.lang.String	accept(ProverVisitor visitor)
int	hashCode()
java.lang.String	toString()

Methods inherited from class org.jmlspecs.jml4.esc.vc.lang.VC

acceptAsTerm, addDecl, addDecls, compareTo, decls, declString, endsInImpliesTrue, equals, getName, hasName, isImplication, kindOfAssertion, kindOfLabel, labelStart, markAsImplication, negateLastImplication, setLabel, setName, toStringWithName, visitVarDecls

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Field Detail

field

public final VcFieldReference field

oldIncarnation

public final int oldIncarnation

newIncarnation

public final int newIncarnation

value

public final VC value

Constructor Detail

VcFieldStore

public VcFieldStore(VcFieldReference field,
                    int oldIncarnation,
                    int newIncarnation,
                    VC value,
                    KindOfAssertion kindOfAssertion,
                    int kindOfLabel,
                    int labelStart)

VcFieldStore

public VcFieldStore(VcFieldReference field,
                    int oldIncarnation,
                    int newIncarnation,
                    VC value)

Method Detail

accept

public java.lang.String accept(ProverVisitor visitor)

Specified by:

accept in class VC

hashCode

public int hashCode()

Specified by:

hashCode in class VC

toString

public java.lang.String toString()

Specified by:

toString in class VC