escjava.vcGeneration.pvs
Class TPvsVisitor

java.lang.Object
  escjava.vcGeneration.TVisitor
      escjava.vcGeneration.pvs.TPvsVisitor

public class TPvsVisitor

extends TVisitor

Field Summary

Fields inherited from class escjava.vcGeneration.TVisitor

indentation, lib, out

Constructor Summary

(package private)

TPvsVisitor(java.io.Writer out)

Method Summary

void	binOp(java.lang.String s, TFunction n) Function for binary operator You give the operator at the first argument and then it outputs (son1 op son2) If son1 is a variable, op isn't on the next line If son2 is a variable, it doesn't go to next line.
void	genericFun(java.lang.String s, TFunction n) General Function You give the operator at the first argument and then it outputs op (son1, son2 ...) )
void	genericOp(java.lang.String s, TFunction n) You give the operator at the first argument and then it outputs (son1 op son2 ...
void	unaryGeneric(java.lang.String s, TFunction n) Function/Operator with arity 1 : (op X)
void	visitTAllocLE(TAllocLE n)
void	visitTAllocLT(TAllocLT n)
void	visitTAnyEQ(TAnyEQ n)
void	visitTAnyNE(TAnyNE n)
void	visitTArrayFresh(TArrayFresh n)
void	visitTArrayLength(TArrayLength n)
void	visitTArrayShapeMore(TArrayShapeMore n)
void	visitTArrayShapeOne(TArrayShapeOne n)
void	visitTAsElems(TAsElems n)
void	visitTAsField(TAsField n)
void	visitTAsLockSet(TAsLockSet n)
void	visitTBoolAnd(TBoolAnd n)
void	visitTBoolean(TBoolean n)
void	visitTBoolEQ(TBoolEQ n)
void	visitTBoolImplies(TBoolImplies n)
void	visitTBoolNE(TBoolNE n)
void	visitTBoolNot(TBoolNot n)
void	visitTBoolOr(TBoolOr n)
void	visitTCast(TCast n)
void	visitTChar(TChar n)
void	visitTDouble(TDouble n)
void	visitTEClosedTime(TEClosedTime n)
void	visitTExist(TExist n)
void	visitTFClosedTime(TFClosedTime n)
void	visitTFloat(TFloat n)
void	visitTFloatAdd(TFloatAdd n)
void	visitTFloatDiv(TFloatDiv n)
void	visitTFloatEQ(TFloatEQ n)
void	visitTFloatGE(TFloatGE n)
void	visitTFloatGT(TFloatGT n)
void	visitTFloatLE(TFloatLE n)
void	visitTFloatLT(TFloatLT n)
void	visitTFloatMod(TFloatMod n)
void	visitTFloatMul(TFloatMul n)
void	visitTFloatNE(TFloatNE n)
void	visitTForAll(TForAll n)
void	visitTInt(TInt n)
void	visitTIntegralAdd(TIntegralAdd n)
void	visitTIntegralDiv(TIntegralDiv n)
void	visitTIntegralEQ(TIntegralEQ n)
void	visitTIntegralGE(TIntegralGE n)
void	visitTIntegralGT(TIntegralGT n)
void	visitTIntegralLE(TIntegralLE n)
void	visitTIntegralLT(TIntegralLT n)
void	visitTIntegralMod(TIntegralMod n)
void	visitTIntegralMul(TIntegralMul n)
void	visitTIntegralNE(TIntegralNE n)
void	visitTIntegralSub(TIntegralSub sub)
void	visitTIs(TIs n)
void	visitTIsAllocated(TIsAllocated n)
void	visitTIsNewArray(TIsNewArray n)
void	visitTLockLE(TLockLE n)
void	visitTLockLT(TLockLT n)
void	visitTMethodCall(TMethodCall call)
void	visitTName(TName n)
void	visitTNull(TNull n)
void	visitTRefEQ(TRefEQ n)
void	visitTRefNE(TRefNE n)
void	visitTRoot(TRoot n)
void	visitTSelect(TSelect n)
void	visitTStore(TStore n)
void	visitTString(TString n)
void	visitTSum(TSum s)
void	visitTTypeEQ(TTypeEQ n)
void	visitTTypeLE(TTypeLE n)
void	visitTTypeNE(TTypeNE n)
void	visitTTypeOf(TTypeOf n)
void	visitTUnset(TUnset n)

Methods inherited from class java.lang.Object

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

Constructor Detail

TPvsVisitor

TPvsVisitor(java.io.Writer out)

Method Detail

genericFun

public void genericFun(java.lang.String s,
                       TFunction n)
                throws java.io.IOException

General Function You give the operator at the first argument and then it outputs op (son1, son2 ...) )

