jif.extension
Class JifConstructorDeclExt

java.lang.Object
  extended bypolyglot.ext.jl.ast.Ext_c
      extended byjif.ast.Jif_c
          extended byjif.extension.JifProcedureDeclExt_c
              extended byjif.extension.JifConstructorDeclExt
All Implemented Interfaces:
java.lang.Cloneable, polyglot.util.Copy, polyglot.ast.Ext, Jif, JifProcedureDeclExt

public class JifConstructorDeclExt
extends JifProcedureDeclExt_c

The Jif extension of the JifConstructorDecl node.

See Also:
ConstructorDecl, JifConstructorDecl

Field Summary
 
Fields inherited from class jif.ast.Jif_c
del, toJava, X
 
Fields inherited from class polyglot.ext.jl.ast.Ext_c
ext, node
 
Constructor Summary
JifConstructorDeclExt(ToJavaExt toJava)
           
 
Method Summary
protected  void checkFinalFieldAssignment(polyglot.ast.Stmt s, java.util.Set uninitFinalVars, LabelChecker lc)
          Check if the stmt is an assignment to a final field.
protected  polyglot.ast.Block checkInitsAndBody(Label Li, JifConstructorInstance ci, polyglot.ast.Block body, LabelChecker lc)
          This method implements the check-inits predicate of the thesis (Figures 4.41-45).
 polyglot.ast.Node labelCheck(LabelChecker lc)
          Label check the node to which this extension is attached.
protected static java.util.Set uninitFinalFields(polyglot.types.ReferenceType type)
          Utility method to get the set of field instances of final fields of the given ReferenceType that do not have an initializer.
 
Methods inherited from class jif.extension.JifProcedureDeclExt_c
addCallers, addReturnConstraints, checkActsForAuthority, checkArguments, constrainPH, constraintAuth
 
Methods inherited from class jif.ast.Jif_c
copy, del, del, init, toJava, toJava, X, X, X, X
 
Methods inherited from class polyglot.ext.jl.ast.Ext_c
ext, ext, node, toString
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 
Methods inherited from interface jif.ast.Jif
del, del, toJava, toJava, X, X
 
Methods inherited from interface polyglot.ast.Ext
ext, ext, init, node
 
Methods inherited from interface polyglot.util.Copy
copy
 

Constructor Detail

JifConstructorDeclExt

public JifConstructorDeclExt(ToJavaExt toJava)
Method Detail

labelCheck

public polyglot.ast.Node labelCheck(LabelChecker lc)
                             throws polyglot.types.SemanticException
Description copied from interface: Jif
Label check the node to which this extension is attached.

Specified by:
labelCheck in interface Jif
Overrides:
labelCheck in class Jif_c
Throws:
polyglot.types.SemanticException

uninitFinalFields

protected static java.util.Set uninitFinalFields(polyglot.types.ReferenceType type)
Utility method to get the set of field instances of final fields of the given ReferenceType that do not have an initializer.


checkInitsAndBody

protected polyglot.ast.Block checkInitsAndBody(Label Li,
                                               JifConstructorInstance ci,
                                               polyglot.ast.Block body,
                                               LabelChecker lc)
                                        throws polyglot.types.SemanticException
This method implements the check-inits predicate of the thesis (Figures 4.41-45).

Throws:
polyglot.types.SemanticException

checkFinalFieldAssignment

protected void checkFinalFieldAssignment(polyglot.ast.Stmt s,
                                         java.util.Set uninitFinalVars,
                                         LabelChecker lc)
                                  throws polyglot.types.SemanticException
Check if the stmt is an assignment to a final field. Moreover, if the final field is a label, and it is being initialized from a final label, share the uids of the fields.

Throws:
polyglot.types.SemanticException