de.uka.ilkd.key.java.recoderext

Class ProofJavaProgramFactory

java.lang.Object

recoder.java.JavaProgramFactory

de.uka.ilkd.key.java.recoderext.ProofJavaProgramFactory

All Implemented Interfaces:

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

public class ProofJavaProgramFactory
extends JavaProgramFactory

Field Summary

Fields

Modifier and Type	Field and Description
private static ProofJavaParser	parser For internal reuse and synchronization.
private static ProofJavaProgramFactory	theFactory The singleton instance of the program factory.
private static SourceElement.Position	ZERO_POSITION

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method and Description
private static void	attachComment(Comment c, ProgramElement pe)
Statement	createCatchAllStatement(VariableReference param, StatementBlock body) Create a CatchAllStatement.
Comment	createComment(java.lang.String text) Create a comment.
Comment	createComment(java.lang.String text, boolean prefixed) Create a comment.
Identifier	createIdentifier(java.lang.String text)
ImplicitIdentifier	createImplicitIdentifier(java.lang.String text) Create an ImplicitIdentifier.
LoopScopeBlock	createLoopScopeBlock()
MergePointStatement	createMergePointStatement()
MergePointStatement	createMergePointStatement(Expression expr)
MethodBodyStatement	createMethodBodyStatement(TypeReference bodySource, Expression resVar, MethodReference methRef) Create a MethodBodyStatement.
MethodCallStatement	createMethodCallStatement(Expression resVar, ExecutionContext ec, StatementBlock block) Create a MethodCallStatement.
MethodSignature	createMethodSignature(Identifier methodName, ASTList<TypeReference> paramTypes) Create a MethodSignature.
ObjectTypeIdentifier	createObjectTypeIdentifier(java.lang.String text)
PassiveExpression	createPassiveExpression() Create a PassiveExpression.
PassiveExpression	createPassiveExpression(Expression e) Create a PassiveExpression.
static JavaProgramFactory	getInstance() Returns the single instance of this class.
void	initialize(ServiceConfiguration cfg)
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.

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, 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, 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

theFactory

private static ProofJavaProgramFactory theFactory

The singleton instance of the program factory.

parser

private static final ProofJavaParser parser

For internal reuse and synchronization.

ZERO_POSITION

private static final SourceElement.Position ZERO_POSITION

Constructor Detail

ProofJavaProgramFactory

protected ProofJavaProgramFactory()

Protected constructor - use getInstance() instead.

Method Detail

getInstance

public static JavaProgramFactory getInstance()

Returns the single instance of this class.

initialize

public void initialize(ServiceConfiguration cfg)

Specified by:

initialize in interface Service

Overrides:

initialize in class JavaProgramFactory

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

createPassiveExpression

public PassiveExpression createPassiveExpression(Expression e)

Create a PassiveExpression.

createPassiveExpression

public PassiveExpression createPassiveExpression()

Create a PassiveExpression.

createMethodSignature

public MethodSignature createMethodSignature(Identifier methodName,
                                             ASTList<TypeReference> paramTypes)

Create a MethodSignature.

createMethodCallStatement

public MethodCallStatement createMethodCallStatement(Expression resVar,
                                                     ExecutionContext ec,
                                                     StatementBlock block)

Create a MethodCallStatement.

createLoopScopeBlock

public LoopScopeBlock createLoopScopeBlock()

createMergePointStatement

public MergePointStatement createMergePointStatement()

createMergePointStatement

public MergePointStatement createMergePointStatement(Expression expr)

createMethodBodyStatement

public MethodBodyStatement createMethodBodyStatement(TypeReference bodySource,
                                                     Expression resVar,
                                                     MethodReference methRef)

Create a MethodBodyStatement.

createCatchAllStatement

public Statement createCatchAllStatement(VariableReference param,
                                         StatementBlock body)

Create a CatchAllStatement.

createComment

public Comment createComment(java.lang.String text)

Create a comment.

Specified by:

createComment in interface ProgramFactory

Overrides:

createComment in class JavaProgramFactory

Parameters:

text - comment text

createComment

public Comment createComment(java.lang.String text,
                             boolean prefixed)

Create a comment.

Specified by:

createComment in interface ProgramFactory

Overrides:

createComment in class JavaProgramFactory

Parameters:

text - comment text

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

createObjectTypeIdentifier

public ObjectTypeIdentifier createObjectTypeIdentifier(java.lang.String text)