Throws:

java.io.IOException

unaryGeneric

public void unaryGeneric(java.lang.String s,
                         TFunction n)
                  throws java.io.IOException

Function/Operator with arity 1 : (op X)

Throws:

java.io.IOException

genericOp

public void genericOp(java.lang.String s,
                      TFunction n)
               throws java.io.IOException

You give the operator at the first argument and then it outputs (son1 op son2 ... op sonN)

Throws:

java.io.IOException

binOp

public void binOp(java.lang.String s,
                  TFunction n)
           throws java.io.IOException

Function for binary operator You give the operator at the first argument and then it outputs (son1 op son2) If son1 is a variable, op isn't on the next line If son2 is a variable, it doesn't go to next line.

Throws:

java.io.IOException

visitTName

public void visitTName(TName n)
                throws java.io.IOException

Specified by:

visitTName in class TVisitor

Throws:

java.io.IOException

visitTRoot

public void visitTRoot(TRoot n)
                throws java.io.IOException

Specified by:

visitTRoot in class TVisitor

Throws:

java.io.IOException

visitTBoolImplies

public void visitTBoolImplies(TBoolImplies n)
                       throws java.io.IOException

Specified by:

visitTBoolImplies in class TVisitor

Throws:

java.io.IOException

visitTBoolAnd

public void visitTBoolAnd(TBoolAnd n)
                   throws java.io.IOException

Specified by:

visitTBoolAnd in class TVisitor

Throws:

java.io.IOException

visitTBoolOr

public void visitTBoolOr(TBoolOr n)
                  throws java.io.IOException

Specified by:

visitTBoolOr in class TVisitor

Throws:

java.io.IOException

visitTBoolNot

public void visitTBoolNot(TBoolNot n)
                   throws java.io.IOException

Specified by:

visitTBoolNot in class TVisitor

Throws:

java.io.IOException

visitTBoolEQ

public void visitTBoolEQ(TBoolEQ n)
                  throws java.io.IOException

Specified by:

visitTBoolEQ in class TVisitor

Throws:

java.io.IOException

visitTBoolNE

public void visitTBoolNE(TBoolNE n)
                  throws java.io.IOException

Specified by:

visitTBoolNE in class TVisitor

Throws:

java.io.IOException

visitTAllocLT

public void visitTAllocLT(TAllocLT n)
                   throws java.io.IOException

Specified by:

visitTAllocLT in class TVisitor

Throws:

java.io.IOException

visitTAllocLE

public void visitTAllocLE(TAllocLE n)
                   throws java.io.IOException

Specified by:

visitTAllocLE in class TVisitor

Throws:

java.io.IOException

visitTAnyEQ

public void visitTAnyEQ(TAnyEQ n)
                 throws java.io.IOException

Specified by:

visitTAnyEQ in class TVisitor

Throws:

java.io.IOException

visitTAnyNE

public void visitTAnyNE(TAnyNE n)
                 throws java.io.IOException

Specified by:

visitTAnyNE in class TVisitor

Throws:

java.io.IOException

visitTIntegralEQ

public void visitTIntegralEQ(TIntegralEQ n)
                      throws java.io.IOException

Specified by:

visitTIntegralEQ in class TVisitor

Throws:

java.io.IOException

visitTIntegralGE

public void visitTIntegralGE(TIntegralGE n)
                      throws java.io.IOException

Specified by:

visitTIntegralGE in class TVisitor

Throws:

java.io.IOException

visitTIntegralGT

public void visitTIntegralGT(TIntegralGT n)
                      throws java.io.IOException

Specified by:

visitTIntegralGT in class TVisitor

Throws:

java.io.IOException

visitTIntegralLE

public void visitTIntegralLE(TIntegralLE n)
                      throws java.io.IOException

Specified by:

visitTIntegralLE in class TVisitor

Throws:

java.io.IOException

visitTIntegralLT

public void visitTIntegralLT(TIntegralLT n)
                      throws java.io.IOException

Specified by:

visitTIntegralLT in class TVisitor

Throws:

java.io.IOException

visitTIntegralNE

public void visitTIntegralNE(TIntegralNE n)
                      throws java.io.IOException

Specified by:

visitTIntegralNE in class TVisitor

Throws:

java.io.IOException

visitTIntegralAdd

public void visitTIntegralAdd(TIntegralAdd n)
                       throws java.io.IOException

Specified by:

visitTIntegralAdd in class TVisitor

