gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess

Class SubstituteGetOutput

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubstituteGetOutput

public class SubstituteGetOutput
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
za.ac.sun.cs.green.expr.Expression	def
java.lang.String	exceptionalMessage
FieldRef	fieldRef
private gov.nasa.jpf.symbc.numeric.Expression	finalValue
private boolean	isRead
private gov.nasa.jpf.vm.ThreadInfo	ti
java.lang.String	type

Constructor Summary

Constructors

Constructor and Description
SubstituteGetOutput(gov.nasa.jpf.vm.ThreadInfo ti, FieldRef fieldRef, boolean isRead, gov.nasa.jpf.symbc.numeric.Expression finalValue)

Method Summary

Modifier and Type	Method and Description
private void	executeRead(gov.nasa.jpf.vm.ElementInfo eiFieldOwner, gov.nasa.jpf.vm.FieldInfo fieldInfo)
private void	executeWrite(gov.nasa.jpf.vm.ElementInfo eiFieldOwner, gov.nasa.jpf.vm.FieldInfo fieldInfo)
za.ac.sun.cs.green.expr.Expression	getDef()
(package private) java.lang.String	getExceptionalMessage()
java.lang.String	getType()
SubstituteGetOutput	invoke()

Methods inherited from class java.lang.Object

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

Field Detail

fieldRef

public FieldRef fieldRef

exceptionalMessage

public java.lang.String exceptionalMessage

def

public za.ac.sun.cs.green.expr.Expression def

type

public java.lang.String type

isRead

private boolean isRead

ti

private gov.nasa.jpf.vm.ThreadInfo ti

finalValue

private gov.nasa.jpf.symbc.numeric.Expression finalValue

Constructor Detail

SubstituteGetOutput

public SubstituteGetOutput(gov.nasa.jpf.vm.ThreadInfo ti,
                           FieldRef fieldRef,
                           boolean isRead,
                           gov.nasa.jpf.symbc.numeric.Expression finalValue)

Method Detail

getExceptionalMessage

java.lang.String getExceptionalMessage()

getDef

public za.ac.sun.cs.green.expr.Expression getDef()

getType

public java.lang.String getType()

invoke

public SubstituteGetOutput invoke()

executeWrite

private void executeWrite(gov.nasa.jpf.vm.ElementInfo eiFieldOwner,
                          gov.nasa.jpf.vm.FieldInfo fieldInfo)

executeRead

private void executeRead(gov.nasa.jpf.vm.ElementInfo eiFieldOwner,
                         gov.nasa.jpf.vm.FieldInfo fieldInfo)