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 abstract class AssignCmd extends GuardedCmd
032    {
033      // denotes a subtype-dependent assignment to v
034      // rhs must be pure
035      public /*@ non_null @*/ VariableAccess v;
036    
037      public /*@ non_null @*/ Expr rhs;
038    
039    
040      //@ public represents startLoc <- v.getStartLoc();
041      public /*@ pure @*/ int getStartLoc() { return v.getStartLoc(); }
042      /*@ also
043        @ public normal_behavior
044        @ ensures \result == rhs.getEndLoc();
045        @*/
046      public /*@ pure @*/ int getEndLoc() { return rhs.getEndLoc(); }
047    
048    
049    // Generated boilerplate constructors:
050    
051      //@ ensures this.v == v;
052      //@ ensures this.rhs == rhs;
053      protected AssignCmd(/*@ non_null @*/ VariableAccess v, /*@ non_null @*/ Expr rhs) {
054         super();
055         this.v = v;
056         this.rhs = rhs;
057      }
058      public void check() {
059         super.check();
060         this.v.check();
061         this.rhs.check();
062      }
063    
064    }