Throws:

java.io.IOException

visitTIntegralDiv

public void visitTIntegralDiv(TIntegralDiv n)
                       throws java.io.IOException

Specified by:

visitTIntegralDiv in class TVisitor

Throws:

java.io.IOException

visitTIntegralMod

public void visitTIntegralMod(TIntegralMod n)
                       throws java.io.IOException

Specified by:

visitTIntegralMod in class TVisitor

Throws:

java.io.IOException

visitTIntegralMul

public void visitTIntegralMul(TIntegralMul n)
                       throws java.io.IOException

Specified by:

visitTIntegralMul in class TVisitor

Throws:

java.io.IOException

visitTFloatEQ

public void visitTFloatEQ(TFloatEQ n)
                   throws java.io.IOException

Specified by:

visitTFloatEQ in class TVisitor

Throws:

java.io.IOException

visitTFloatGE

public void visitTFloatGE(TFloatGE n)
                   throws java.io.IOException

Specified by:

visitTFloatGE in class TVisitor

Throws:

java.io.IOException

visitTFloatGT

public void visitTFloatGT(TFloatGT n)
                   throws java.io.IOException

Specified by:

visitTFloatGT in class TVisitor

Throws:

java.io.IOException

visitTFloatLE

public void visitTFloatLE(TFloatLE n)
                   throws java.io.IOException

Specified by:

visitTFloatLE in class TVisitor

Throws:

java.io.IOException

visitTFloatLT

public void visitTFloatLT(TFloatLT n)
                   throws java.io.IOException

Specified by:

visitTFloatLT in class TVisitor

Throws:

java.io.IOException

visitTFloatNE

public void visitTFloatNE(TFloatNE n)
                   throws java.io.IOException

Specified by:

visitTFloatNE in class TVisitor

Throws:

java.io.IOException

visitTFloatAdd

public void visitTFloatAdd(TFloatAdd n)
                    throws java.io.IOException

Specified by:

visitTFloatAdd in class TVisitor

Throws:

java.io.IOException

visitTFloatDiv

public void visitTFloatDiv(TFloatDiv n)
                    throws java.io.IOException

Specified by:

visitTFloatDiv in class TVisitor

Throws:

java.io.IOException

visitTFloatMod

public void visitTFloatMod(TFloatMod n)
                    throws java.io.IOException

Specified by:

visitTFloatMod in class TVisitor

Throws:

java.io.IOException

visitTFloatMul

public void visitTFloatMul(TFloatMul n)
                    throws java.io.IOException

Specified by:

visitTFloatMul in class TVisitor

Throws:

java.io.IOException

visitTLockLE

public void visitTLockLE(TLockLE n)
                  throws java.io.IOException

Specified by:

visitTLockLE in class TVisitor

Throws:

java.io.IOException

visitTLockLT

public void visitTLockLT(TLockLT n)
                  throws java.io.IOException

Specified by:

visitTLockLT in class TVisitor

Throws:

java.io.IOException

visitTRefEQ

public void visitTRefEQ(TRefEQ n)
                 throws java.io.IOException

Specified by:

visitTRefEQ in class TVisitor

Throws:

java.io.IOException

visitTRefNE

public void visitTRefNE(TRefNE n)
                 throws java.io.IOException

Specified by:

visitTRefNE in class TVisitor

Throws:

java.io.IOException

visitTTypeEQ

public void visitTTypeEQ(TTypeEQ n)
                  throws java.io.IOException

Specified by:

visitTTypeEQ in class TVisitor

Throws:

java.io.IOException

visitTTypeNE

public void visitTTypeNE(TTypeNE n)
                  throws java.io.IOException

Specified by:

visitTTypeNE in class TVisitor

Throws:

java.io.IOException

visitTTypeLE

public void visitTTypeLE(TTypeLE n)
                  throws java.io.IOException

Specified by:

visitTTypeLE in class TVisitor

Throws:

java.io.IOException

visitTCast

public void visitTCast(TCast n)
                throws java.io.IOException

Specified by:

visitTCast in class TVisitor

Throws:

java.io.IOException

visitTIs

public void visitTIs(TIs n)
              throws java.io.IOException

Specified by:

visitTIs in class TVisitor

Throws:

java.io.IOException

visitTSelect

public void visitTSelect(TSelect n)
                  throws java.io.IOException

Specified by:

visitTSelect in class TVisitor

Throws:

java.io.IOException

visitTStore

public void visitTStore(TStore n)
                 throws java.io.IOException

Specified by:

visitTStore in class TVisitor

Throws:

