|
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 |
||||||||||
PREV NEXT | FRAMES NO FRAMES |
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 |
||||||||||
PREV NEXT | FRAMES NO FRAMES |