public class ProofJavaProgramFactory extends JavaProgramFactory
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
protected ProofJavaProgramFactory()
getInstance()
instead.public static JavaProgramFactory getInstance()
public void initialize(ServiceConfiguration cfg)
initialize
in interface Service
initialize
in class JavaProgramFactory
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)
public Exec createExec()
public Exec createExec(StatementBlock body)
public Exec createExec(StatementBlock body, ASTList<Branch> branches)
public Ccatch createCcatch()
public Ccatch createCcatch(ParameterDeclaration e, StatementBlock body)
public CcatchReturnParameterDeclaration createCcatchReturnParameterDeclaration()
public CcatchBreakParameterDeclaration createCcatchBreakParameterDeclaration()
public CcatchBreakLabelParameterDeclaration createCcatchBreakLabelParameterDeclaration(Identifier label)
public CcatchBreakWildcardParameterDeclaration createCcatchBreakWildcardParameterDeclaration()
public CcatchContinueParameterDeclaration createCcatchContinueParameterDeclaration()
public CcatchContinueLabelParameterDeclaration createCcatchContinueLabelParameterDeclaration(Identifier label)
public CcatchContinueWildcardParameterDeclaration createCcatchContinueWildcardParameterDeclaration()
public CcatchNonstandardParameterDeclaration createCcatchReturnValParameterDeclaration(ParameterDeclaration e)
Copyright © 2003-2019 The KeY-Project.