001    // -*- mode: java -*-
002    /* Copyright 2000, 2001, Compaq Computer Corporation */
003    
004    /* IF THIS IS A JAVA FILE, DO NOT EDIT IT!  
005    
006       Most Java files in this directory which are part of the Javafe AST
007       are automatically generated using the astgen comment (see
008       ESCTools/Javafe/astgen) from the input file 'hierarchy.h'.  If you
009       wish to modify AST classes or introduce new ones, modify
010       'hierarchy.j.'
011     */
012    
013    package javafe.ast;
014    
015    import javafe.util.Assert;
016    import javafe.util.Location;
017    import javafe.util.ErrorSet;
018    
019    // Convention: unless otherwise noted, integer fields named "loc" refer
020    // to the location of the first character of the syntactic unit
021    
022    
023    /**
024     * Represents various kinds of field access expressions. 
025     * The FieldDecl is filled in by the name resolution code.
026     */
027    
028    public class FieldAccess extends Expr
029    {
030      public /*@ non_null @*/ ObjectDesignator od;
031    
032      public /*@ non_null @*/ Identifier id;
033    
034      //@ invariant locId != javafe.util.Location.NULL;
035      public int locId;
036    
037    
038      //@ invariant decl == null || decl.id==id;
039      public FieldDecl decl;
040    
041      private void postCheck() {
042        if (decl != null) {
043          Assert.notFalse(id == decl.id);
044          // Any other invariants here...???
045        }
046      }
047      //@ public represents startLoc <- (od.getStartLoc() == Location.NULL) ? locId : od.getStartLoc();
048      public /*@ pure @*/ int getStartLoc() { 
049        int locOd = od.getStartLoc();
050        if (locOd == Location.NULL) 
051          return locId;
052        else
053          return locOd;
054      }
055      //@ also public normal_behavior
056      //@ ensures \result == locId;
057      public /*@ pure @*/ int getEndLoc() { return locId; }
058    
059      //@ requires locId != javafe.util.Location.NULL;
060      public static /*@non_null*/ FieldAccess make(/*@ non_null @*/ ObjectDesignator od, 
061                                     /*@ non_null @*/ Identifier id, 
062                                     int locId) {
063         FieldAccess result = new FieldAccess(
064                                  od,
065                                  id,
066                                  locId);
067         result.decl = null; // Easier than puting an ensures on constructor
068         return result;
069      }
070    
071    
072    // Generated boilerplate constructors:
073    
074      //@ ensures this.od == od;
075      //@ ensures this.id == id;
076      //@ ensures this.locId == locId;
077      protected FieldAccess(/*@ non_null @*/ ObjectDesignator od, /*@ non_null @*/ Identifier id, int locId) {
078         super();
079         this.od = od;
080         this.id = id;
081         this.locId = locId;
082      }
083    
084    // Generated boilerplate methods:
085    
086      public final int childCount() {
087         return 2;
088      }
089    
090      public final Object childAt(int index) {
091              /*throws IndexOutOfBoundsException*/
092         if (index < 0)
093            throw new IndexOutOfBoundsException("AST child index " + index);
094         int indexPre = index;
095    
096         int sz;
097    
098         if (index == 0) return this.od;
099         else index--;
100    
101         if (index == 0) return this.id;
102         else index--;
103    
104         throw new IndexOutOfBoundsException("AST child index " + indexPre);
105      }   //@ nowarn Exception;
106    
107      public final /*@non_null*/String toString() {
108         return "[FieldAccess"
109            + " od = " + this.od
110            + " id = " + this.id
111            + " locId = " + this.locId
112            + "]";
113      }
114    
115      public final int getTag() {
116         return TagConstants.FIELDACCESS;
117      }
118    
119      public final void accept(Visitor v) { v.visitFieldAccess(this); }
120    
121      public final Object accept(VisitorArgResult v, Object o) {return v.visitFieldAccess(this, o); }
122    
123      public void check() {
124         super.check();
125         this.od.check();
126         if (this.id == null) throw new RuntimeException();
127         postCheck();
128      }
129    
130    }