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

Uses of Interface
javafe.parser.PragmaParser

Packages that use PragmaParser
escjava   
escjava.parser   
escjava.reader   
javafe   
javafe.parser   
javafe.reader   
 

Uses of PragmaParser in escjava
 

Methods in escjava that return PragmaParser
 PragmaParser Main.makePragmaParser()
          Returns the EscPragmaParser.
 

Methods in escjava with parameters of type PragmaParser
 StandardTypeReader Main.makeStandardTypeReader(java.lang.String path, java.lang.String sourcePath, PragmaParser P)
          Returns the Esc StandardTypeReader, EscTypeReader.
 

Uses of PragmaParser in escjava.parser
 

Classes in escjava.parser that implement PragmaParser
 class ErrorPragmaParser
          This class produces a PragmaParser that reports an client-chosen error message each time an annotation comment is encountered.
 class EscPragmaParser
          Grammar: Pragma ::= LexicalPragma | ModifierPragma | TypeDeclElemPragma | StmtPragma LexicalPragma ::= "nowarn" [ Idn [',' Idn]* ] [';'] StmtPragma ::= SimpleStmtPragma [';'] | ExprStmtPragma SpecExpr [';'] | 'set' PrimaryExpr '=' SpecExpr [';'] SimpleStmtPragma ::= 'unreachable' ExprStmtPragma ::= 'assume' | 'assume_redundantly' | 'assert' | 'assert_redundantly' | 'loop_inv' | 'loop_invariant' | 'loop_invariant_redundantly' | 'decreases' | 'decreases_redundantly' | 'loop_predicate' | 'maintaining' | 'maintaining_redundantly' | 'decreasing' | 'decreasing_redundantly' TypeDeclElemPragma ::= ExprDeclPragma SpecExpr [';'] | 'ghost' Modifiers Type VariableDeclarator [';'] | 'still_deferred' Idn [',' Idn]* [';'] ExprDeclPragma ::= 'axiom' | 'invariant' | 'invariant_redundantly' ModifierPragma ::= [PrivacyPragma] [BehaviorPragma] SimpleModifierPragma [PrivacyPragma] [BehaviorPragma] NonSimpleModifierPragma NonSimpleModifierPragma ::= | ['also'] ExprModifierPragma SpecExpr [';'] | ['also'] VarExprModifierPragma '(' Type Idn ')' SpecExpr [';'] | ['also'] 'monitored_by' SpecExpr [',' SpecExpr]* [';'] | ['also'] ModifierPragma SpecDesignator [',' SpecDesignator]* [';'] PrivacyPragma ::= 'public' | 'private' | 'protected' BehaviorPragma ::= 'behavior' | 'normal_behavior' | 'exceptional_behavior' SimpleModifierPragma ::= 'uninitialized' | 'monitored' | 'non_null' | 'instance' | 'pure' | 'spec_public' | 'writable_deferred' | 'helper' | 'public' | 'private' | 'protected' | 'spec_protected' | 'model' | 'transient' | '\peer' | '\readonly' | '\rep' | 'may_be_null' | 'non_null_ref_by_default' | 'null_ref_by_default' | 'obs_pure' | 'code_java_math' | 'code_safe_math' | 'code_bigint_math' | 'spec_java_math' | 'spec_safe_math' | 'spec_bigint_math' ExprModifierPragma ::= 'readable_if' | 'writable_if' | 'requires' | 'requires_redundantly' | 'also_requires' (if Main.allowAlsoRequires) | 'ensures' | 'ensures_redundantly' | 'also_ensures' | 'pre' | 'pre_redundantly' | 'post' | 'post_redundantly' VarExprModifierPragma ::= 'exsures' | 'exsures_redundantly' | 'also_exsures" | 'signals' | 'signals_redundantly' ModifierPragma ::= 'modifies' | 'modifies_redundantly' | 'also_modifies' | 'modifiable' | 'modifiable_redundantly' | 'assignable' | 'assignable_redundantly' DurationClause ::= DurationKeyword '\not_specified' ';' | DurationKeyword DurSpecExpr [ 'if' predicate ] ';' DurSpecExpr ::= SpecExpr (of type long) OpWithLongResult DurSpecExpr | '\duration' '(' MethodInvOrConstructor ')' LongOp DurSpecExpr; MethodInvOrConstructorOrNotSpecified ::= MethodInvOrConstructor | '\not_specified'; InvariantForExpr ::= '\invariant_for' '(' SpecExpr ')' ';' SpaceExpr ::= '\space' '(' SpecExpr ')' IsInitializedExpr ::= '\is_initialized' '(' Idn ')' ';' InvariantFor ::= '\invariant_for' '(' SpecExpr ')' ';' WorkingSpaceClause ::= WorkingSpaceKeyword '\not_specified' ';' | WorkingSpaceKeyword WorkingSpaceSpecExpr [ 'if' predicate ] ';' WorkingSpaceSpecExpr ::= SpecExpr (of type int) OpWithIntResult WorkingSpaceSpecExpr | '\working_space' '(' MethodInvOrConstructor ')' IntOp WorkingSpaceSpecExpr MethodInvOrConstructor ::= MethodInvocation | ConstructorInvocation OpWithIntResult ::= STAR | '/' | '%' | PLUS | '-' | '&' | BITOR | '^' WorkingSpaceKeyword ::= 'working_space' | 'working_space_redundantly' DurationKeyword ::= 'duration' | 'duration_redundantly' PrivateDataKeyword ::= '\private_data' NotModifiedExpr ::= '\not_modified' '(' SpecDesignator [',' SpecDesignator]* ')' ';' ReachExpr ::= '\reach' '(' SpecExpr [ ',' Idn [ ',' StoreRefExpr ] ] ')' ';' FieldsOfExpr ::= '\fields_of' '(' SpecExpr [ ',' Idn [ ',' StoreRefExpr ] ] ')' ';' OtherExpr ::= '\other' [ StoreRefNameSuffix ] ';' ReachExpr ::= '\reach' '(' SpecExpr [ ',' Idn [ ',' StoreRefExpr ] ] ')' ';' StoreRefList ::= StoreRef [ ',' StoreRef ] ...
 

