ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

escjava
Class AnnotationHandler

java.lang.Object
  extended byescjava.AnnotationHandler

public class AnnotationHandler
extends java.lang.Object

This class handles the desugaring of annotations.


Nested Class Summary
static class AnnotationHandler.CheckPurity
           
static class AnnotationHandler.Context
           
static class AnnotationHandler.NestedPragmaParser
          The routines in this class parse a sequence of ModifierPragma that occur prior to a method or constructor declaration.
static class AnnotationHandler.NonNullExpr
           
 
Field Summary
static LiteralExpr F
           
private static ModifierPragma heavyweightFlag
           
(package private) static AnnotationHandler.NestedPragmaParser specparser
           
static LiteralExpr T
           
protected  TypeDecl td
           
 
Constructor Summary
AnnotationHandler()
           
 
Method Summary
static ExprModifierPragma and(java.util.ArrayList a)
          Produces an ExprModifierPragma whose expression is the conjunction of all of the expressions in the ExprModifierPragmas in the argument.
static Expr and(Expr e1, Expr e2)
          Produces an expression which is the conjunction of the two expressions.
static ExprModifierPragma and(ExprModifierPragma e1, ExprModifierPragma e2)
          Produces an ExprModifierPragma whose expression is the conjunction of the expressions in the input pragmas.
static ExprModifierPragma andLabeled(java.util.ArrayList a)
          The same as and(ArrayList), but produces labelled expressions within the conjunction so that error messages come out with useful locations.
private  void checkMaybeAdd(Expr e, TypeNameVec tv, int locThrows)
           
 void checkSignalsOnly(ModifierPragmaVec mpv, RoutineDecl tde)
           
 void combineModifies(ModifierPragmaVec list)
           
static ModifiesGroupPragma defaultModifies(int loc, Expr req, RoutineDecl rd)
           
static VarExprModifierPragma defaultSignalsOnly(RoutineDecl tde, Expr req)
           
 void deNest(java.util.ArrayList ps, ModifierPragmaVec prefix, java.util.ArrayList deNestedSpecs)
           
 void deNest(ModifierPragmaVec m, ModifierPragmaVec prefix, java.util.ArrayList deNestedSpecs)
           
 ModifierPragmaVec desugar(java.util.ArrayList ps, RoutineDecl tde)
           
 void desugar(ModifierPragmaVec m, java.util.ArrayList requiresList, ModifierPragmaVec resultList, RoutineDecl tde)
           
 void desugar(RoutineDecl tde)
           
 void desugar(TypeDecl td)
           
protected  ModifierPragmaVec desugarAnnotations(ModifierPragmaVec pm, RoutineDecl tde)
           
 void fixDefaultSpecs(ModifierPragmaVec prefix)
           
 Expr forallWrap(GenericVarDeclVec foralls, Expr e)
           
 ModifierPragma forallWrap(GenericVarDeclVec foralls, ModifierPragma mp)
           
 ModifierPragmaVec getNonNull(RoutineDecl rd)
           
 void handlePragmas(CompilationUnit cu)
          This must be called on a compilation unit to get the model imports listed, so that type names used in annotations can be found, and to get model methods put into the class's signature.
 void handlePragmas(TypeDeclElem tde)
           
 void handleTypeDecl(TypeDecl td)
          After parsing, but before type checking, we need to convert model methods to regular methods, so that names are resolved correctly; also need to set ACC_PURE bits correctly in all classes so that later checks get done correctly.
static Expr implies(Expr e1, Expr e2)
          Produces an expression which is the implication of the two expressions.
(package private) static boolean isFalse(Expr e)
          Returns true if the argument is literally false, and returns false if it is not a literal or is literally true.
private  boolean isInSignalsOnlyExpr(Type t, Expr e, boolean allowSuperTypes)
           
(package private) static boolean isTrue(Expr e)
          Returns true if the argument is literally true, and returns false if it is not a literal or is literally false.
static ExprModifierPragma or(java.util.ArrayList a)
          Produces an ExprModifierPragma whose expression is the disjunction of all of the expressions in the ExprModifierPragmas in the argument.
static ExprModifierPragma or(ExprModifierPragma e1, ExprModifierPragma e2)
          Produces an ExprModifierPragma whose expression is the disjunction of the expressions in the input pragmas.
 void parseAllRoutineSpecs(CompilationUnit ccu)
           
private static void print(Expr e)
           
static void printSpec(ModifierPragma mp)
           
static void printSpecs(RoutineDecl tde)
           
protected  void process(RoutineDecl tde)
           
 void process(TypeDeclElem tde)
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

td

protected TypeDecl td

T

public static final LiteralExpr T

F

public static final LiteralExpr F

specparser

static AnnotationHandler.NestedPragmaParser specparser

heavyweightFlag

private static ModifierPragma heavyweightFlag
Constructor Detail

AnnotationHandler

public AnnotationHandler()
Method Detail

handlePragmas

