org.jmlspecs.jml4.esc.vc
Class WlpVisitor

java.lang.Object
  org.jmlspecs.jml4.esc.vc.WlpVisitor

public class WlpVisitor
extends java.lang.Object

Constructor Summary

WlpVisitor()

Method Summary

VC	visit(CfgArrayAllocationExpression arrayAlloc)
VC	visit(CfgArrayReference arrayRef)
VC	visit(CfgAssert cfgAssert, VC N)
VC	visit(CfgAssume cfgAssume, VC N)
VC	visit(CfgBinaryExpression binExpr)
VC	visit(CfgBlock cfgBlock, VC N)
VC	visit(CfgBooleanConstant bool)
VC	visit(CfgConditionalExpression condExpr)
VC	visit(CfgFieldReference fieldRef)
VC	visit(CfgFieldStore fieldStore)
VC	visit(CfgGoto cfgGoto, VC N)
VC	visit(CfgIntegerConstant intConst)
VC	visit(CfgNotExpression notRef)
VC	visit(CfgQuantifiedExpression expr)
VC	visit(CfgSequence cfgSequence, VC N)
VC	visit(CfgStatementBlock cfgStatementBlock, VC N)
VC	visit(CfgSuperReference superRef)
VC	visit(CfgThisReference thisRef)
VC	visit(CfgVarDecl cfgVarDecl)
VC	visit(CfgVariable var)
VcProgram	visit(GcProgram gcProgram)

Methods inherited from class java.lang.Object

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

Constructor Detail

WlpVisitor

public WlpVisitor()

Method Detail

visit

public VcProgram visit(GcProgram gcProgram)

visit

public VC visit(CfgBlock cfgBlock,
                VC N)

visit

public VC visit(CfgAssert cfgAssert,
                VC N)

visit

public VC visit(CfgAssume cfgAssume,
                VC N)

visit

public VC visit(CfgSequence cfgSequence,
                VC N)

visit

public VC visit(CfgStatementBlock cfgStatementBlock,
                VC N)

visit

public VC visit(CfgVarDecl cfgVarDecl)

visit

public VC visit(CfgQuantifiedExpression expr)

visit

public VC visit(CfgVariable var)

visit

public VC visit(CfgBooleanConstant bool)

visit

public VC visit(CfgIntegerConstant intConst)

visit

public VC visit(CfgNotExpression notRef)

visit

public VC visit(CfgBinaryExpression binExpr)

visit

public VC visit(CfgConditionalExpression condExpr)

visit

public VC visit(CfgGoto cfgGoto,
                VC N)

visit

public VC visit(CfgSuperReference superRef)

visit

public VC visit(CfgThisReference thisRef)

visit

public VC visit(CfgFieldReference fieldRef)

visit

public VC visit(CfgFieldStore fieldStore)

visit

public VC visit(CfgArrayReference arrayRef)

visit

public VC visit(CfgArrayAllocationExpression arrayAlloc)