java.io.IOException

visitTTypeOf

public void visitTTypeOf(TTypeOf n)
                  throws java.io.IOException

Specified by:

visitTTypeOf in class TVisitor

Throws:

java.io.IOException

visitTForAll

public void visitTForAll(TForAll n)
                  throws java.io.IOException

Specified by:

visitTForAll in class TVisitor

Throws:

java.io.IOException

visitTExist

public void visitTExist(TExist n)
                 throws java.io.IOException

Specified by:

visitTExist in class TVisitor

Throws:

java.io.IOException

visitTIsAllocated

public void visitTIsAllocated(TIsAllocated n)
                       throws java.io.IOException

Specified by:

visitTIsAllocated in class TVisitor

Throws:

java.io.IOException

visitTEClosedTime

public void visitTEClosedTime(TEClosedTime n)
                       throws java.io.IOException

Specified by:

visitTEClosedTime in class TVisitor

Throws:

java.io.IOException

visitTFClosedTime

public void visitTFClosedTime(TFClosedTime n)
                       throws java.io.IOException

Specified by:

visitTFClosedTime in class TVisitor

Throws:

java.io.IOException

visitTAsElems

public void visitTAsElems(TAsElems n)
                   throws java.io.IOException

Specified by:

visitTAsElems in class TVisitor

Throws:

java.io.IOException

visitTAsField

public void visitTAsField(TAsField n)
                   throws java.io.IOException

Specified by:

visitTAsField in class TVisitor

Throws:

java.io.IOException

visitTAsLockSet

public void visitTAsLockSet(TAsLockSet n)
                     throws java.io.IOException

Specified by:

visitTAsLockSet in class TVisitor

Throws:

java.io.IOException

visitTArrayLength

public void visitTArrayLength(TArrayLength n)
                       throws java.io.IOException

Specified by:

visitTArrayLength in class TVisitor

Throws:

java.io.IOException

visitTArrayFresh

public void visitTArrayFresh(TArrayFresh n)
                      throws java.io.IOException

Specified by:

visitTArrayFresh in class TVisitor

Throws:

java.io.IOException

visitTArrayShapeOne

public void visitTArrayShapeOne(TArrayShapeOne n)
                         throws java.io.IOException

Specified by:

visitTArrayShapeOne in class TVisitor

Throws:

java.io.IOException

visitTArrayShapeMore

public void visitTArrayShapeMore(TArrayShapeMore n)
                          throws java.io.IOException

Specified by:

visitTArrayShapeMore in class TVisitor

Throws:

java.io.IOException

visitTIsNewArray

public void visitTIsNewArray(TIsNewArray n)
                      throws java.io.IOException

Specified by:

visitTIsNewArray in class TVisitor

Throws:

java.io.IOException

visitTString

public void visitTString(TString n)
                  throws java.io.IOException

Specified by:

visitTString in class TVisitor

Throws:

java.io.IOException

visitTBoolean

public void visitTBoolean(TBoolean n)
                   throws java.io.IOException

Specified by:

visitTBoolean in class TVisitor

Throws:

java.io.IOException

visitTChar

public void visitTChar(TChar n)
                throws java.io.IOException

Specified by:

visitTChar in class TVisitor

Throws:

java.io.IOException

visitTInt

public void visitTInt(TInt n)
               throws java.io.IOException

Specified by:

visitTInt in class TVisitor

Throws:

java.io.IOException

visitTFloat

public void visitTFloat(TFloat n)
                 throws java.io.IOException

Specified by:

visitTFloat in class TVisitor

Throws:

java.io.IOException

visitTDouble

public void visitTDouble(TDouble n)
                  throws java.io.IOException

Specified by:

visitTDouble in class TVisitor

Throws:

java.io.IOException

visitTNull

public void visitTNull(TNull n)
                throws java.io.IOException

Specified by:

visitTNull in class TVisitor

Throws:

java.io.IOException

visitTUnset

public void visitTUnset(TUnset n)
                 throws java.io.IOException

Specified by:

visitTUnset in class TVisitor

Throws:

java.io.IOException

visitTMethodCall

public void visitTMethodCall(TMethodCall call)
                      throws java.io.IOException

Specified by:

visitTMethodCall in class TVisitor

Throws:

java.io.IOException

visitTIntegralSub

public void visitTIntegralSub(TIntegralSub sub)
                       throws java.io.IOException

Specified by:

visitTIntegralSub in class TVisitor

Throws:

java.io.IOException

visitTSum

public void visitTSum(TSum s)

Specified by:

visitTSum in class TVisitor