Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## escjava.ast
Class LoopCmd

    java.lang.Object
      javafe.ast.ASTNode
          escjava.ast.GuardedCmd
              escjava.ast.LoopCmd

All Implemented Interfaces:
  java.lang.Cloneable

public class LoopCmd
extends GuardedCmd

Field Summary
`GuardedCmd` | `body`
`DecreasesInfoVec` | `decreases`
`GuardedCmd` | `desugared`
`GuardedCmd` | `guard`
`ConditionVec` | `invariants`
`int` | `locEnd`
`int` | `locHotspot`
`int` | `locStart`
`java.util.Hashtable` | `oldmap`
`ExprVec` | `predicates`
`LocalVarDeclVec` | `skolemConstants`
`GenericVarDeclVec` | `tempVars`

Fields inherited from class javafe.ast.ASTNode
``

Constructor Summary
`protected` | `LoopCmd()` Construct a raw LoopCmd whose class invariant(s) have not yet been established.

Method Summary
`void` | `accept(Visitor v)` Accept a visit from `v`.
`java.lang.Object` | `accept(VisitorArgResult v, java.lang.Object o)`
`void` | `check()`
`java.lang.Object` | `childAt(int index)` Return the first-but-ith child of a node.
`int` | `childCount()` Return the number of children a node has.
`int` | `getEndLoc()`
`int` | `getStartLoc()`
`int` | `getTag()` Return the tag of a node.
`static LoopCmd` | `make(int locStart, int locEnd, int locHotspot, java.util.Hashtable oldmap, ConditionVec invariants, DecreasesInfoVec decreases, LocalVarDeclVec skolemConstants, ExprVec predicates, GenericVarDeclVec tempVars, GuardedCmd guard, GuardedCmd body)`
`java.lang.String` | `toString()` Return a string representation of `this`.

Methods inherited from class javafe.ast.ASTNode
`clone, clone, getDecorations, setDecorations`

Methods inherited from class java.lang.Object
`equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait`

Field Detail

### locStart

    public int locStart

### locEnd

    public int locEnd

### locHotspot

    public int locHotspot

### oldmap

    public java.util.Hashtable oldmap

### invariants

    public ConditionVec invariants

### decreases

    public DecreasesInfoVec decreases

### skolemConstants

    public LocalVarDeclVec skolemConstants

### predicates

    public ExprVec predicates

### tempVars

    public GenericVarDeclVec tempVars

### guard

    public GuardedCmd guard

### body

    public GuardedCmd body

### desugared

    public GuardedCmd desugared

Constructor Detail

### LoopCmd

    protected LoopCmd()

  Construct a raw LoopCmd whose class invariant(s) have not yet been established. It is the caller's job to initialize the returned node's fields so that any class invariants hold.

Method Detail

### getStartLoc

    public int getStartLoc()

  Specified by:
    `getStartLoc` in class `ASTNode`

### getEndLoc

    public int getEndLoc()

  Overrides:
    `getEndLoc` in class `ASTNode`

### childCount

    public final int childCount()

  Description copied from class: `GuardedCmd`
  Return the number of children a node has.

  Specified by:
    `childCount` in class `GuardedCmd`

### childAt

    public final java.lang.Object childAt(int index)

  Description copied from class: `GuardedCmd`
  Return the first-but-ith child of a node.

  Specified by:
    `childAt` in class `GuardedCmd`

### toString

    public final java.lang.String toString()

  Description copied from class: `GuardedCmd`
  Return a string representation of `this`. Meant for debugging use only, not for presentation.

  Specified by:
    `toString` in class `GuardedCmd`

### getTag

    public final int getTag()

  Description copied from class: `GuardedCmd`
  Return the tag of a node.

  Specified by:
    `getTag` in class `GuardedCmd`

### accept

    public final void accept(Visitor v)

  Description copied from class: `GuardedCmd`
  Accept a visit from `v`. This method simply calls the method of `v` corresponding to the allocated type of `this`, passing `this` as the argument. See the design patterns book.

  Specified by:
    `accept` in class `GuardedCmd`

### accept

    public final java.lang.Object accept(VisitorArgResult v,
                                         java.lang.Object o)

  Specified by:
    `accept` in class `GuardedCmd`

### check

    public void check()

  Overrides:
    `check` in class `GuardedCmd`

### make

    public static LoopCmd make(int locStart,
                               int locEnd,
                               int locHotspot,
                               java.util.Hashtable oldmap,
                               ConditionVec invariants,
                               DecreasesInfoVec decreases,
                               LocalVarDeclVec skolemConstants,
                               ExprVec predicates,
                               GenericVarDeclVec tempVars,
                               GuardedCmd guard,
                               GuardedCmd body)

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage