de.uka.ilkd.key.java.recoderext

Class SchemaJavaProgramFactory

java.lang.Object

recoder.java.JavaProgramFactory

de.uka.ilkd.key.java.recoderext.SchemaJavaProgramFactory

All Implemented Interfaces:

java.beans.PropertyChangeListener, java.util.EventListener, ProgramFactory, Service

public class SchemaJavaProgramFactory
extends JavaProgramFactory

Field Summary

Fields

Modifier and Type	Field and Description
private static SchemaJavaParser	parser For internal reuse and synchronization.
protected Namespace<SchemaVariable>	svns
private static SchemaJavaProgramFactory	theFactory The singleton instance of the program factory.
private static SourceElement.Position	ZERO_POSITION

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	SchemaJavaProgramFactory() Protected constructor - use getInstance() instead.

Method Summary

Modifier and Type	Method and Description
private static void	attachComment(Comment c, ProgramElement pe)
ContextStatementBlock	createContextStatementBlock(ExecCtxtSVWrapper ec)
ContextStatementBlock	createContextStatementBlock(TypeSVWrapper typeRef, MethodSignatureSVWrapper pm, ExpressionSVWrapper var)
Identifier	createIdentifier(java.lang.String text)
ImplicitIdentifier	createImplicitIdentifier(java.lang.String text) Create an ImplicitIdentifier.
LoopScopeBlock	createLoopScopeBlock()
MergePointStatement	createMergePointStatement()
MergePointStatement	createMergePointStatement(Expression e)
PassiveExpression	createPassiveExpression() Create a PassiveExpression.
PassiveExpression	createPassiveExpression(Expression e) Create a PassiveExpression.
RKeYMetaConstruct	createRKeYMetaConstruct()
RKeYMetaConstructExpression	createRKeYMetaConstructExpression()
RKeYMetaConstructType	createRKeYMetaConstructType()
RMethodBodyStatement	createRMethodBodyStatement(TypeReference typeRef, ProgramVariableSVWrapper resVar, MethodReference mr)
RMethodCallStatement	createRMethodCallStatement(ProgramVariableSVWrapper resVar, ExecutionContext esvw, Statement st)
SpecialReferenceWrapper	createThisReference(TypeReference typeRef, Expression var)
CatchSVWrapper	getCatchSV(java.lang.String s)
ExecCtxtSVWrapper	getExecutionContextSV(java.lang.String s)
ExpressionSVWrapper	getExpressionSV(java.lang.String s)
static JavaProgramFactory	getInstance() Returns the single instance of this class.
JumpLabelSVWrapper	getJumpLabelSV(java.lang.String s)
LabelSVWrapper	getLabelSV(java.lang.String s)
MethodSignatureSVWrapper	getMethodSignatureSVWrapper(java.lang.String s)
ProgramVariableSVWrapper	getProgramVariableSV(java.lang.String s)
StatementSVWrapper	getStatementSV(java.lang.String s)
TypeSVWrapper	getTypeSV(java.lang.String s)
SchemaVariable	lookupSchemaVariable(java.lang.String s)
boolean	lookupSchemaVariableType(java.lang.String s, ProgramSVSort sort)
CompilationUnit	parseCompilationUnit(java.io.Reader in) Parse a CompilationUnit from the given reader.
ConstructorDeclaration	parseConstructorDeclaration(java.io.Reader in) Parse a ConstructorDeclaration from the given reader.
Expression	parseExpression(java.io.Reader in) Parse an Expression from the given reader.
FieldDeclaration	parseFieldDeclaration(java.io.Reader in) Parse a FieldDeclaration from the given reader.
MemberDeclaration	parseMemberDeclaration(java.io.Reader in) Parse a MemberDeclaration from the given reader.
MethodDeclaration	parseMethodDeclaration(java.io.Reader in) Parse a MethodDeclaration from the given reader.
ParameterDeclaration	parseParameterDeclaration(java.io.Reader in) Parse a ParameterDeclaration from the given reader.
StatementBlock	parseStatementBlock(java.io.Reader in) Parse a StatementBlock from the given string.
ASTList<Statement>	parseStatements(java.io.Reader in) Parse some Statements from the given reader.
TypeDeclaration	parseTypeDeclaration(java.io.Reader in) Parse a TypeDeclaration from the given reader.
TypeReference	parseTypeReference(java.io.Reader in) Parse a TypeReference from the given reader.
private static void	postWork(ProgramElement pe) Perform post work on the created element.
void	setSVNamespace(Namespace<SchemaVariable> ns)
static void	throwSortInvalid(SchemaVariable sv, java.lang.String s)

Methods inherited from class recoder.java.JavaProgramFactory

