org.jmlspecs.jml4.esc.gc
Class DesugarLoopVisitor

java.lang.Object
  org.jmlspecs.jml4.esc.gc.DesugarLoopVisitor

All Implemented Interfaces:

SugaredStatementVisitor

public class DesugarLoopVisitor
extends java.lang.Object
implements SugaredStatementVisitor

Field Summary

static boolean

useNewLoopSemantics

Constructor Summary

DesugarLoopVisitor()

Method Summary

SugaredStatement	visit(SugaredAssert sugaredAssert, SugaredStatement rest)
SugaredStatement	visit(SugaredAssume sugaredAssume, SugaredStatement rest)
SugaredBlock[]	visit(SugaredBlock origBlock)
SugaredStatement	visit(SugaredBreakStatement breakStmt, SugaredStatement rest)
SugaredStatement	visit(SugaredContinueStatement continueStmt, SugaredStatement rest)
SugaredStatement	visit(SugaredExprStatement sugaredExprStatement, SugaredStatement rest)
SugaredStatement	visit(SugaredGoto sugaredGoto, SugaredStatement rest)
SugaredStatement	visit(SugaredHavoc sugaredHavoc, SugaredStatement rest)
SugaredStatement	visit(SugaredIfStatement sugaredIfStatement, SugaredStatement rest)
SugaredStatement	visit(SugaredPostcondition sugaredPostcondition, SugaredStatement rest)
SugaredStatement	visit(SugaredPrecondition sugaredPrecondition, SugaredStatement rest)
SugaredProgram	visit(SugaredProgram origProgram)
SugaredStatement	visit(SugaredReturnStatement returnStmt, SugaredStatement rest)
SugaredStatement	visit(SugaredSequence sugaredSequence, SugaredStatement rest)
SugaredStatement	visit(SugaredVarDecl sugaredVarDecl, SugaredStatement rest)
SugaredStatement	visit(SugaredWhileStatement whileStmt, SugaredStatement rest)

Methods inherited from class java.lang.Object

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

Field Detail

useNewLoopSemantics

public static final boolean useNewLoopSemantics

See Also:

Constant Field Values

Constructor Detail

DesugarLoopVisitor

public DesugarLoopVisitor()

Method Detail

visit

public SugaredProgram visit(SugaredProgram origProgram)

visit

public SugaredBlock[] visit(SugaredBlock origBlock)

visit

public SugaredStatement visit(SugaredAssert sugaredAssert,
                              SugaredStatement rest)

Specified by:

visit in interface SugaredStatementVisitor

visit

public SugaredStatement visit(SugaredAssume sugaredAssume,
                              SugaredStatement rest)

Specified by:

visit in interface SugaredStatementVisitor

visit

public SugaredStatement visit(SugaredPrecondition sugaredPrecondition,
                              SugaredStatement rest)

Specified by:

visit in interface SugaredStatementVisitor

visit

public SugaredStatement visit(SugaredPostcondition sugaredPostcondition,
                              SugaredStatement rest)

Specified by:

visit in interface SugaredStatementVisitor

visit

public SugaredStatement visit(SugaredVarDecl sugaredVarDecl,
                              SugaredStatement rest)

Specified by:

visit in interface SugaredStatementVisitor

visit

public SugaredStatement visit(SugaredGoto sugaredGoto,
                              SugaredStatement rest)

Specified by:

visit in interface SugaredStatementVisitor

visit

public SugaredStatement visit(SugaredExprStatement sugaredExprStatement,
                              SugaredStatement rest)

Specified by:

visit in interface SugaredStatementVisitor

visit

public SugaredStatement visit(SugaredSequence sugaredSequence,
                              SugaredStatement rest)

Specified by:

visit in interface SugaredStatementVisitor

visit

public SugaredStatement visit(SugaredIfStatement sugaredIfStatement,
                              SugaredStatement rest)

visit

public SugaredStatement visit(SugaredWhileStatement whileStmt,
                              SugaredStatement rest)

Specified by:

visit in interface SugaredStatementVisitor

visit

public SugaredStatement visit(SugaredBreakStatement breakStmt,
                              SugaredStatement rest)

Specified by:

visit in interface SugaredStatementVisitor

visit

public SugaredStatement visit(SugaredContinueStatement continueStmt,
                              SugaredStatement rest)

Specified by:

visit in interface SugaredStatementVisitor

visit

public SugaredStatement visit(SugaredHavoc sugaredHavoc,
                              SugaredStatement rest)

Specified by:

visit in interface SugaredStatementVisitor

visit

public SugaredStatement visit(SugaredReturnStatement returnStmt,
                              SugaredStatement rest)

Specified by:

visit in interface SugaredStatementVisitor