public void handlePragmas(CompilationUnit cu)
This must be called on a compilation unit to get the model imports listed, so that type names used in annotations can be found, and to get model methods put into the class's signature. It is called as part of EscSrcReader, a subclass of SrcReader, defined in EscTypeReader.


handleTypeDecl

public void handleTypeDecl(TypeDecl td)
After parsing, but before type checking, we need to convert model methods to regular methods, so that names are resolved correctly; also need to set ACC_PURE bits correctly in all classes so that later checks get done correctly.


handlePragmas

public void handlePragmas(TypeDeclElem tde)

process

public void process(TypeDeclElem tde)

process

protected void process(RoutineDecl tde)

desugar

public void desugar(TypeDecl td)

desugar

public void desugar(RoutineDecl tde)

printSpecs

public static void printSpecs(RoutineDecl tde)

printSpec

public static void printSpec(ModifierPragma mp)

desugarAnnotations

protected ModifierPragmaVec desugarAnnotations(ModifierPragmaVec pm,
                                               RoutineDecl tde)

checkSignalsOnly

public void checkSignalsOnly(ModifierPragmaVec mpv,
                             RoutineDecl tde)

checkMaybeAdd

private void checkMaybeAdd(Expr e,
                           TypeNameVec tv,
                           int locThrows)

getNonNull

public ModifierPragmaVec getNonNull(RoutineDecl rd)

desugar

public ModifierPragmaVec desugar(java.util.ArrayList ps,
                                 RoutineDecl tde)

desugar

public void desugar(ModifierPragmaVec m,
                    java.util.ArrayList requiresList,
                    ModifierPragmaVec resultList,
                    RoutineDecl tde)

isInSignalsOnlyExpr

private boolean isInSignalsOnlyExpr(Type t,
                                    Expr e,
                                    boolean allowSuperTypes)

defaultSignalsOnly

public static final VarExprModifierPragma defaultSignalsOnly(RoutineDecl tde,
                                                             Expr req)

defaultModifies

public static final ModifiesGroupPragma defaultModifies(int loc,
                                                        Expr req,
                                                        RoutineDecl rd)

forallWrap

public ModifierPragma forallWrap(GenericVarDeclVec foralls,
                                 ModifierPragma mp)

forallWrap

public Expr forallWrap(GenericVarDeclVec foralls,
                       Expr e)

deNest

public void deNest(java.util.ArrayList ps,
                   ModifierPragmaVec prefix,
                   java.util.ArrayList deNestedSpecs)

combineModifies

public void combineModifies(ModifierPragmaVec list)

deNest

public void deNest(ModifierPragmaVec m,
                   ModifierPragmaVec prefix,
                   java.util.ArrayList deNestedSpecs)

fixDefaultSpecs

public void fixDefaultSpecs(ModifierPragmaVec prefix)

and

public static Expr and(Expr e1,
                       Expr e2)
Produces an expression which is the conjunction of the two expressions. If either input is null, the other is returned. If either input is literally true or false, the appropriate constant folding is performed.


and

public static ExprModifierPragma and(ExprModifierPragma e1,
                                     ExprModifierPragma e2)
Produces an ExprModifierPragma whose expression is the conjunction of the expressions in the input pragmas. If either input is null, the other is returned. If either input is literally true or false, the appropriate constant folding is performed.


and

public static ExprModifierPragma and(java.util.ArrayList a)
Produces an ExprModifierPragma whose expression is the conjunction of all of the expressions in the ExprModifierPragmas in the argument. If the argument is empty, null is returned. Otherwise, some object is returned, though its expression might be a literal.


andLabeled

public static ExprModifierPragma andLabeled(java.util.ArrayList a)
The same as and(ArrayList), but produces labelled expressions within the conjunction so that error messages come out with useful locations.


or

public static ExprModifierPragma or(ExprModifierPragma e1,
                                    ExprModifierPragma e2)
Produces an ExprModifierPragma whose expression is the disjunction of the expressions in the input pragmas. If either input is null, the other is returned. If either input is literally true or false, the appropriate constant folding is performed.


or

public static ExprModifierPragma or(java.util.ArrayList a)
Produces an ExprModifierPragma whose expression is the disjunction of all of the expressions in the ExprModifierPragmas in the argument. If the argument is empty, null is returned. Otherwise, some object is returned, though its expression might be a literal.


implies

public static Expr implies(Expr e1,
                           Expr e2)
Produces an expression which is the implication of the two expressions. Neither input may be null. If either input is literally true or false, the appropriate constant folding is performed.


isTrue

static boolean isTrue(Expr e)
Returns true if the argument is literally true, and returns false if it is not a literal or is literally false.


isFalse

static boolean isFalse(Expr e)
Returns true if the argument is literally false, and returns false if it is not a literal or is literally true.


print

private static void print(Expr e)

parseAllRoutineSpecs

public void parseAllRoutineSpecs(CompilationUnit ccu)

ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

The ESC/Java2 Project Homepage