createAbstract, createAnnotationDeclaration, createAnnotationDeclaration, createAnnotationPropertyDeclaration, createAnnotationPropertyReference, createAnnotationPropertyReference, createAnnotationUseSpecification, createArrayInitializer, createArrayInitializer, createArrayLengthReference, createArrayLengthReference, createArrayReference, createArrayReference, createAssert, createAssert, createAssert, createBinaryAnd, createBinaryAnd, createBinaryAndAssignment, createBinaryAndAssignment, createBinaryNot, createBinaryNot, createBinaryOr, createBinaryOr, createBinaryOrAssignment, createBinaryOrAssignment, createBinaryXOr, createBinaryXOr, createBinaryXOrAssignment, createBinaryXOrAssignment, createBooleanLiteral, createBooleanLiteral, createBreak, createBreak, createCase, createCase, createCase, createCatch, createCatch, createCharLiteral, createCharLiteral, createCharLiteral, createClassDeclaration, createClassDeclaration, createClassDeclaration, createClassInitializer, createClassInitializer, createClassInitializer, createComment, createComment, createComment, createCompilationUnit, createCompilationUnit, createConditional, createConditional, createConstructorDeclaration, createConstructorDeclaration, createContinue, createContinue, createCopyAssignment, createCopyAssignment, createDefault, createDefault, createDivide, createDivide, createDivideAssignment, createDivideAssignment, createDo, createDo, createDo, createDocComment, createDocComment, createDoubleLiteral, createDoubleLiteral, createDoubleLiteral, createElse, createElse, createEmptyStatement, createEnhancedFor, createEquals, createEquals, createExtends, createExtends, createExtends, createFieldDeclaration, createFieldDeclaration, createFieldDeclaration, createFieldDeclaration, createFieldReference, createFieldReference, createFieldReference, createFieldSpecification, createFieldSpecification, createFieldSpecification, createFieldSpecification, createFinal, createFinally, createFinally, createFloatLiteral, createFloatLiteral, createFloatLiteral, createFor, createFor, createGreaterOrEquals, createGreaterOrEquals, createGreaterThan, createGreaterThan, createIdentifier, createIf, createIf, createIf, createIf, createIf, createImplements, createImplements, createImplements, createImport, createImport, createImport, createInstanceof, createInstanceof, createInterfaceDeclaration, createInterfaceDeclaration, createIntLiteral, createIntLiteral, createIntLiteral, createLabeledStatement, createLabeledStatement, createLabeledStatement, createLessOrEquals, createLessOrEquals, createLessThan, createLessThan, createLocalVariableDeclaration, createLocalVariableDeclaration, createLocalVariableDeclaration, createLocalVariableDeclaration, createLogicalAnd, createLogicalAnd, createLogicalNot, createLogicalNot, createLogicalOr, createLogicalOr, createLongLiteral, createLongLiteral, createLongLiteral, createMetaClassReference, createMetaClassReference, createMethodDeclaration, createMethodDeclaration, createMethodDeclaration, createMethodReference, createMethodReference, createMethodReference, createMethodReference, createMethodReference, createMethodReference, createMinus, createMinus, createMinusAssignment, createMinusAssignment, createModulo, createModulo, createModuloAssignment, createModuloAssignment, createNative, createNegative, createNegative, createNew, createNew, createNew, createNewArray, createNewArray, createNewArray, createNotEquals, createNotEquals, createNullLiteral, createPackageReference, createPackageReference, createPackageReference, createPackageSpecification, createPackageSpecification, createParameterDeclaration, createParameterDeclaration, createParameterDeclaration, createParenthesizedExpression, createParenthesizedExpression, createPlus, createPlus, createPlusAssignment, createPlusAssignment, createPositive, createPositive, createPostDecrement, createPostDecrement, createPostIncrement, createPostIncrement, createPreDecrement, createPreDecrement, createPreIncrement, createPreIncrement, createPrivate, createProtected, createPublic, createReturn, createReturn, createShiftLeft, createShiftLeft, createShiftLeftAssignment, createShiftLeftAssignment, createShiftRight, createShiftRight, createShiftRightAssignment, createShiftRightAssignment, createSingleLineComment, createSingleLineComment, createStatementBlock, createStatementBlock, createStatic, createStaticImport, createStaticImport, createStrictFp, createStringLiteral, createStringLiteral, createSuperConstructorReference, createSuperConstructorReference, createSuperConstructorReference, createSuperReference, createSuperReference, createSwitch, createSwitch, createSwitch, createSynchronized, createSynchronizedBlock, createSynchronizedBlock, createSynchronizedBlock, createThen, createThen, createThisConstructorReference, createThisConstructorReference, createThisReference, createThisReference, createThrow, createThrow, createThrows, createThrows, createThrows, createTimes, createTimes, createTimesAssignment, createTimesAssignment, createTransient, createTry, createTry, createTry, createTypeCast, createTypeCast, createTypeReference, createTypeReference, createTypeReference, createTypeReference, createUncollatedReferenceQualifier, createUncollatedReferenceQualifier, createUncollatedReferenceQualifier, createUnsignedShiftRight, createUnsignedShiftRight, createUnsignedShiftRightAssignment, createUnsignedShiftRightAssignment, createVariableReference, createVariableReference, createVariableSpecification, createVariableSpecification, createVariableSpecification, createVariableSpecification, createVolatile, createWhile, createWhile, createWhile, getPrettyPrinter, getServiceConfiguration, initialize, main, parseCompilationUnit, parseCompilationUnits, parseConstructorDeclaration, parseExpression, parseFieldDeclaration, parseInt, parseLong, parseMemberDeclaration, parseMethodDeclaration, parseParameterDeclaration, parseStatements, parseTypeDeclaration, parseTypeReference, propertyChange

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

