public class ProofJavaProgramFactory extends JavaProgramFactory
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 |
Modifier | Constructor and Description |
---|---|
protected |
ProofJavaProgramFactory()
Protected constructor - use
getInstance() instead. |
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
private static ProofJavaProgramFactory theFactory
private static final ProofJavaParser parser
private static final SourceElement.Position ZERO_POSITION
protected ProofJavaProgramFactory()
getInstance()
instead.public static JavaProgramFactory getInstance()
public void initialize(ServiceConfiguration cfg)
initialize
in interface Service
initialize
in class JavaProgramFactory
private static void attachComment(Comment c, ProgramElement pe)
private static void postWork(ProgramElement pe)
public CompilationUnit parseCompilationUnit(java.io.Reader in) throws java.io.IOException, ParserException
CompilationUnit
from the given reader.parseCompilationUnit
in interface ProgramFactory
parseCompilationUnit
in class JavaProgramFactory
java.io.IOException
ParserException
public TypeDeclaration parseTypeDeclaration(java.io.Reader in) throws java.io.IOException, ParserException
TypeDeclaration
from the given reader.parseTypeDeclaration
in interface ProgramFactory
parseTypeDeclaration
in class JavaProgramFactory
java.io.IOException
ParserException
public FieldDeclaration parseFieldDeclaration(java.io.Reader in) throws java.io.IOException, ParserException
FieldDeclaration
from the given reader.parseFieldDeclaration
in interface ProgramFactory
parseFieldDeclaration
in class JavaProgramFactory
java.io.IOException
ParserException
public MethodDeclaration parseMethodDeclaration(java.io.Reader in) throws java.io.IOException, ParserException
MethodDeclaration
from the given reader.parseMethodDeclaration
in interface ProgramFactory
parseMethodDeclaration
in class JavaProgramFactory
java.io.IOException
ParserException
public MemberDeclaration parseMemberDeclaration(java.io.Reader in) throws java.io.IOException, ParserException
MemberDeclaration
from the given reader.parseMemberDeclaration
in interface ProgramFactory
parseMemberDeclaration
in class JavaProgramFactory
java.io.IOException
ParserException
public ParameterDeclaration parseParameterDeclaration(java.io.Reader in) throws java.io.IOException, ParserException
ParameterDeclaration
from the given reader.parseParameterDeclaration
in interface ProgramFactory
parseParameterDeclaration
in class JavaProgramFactory
java.io.IOException
ParserException
public ConstructorDeclaration parseConstructorDeclaration(java.io.Reader in) throws java.io.IOException, ParserException
ConstructorDeclaration
from the given reader.parseConstructorDeclaration
in interface ProgramFactory
parseConstructorDeclaration
in class JavaProgramFactory
java.io.IOException
ParserException
public TypeReference parseTypeReference(java.io.Reader in) throws java.io.IOException, ParserException
TypeReference
from the given reader.parseTypeReference
in interface ProgramFactory
parseTypeReference
in class JavaProgramFactory
java.io.IOException
ParserException
public Expression parseExpression(java.io.Reader in) throws java.io.IOException, ParserException
Expression
from the given reader.parseExpression
in interface ProgramFactory
parseExpression
in class JavaProgramFactory
java.io.IOException
ParserException
public ASTList<Statement> parseStatements(java.io.Reader in) throws java.io.IOException, ParserException
Statement
s from the given reader.parseStatements
in interface ProgramFactory
parseStatements
in class JavaProgramFactory
java.io.IOException
ParserException
public StatementBlock parseStatementBlock(java.io.Reader in) throws java.io.IOException, ParserException
StatementBlock
from the given string.parseStatementBlock
in interface ProgramFactory
parseStatementBlock
in class JavaProgramFactory
java.io.IOException
ParserException
public PassiveExpression createPassiveExpression(Expression e)
PassiveExpression
.public PassiveExpression createPassiveExpression()
PassiveExpression
.public MethodSignature createMethodSignature(Identifier methodName, ASTList<TypeReference> paramTypes)
MethodSignature
.public MethodCallStatement createMethodCallStatement(Expression resVar, ExecutionContext ec, StatementBlock block)
MethodCallStatement
.public LoopScopeBlock createLoopScopeBlock()
public MergePointStatement createMergePointStatement()
public MergePointStatement createMergePointStatement(Expression expr)
public MethodBodyStatement createMethodBodyStatement(TypeReference bodySource, Expression resVar, MethodReference methRef)
MethodBodyStatement
.public Statement createCatchAllStatement(VariableReference param, StatementBlock body)
CatchAllStatement
.public Comment createComment(java.lang.String text)
createComment
in interface ProgramFactory
createComment
in class JavaProgramFactory
text
- comment textpublic Comment createComment(java.lang.String text, boolean prefixed)
createComment
in interface ProgramFactory
createComment
in class JavaProgramFactory
text
- comment textpublic ImplicitIdentifier createImplicitIdentifier(java.lang.String text)
ImplicitIdentifier
.public Identifier createIdentifier(java.lang.String text)
createIdentifier
in interface ProgramFactory
createIdentifier
in class JavaProgramFactory
public ObjectTypeIdentifier createObjectTypeIdentifier(java.lang.String text)