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 escjava.ast;
014    
015    import java.util.Hashtable;
016    import java.util.Set;
017    import java.util.ArrayList;
018    
019    import javafe.ast.*;
020    import javafe.util.Assert;
021    import javafe.util.Location;
022    import escjava.ParsedRoutineSpecs;
023    
024    // Convention: unless otherwise noted, integer fields named "loc" refer
025    // to the location of the first character of the syntactic unit
026    
027    //# TagBase javafe.tc.TagConstants.LAST_TAG + 1
028    //# VisitorRoot javafe.ast.Visitor
029    
030    
031    public class ModelDeclPragma extends TypeDeclElemPragma
032    {
033      public /*@ non_null @*/ FieldDecl decl;
034    
035      public int loc;
036    
037    
038      public void setParent(/*@non_null*/TypeDecl p) {
039        super.setParent(p);
040        if (decl != null)
041            decl.setParent(p);
042      }
043    
044      //@ public represents startLoc <- loc;
045      public /*@ pure @*/ int getStartLoc() { return loc; }
046      /*@ also
047        @ public normal_behavior
048        @ ensures \result == decl.getEndLoc();
049        @*/
050      public /*@ pure @*/ int getEndLoc() { return decl.getEndLoc(); }
051      public void decorate(ModifierPragmaVec modifierPragmas) {
052        if (decl.pmodifiers == null) {
053            decl.pmodifiers = modifierPragmas;
054        } else if (modifierPragmas != null) {
055            // FIXME - should be prepen???
056            decl.pmodifiers.append(modifierPragmas); 
057        }
058      }
059      public ModifierPragmaVec getPModifiers() { return decl.pmodifiers; }
060    
061    
062    // Generated boilerplate constructors:
063    
064      //@ ensures this.decl == decl;
065      //@ ensures this.loc == loc;
066      protected ModelDeclPragma(/*@ non_null @*/ FieldDecl decl, int loc) {
067         this.decl = decl;
068         this.loc = loc;
069      }
070    
071    // Generated boilerplate methods:
072    
073      public final int childCount() {
074         return 1;
075      }
076    
077      public final Object childAt(int index) {
078              /*throws IndexOutOfBoundsException*/
079         if (index < 0)
080            throw new IndexOutOfBoundsException("AST child index " + index);
081         int indexPre = index;
082    
083         int sz;
084    
085         if (index == 0) return this.decl;
086         else index--;
087    
088         throw new IndexOutOfBoundsException("AST child index " + indexPre);
089      }   //@ nowarn Exception;
090    
091      public final /*@non_null*/String toString() {
092         return "[ModelDeclPragma"
093            + " decl = " + this.decl
094            + " loc = " + this.loc
095            + "]";
096      }
097    
098      public final int getTag() {
099         return TagConstants.MODELDECLPRAGMA;
100      }
101    
102      public final void accept(javafe.ast.Visitor v) { 
103        if (v instanceof Visitor) ((Visitor)v).visitModelDeclPragma(this);
104      }
105    
106      public final Object accept(javafe.ast.VisitorArgResult v, Object o) { 
107        if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitModelDeclPragma(this, o); else return null;
108      }
109    
110      public void check() {
111         this.decl.check();
112      }
113    
114      //@ ensures \result != null;
115      public static ModelDeclPragma make(/*@ non_null @*/ FieldDecl decl, int loc) {
116         ModelDeclPragma result = new ModelDeclPragma(decl, loc);
117         return result;
118      }
119    }