svns

protected Namespace<SchemaVariable> svns

theFactory

private static SchemaJavaProgramFactory theFactory

The singleton instance of the program factory.

parser

private static final SchemaJavaParser parser

For internal reuse and synchronization.

ZERO_POSITION

private static final SourceElement.Position ZERO_POSITION

Constructor Detail

SchemaJavaProgramFactory

protected SchemaJavaProgramFactory()

Protected constructor - use getInstance() instead.

Method Detail

getInstance

public static JavaProgramFactory getInstance()

Returns the single instance of this class.

createImplicitIdentifier

public ImplicitIdentifier createImplicitIdentifier(java.lang.String text)

Create an ImplicitIdentifier.

createIdentifier

public Identifier createIdentifier(java.lang.String text)

Specified by:

createIdentifier in interface ProgramFactory

Overrides:

createIdentifier in class JavaProgramFactory

createThisReference

public SpecialReferenceWrapper createThisReference(TypeReference typeRef,
                                                   Expression var)

createRMethodCallStatement

public RMethodCallStatement createRMethodCallStatement(ProgramVariableSVWrapper resVar,
                                                       ExecutionContext esvw,
                                                       Statement st)

createLoopScopeBlock

public LoopScopeBlock createLoopScopeBlock()

createRMethodBodyStatement

public RMethodBodyStatement createRMethodBodyStatement(TypeReference typeRef,
                                                       ProgramVariableSVWrapper resVar,
                                                       MethodReference mr)

createRKeYMetaConstruct

public RKeYMetaConstruct createRKeYMetaConstruct()

createRKeYMetaConstructExpression

public RKeYMetaConstructExpression createRKeYMetaConstructExpression()

createRKeYMetaConstructType

public RKeYMetaConstructType createRKeYMetaConstructType()

createContextStatementBlock

public ContextStatementBlock createContextStatementBlock(TypeSVWrapper typeRef,
                                                         MethodSignatureSVWrapper pm,
                                                         ExpressionSVWrapper var)

createContextStatementBlock

public ContextStatementBlock createContextStatementBlock(ExecCtxtSVWrapper ec)

createPassiveExpression

public PassiveExpression createPassiveExpression(Expression e)

Create a PassiveExpression.

createMergePointStatement

public MergePointStatement createMergePointStatement()

createMergePointStatement

public MergePointStatement createMergePointStatement(Expression e)

createPassiveExpression

public PassiveExpression createPassiveExpression()

Create a PassiveExpression.

throwSortInvalid

public static void throwSortInvalid(SchemaVariable sv,
                                    java.lang.String s)
                             throws ParseException

Throws:

ParseException

lookupSchemaVariableType

public boolean lookupSchemaVariableType(java.lang.String s,
                                        ProgramSVSort sort)

lookupSchemaVariable

public SchemaVariable lookupSchemaVariable(java.lang.String s)
                                    throws ParseException

Throws:

ParseException

getStatementSV

public StatementSVWrapper getStatementSV(java.lang.String s)
                                  throws ParseException

Throws:

ParseException

getExpressionSV

public ExpressionSVWrapper getExpressionSV(java.lang.String s)
                                    throws ParseException

Throws:

ParseException

getLabelSV

public LabelSVWrapper getLabelSV(java.lang.String s)
                          throws ParseException

Throws:

ParseException

getMethodSignatureSVWrapper

public MethodSignatureSVWrapper getMethodSignatureSVWrapper(java.lang.String s)
                                                     throws ParseException

Throws:

ParseException

getJumpLabelSV

public JumpLabelSVWrapper getJumpLabelSV(java.lang.String s)
                                  throws ParseException

Throws:

ParseException

getTypeSV

public TypeSVWrapper getTypeSV(java.lang.String s)
                        throws ParseException

Throws:

ParseException

getExecutionContextSV

