gov.nasa.jpf.symbc.veritesting.ast.def

Class SPFCaseStmt

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.def.SPFCaseStmt

All Implemented Interfaces:

Ast, Stmt

public class SPFCaseStmt
extends java.lang.Object
implements Stmt

This is SPFCases in RangerIR. These are basically a place holder for places in RangerIR where SPF needs to explore.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	SPFCaseStmt.SPFReason These are the different reasons that requires SPF exploration.

Field Summary

Fields

Modifier and Type	Field and Description
SPFCaseStmt.SPFReason	reason
za.ac.sun.cs.green.expr.Expression	spfCondition

Constructor Summary

Constructors

Constructor and Description
SPFCaseStmt(za.ac.sun.cs.green.expr.Expression spfCondition, SPFCaseStmt.SPFReason reason)

Method Summary

Modifier and Type	Method and Description
<T> T	accept(AstVisitor<T> visitor)
boolean	equals(java.lang.Object stmt2)
boolean	equals(Stmt stmt2)
int	hashCode()
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

spfCondition

public final za.ac.sun.cs.green.expr.Expression spfCondition

reason

public final SPFCaseStmt.SPFReason reason

Constructor Detail

SPFCaseStmt

public SPFCaseStmt(za.ac.sun.cs.green.expr.Expression spfCondition,
                   SPFCaseStmt.SPFReason reason)

Method Detail

accept

public <T> T accept(AstVisitor<T> visitor)

Specified by:

accept in interface Ast

Specified by:

accept in interface Stmt

toString

public java.lang.String toString()

Specified by:

toString in interface Stmt

Overrides:

toString in class java.lang.Object

equals

public boolean equals(java.lang.Object stmt2)

Overrides:

equals in class java.lang.Object

equals

public boolean equals(Stmt stmt2)

Specified by:

equals in interface Stmt

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object