Constructors in escjava.parser with parameters of type PragmaParser
EscPragmaLex(PragmaParser pragmaParser, boolean isJava)
           
 

Uses of PragmaParser in escjava.reader
 

Methods in escjava.reader with parameters of type PragmaParser
static StandardTypeReader EscTypeReader.make(Query Q, Query sourceQ, PragmaParser pragmaP, AnnotationHandler ah)
          Create a EscTypeReader from a non-null query engine and a pragma parser.
static StandardTypeReader EscTypeReader.make(java.lang.String path, java.lang.String srcPath, PragmaParser pragmaP, AnnotationHandler ah)
          Create a EscTypeReader using a given Java classpath for our underlying Java file space and a given pragma parser.
static StandardTypeReader EscTypeReader.make(PragmaParser pragmaP)
          Create a EscTypeReader using a the default Java classpath for our underlying Java file space and a given pragma parser.
 

Uses of PragmaParser in javafe
 

Methods in javafe that return PragmaParser
 PragmaParser FrontEndTool.makePragmaParser()
          Called to obtain the pragma parser to be used for parsing input files.
 

Methods in javafe with parameters of type PragmaParser
 StandardTypeReader FrontEndTool.makeStandardTypeReader(java.lang.String path, java.lang.String sourcePath, PragmaParser P)
          Called to obtain the StandardTypeReader to be used for locating and reading in types.
 

Uses of PragmaParser in javafe.parser
 

Fields in javafe.parser declared as PragmaParser
protected  PragmaParser Lex.pragmaParser
           
 

Constructors in javafe.parser with parameters of type PragmaParser
Lex(PragmaParser pragmaParser, boolean isJava)
          Creates a lexical analyzer that will tokenize the characters read from an underlying CorrelatedReader.
 

Uses of PragmaParser in javafe.reader
 

Methods in javafe.reader with parameters of type PragmaParser
static StandardTypeReader StandardTypeReader.make(Query Q, Query sourceQ, PragmaParser pragmaP)
          Create a StandardTypeReader from a query engine and a pragma parser.
static StandardTypeReader StandardTypeReader.make(java.lang.String path, java.lang.String sourcePath, PragmaParser pragmaP)
          Create a StandardTypeReader using a given Java classpath for our underlying Java file space and a given pragma parser.
static StandardTypeReader StandardTypeReader.make(PragmaParser pragmaP)
          Create a StandardTypeReader using a the default Java classpath for our underlying Java file space and a given pragma parser.
 

Constructors in javafe.reader with parameters of type PragmaParser
SrcReader(PragmaParser p)
           
 


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