public ExecCtxtSVWrapper getExecutionContextSV(java.lang.String s)
                                        throws ParseException

Throws:

ParseException

getProgramVariableSV

public ProgramVariableSVWrapper getProgramVariableSV(java.lang.String s)
                                              throws ParseException

Throws:

ParseException

getCatchSV

public CatchSVWrapper getCatchSV(java.lang.String s)
                          throws ParseException

Throws:

ParseException

attachComment

private static void attachComment(Comment c,
                                  ProgramElement pe)

postWork

private static void postWork(ProgramElement pe)

Perform post work on the created element. Creates parent links and assigns comments.

parseCompilationUnit

public CompilationUnit parseCompilationUnit(java.io.Reader in)
                                     throws java.io.IOException,
                                            ParserException

Parse a CompilationUnit from the given reader.

Specified by:

parseCompilationUnit in interface ProgramFactory

Overrides:

parseCompilationUnit in class JavaProgramFactory

Throws:

java.io.IOException

ParserException

parseTypeDeclaration

public TypeDeclaration parseTypeDeclaration(java.io.Reader in)
                                     throws java.io.IOException,
                                            ParserException

Parse a TypeDeclaration from the given reader.

Specified by:

parseTypeDeclaration in interface ProgramFactory

Overrides:

parseTypeDeclaration in class JavaProgramFactory

Throws:

java.io.IOException

ParserException

parseFieldDeclaration

public FieldDeclaration parseFieldDeclaration(java.io.Reader in)
                                       throws java.io.IOException,
                                              ParserException

Parse a FieldDeclaration from the given reader.

Specified by:

parseFieldDeclaration in interface ProgramFactory

Overrides:

parseFieldDeclaration in class JavaProgramFactory

Throws:

java.io.IOException

ParserException

parseMethodDeclaration

public MethodDeclaration parseMethodDeclaration(java.io.Reader in)
                                         throws java.io.IOException,
                                                ParserException

Parse a MethodDeclaration from the given reader.

Specified by:

parseMethodDeclaration in interface ProgramFactory

Overrides:

parseMethodDeclaration in class JavaProgramFactory

Throws:

java.io.IOException

ParserException

parseMemberDeclaration

public MemberDeclaration parseMemberDeclaration(java.io.Reader in)
                                         throws java.io.IOException,
                                                ParserException

Parse a MemberDeclaration from the given reader.

Specified by:

parseMemberDeclaration in interface ProgramFactory

Overrides:

parseMemberDeclaration in class JavaProgramFactory

Throws:

java.io.IOException

ParserException

parseParameterDeclaration

public ParameterDeclaration parseParameterDeclaration(java.io.Reader in)
                                               throws java.io.IOException,
                                                      ParserException

Parse a ParameterDeclaration from the given reader.

Specified by:

parseParameterDeclaration in interface ProgramFactory

Overrides:

parseParameterDeclaration in class JavaProgramFactory

Throws:

java.io.IOException

ParserException

parseConstructorDeclaration

public ConstructorDeclaration parseConstructorDeclaration(java.io.Reader in)
                                                   throws java.io.IOException,
                                                          ParserException

Parse a ConstructorDeclaration from the given reader.

Specified by:

parseConstructorDeclaration in interface ProgramFactory

Overrides:

parseConstructorDeclaration in class JavaProgramFactory

Throws:

java.io.IOException

ParserException

parseTypeReference

public TypeReference parseTypeReference(java.io.Reader in)
                                 throws java.io.IOException,
                                        ParserException

Parse a TypeReference from the given reader.

Specified by:

parseTypeReference in interface ProgramFactory

Overrides:

parseTypeReference in class JavaProgramFactory

Throws:

java.io.IOException

ParserException

parseExpression

public Expression parseExpression(java.io.Reader in)
                           throws java.io.IOException,
                                  ParserException

Parse an Expression from the given reader.

Specified by:

parseExpression in interface ProgramFactory

Overrides:

parseExpression in class JavaProgramFactory

Throws:

java.io.IOException

ParserException

parseStatements

public ASTList<Statement> parseStatements(java.io.Reader in)
                                   throws java.io.IOException,
                                          ParserException

Parse some Statements from the given reader.

Specified by:

parseStatements in interface ProgramFactory

Overrides:

parseStatements in class JavaProgramFactory

Throws:

java.io.IOException

ParserException

parseStatementBlock

public StatementBlock parseStatementBlock(java.io.Reader in)
                                   throws java.io.IOException,
                                          ParserException

Parse a StatementBlock from the given string.

Specified by:

parseStatementBlock in interface ProgramFactory

Overrides:

parseStatementBlock in class JavaProgramFactory

Throws:

java.io.IOException

ParserException

setSVNamespace

public void setSVNamespace(Namespace<SchemaVariable> ns)