001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 /* IF THIS IS A JAVA FILE, DO NOT EDIT IT! 004 005 Most Java files in this directory which are part of the Javafe AST 006 are automatically generated using the astgen comment (see 007 ESCTools/Javafe/astgen) from the input file 'hierarchy.h'. If you 008 wish to modify AST classes or introduce new ones, modify 009 'hierarchy.j.' 010 */ 011 012 package javafe.ast; 013 014 import javafe.util.Assert; 015 import javafe.util.Location; 016 import javafe.util.ErrorSet; 017 018 // Convention: unless otherwise noted, integer fields named "loc" refer 019 // to the location of the first character of the syntactic unit 020 021 022 public class WhileStmt extends Stmt 023 { 024 public /*@ non_null @*/ Expr expr; 025 026 public /*@ non_null @*/ Stmt stmt; 027 028 //@ invariant loc != javafe.util.Location.NULL; 029 public int loc; 030 031 //@ invariant locGuardOpenParen != javafe.util.Location.NULL; 032 public int locGuardOpenParen; 033 034 035 private void postCheck() { 036 int t = stmt.getTag(); 037 Assert.notFalse(t != TagConstants.SWITCHLABEL //@ nowarn Pre; 038 && t != TagConstants.CONSTRUCTORINVOCATION 039 && t != TagConstants.VARDECLSTMT); 040 } 041 public int getStartLoc() { return loc; } 042 public int getEndLoc() { return stmt.getEndLoc(); } 043 044 045 // Generated boilerplate constructors: 046 047 /** 048 * Construct a raw WhileStmt whose class invariant(s) have not 049 * yet been established. It is the caller's job to 050 * initialize the returned node's fields so that any 051 * class invariants hold. 052 */ 053 //@ requires I_will_establish_invariants_afterwards; 054 protected WhileStmt() {} //@ nowarn Invariant,NonNullInit; 055 056 057 // Generated boilerplate methods: 058 059 public final int childCount() { 060 return 2; 061 } 062 063 public final Object childAt(int index) { 064 /*throws IndexOutOfBoundsException*/ 065 if (index < 0) 066 throw new IndexOutOfBoundsException("AST child index " + index); 067 int indexPre = index; 068 069 int sz; 070 071 if (index == 0) return this.expr; 072 else index--; 073 074 if (index == 0) return this.stmt; 075 else index--; 076 077 throw new IndexOutOfBoundsException("AST child index " + indexPre); 078 } //@ nowarn Exception; 079 080 public final String toString() { 081 return "[WhileStmt" 082 + " expr = " + this.expr 083 + " stmt = " + this.stmt 084 + " loc = " + this.loc 085 + " locGuardOpenParen = " + this.locGuardOpenParen 086 + "]"; 087 } 088 089 public final int getTag() { 090 return TagConstants.WHILESTMT; 091 } 092 093 public final void accept(Visitor v) { v.visitWhileStmt(this); } 094 095 public final Object accept(VisitorArgResult v, Object o) {return v.visitWhileStmt(this, o); } 096 097 public void check() { 098 super.check(); 099 this.expr.check(); 100 this.stmt.check(); 101 postCheck(); 102 } 103 104 //@ requires loc != javafe.util.Location.NULL; 105 //@ requires locGuardOpenParen != javafe.util.Location.NULL; 106 //@ ensures \result != null; 107 public static WhileStmt make(/*@ non_null @*/ Expr expr, /*@ non_null @*/ Stmt stmt, int loc, int locGuardOpenParen) { 108 //@ set I_will_establish_invariants_afterwards = true; 109 WhileStmt result = new WhileStmt(); 110 result.expr = expr; 111 result.stmt = stmt; 112 result.loc = loc; 113 result.locGuardOpenParen = locGuardOpenParen; 114 return result; 115 } 116 }