de.uka.ilkd.key.rule

Class AuxiliaryContractBuilders.ValidityProgramConstructor

java.lang.Object

de.uka.ilkd.key.rule.AuxiliaryContractBuilders.ValidityProgramConstructor

Enclosing class:

AuxiliaryContractBuilders

public static final class AuxiliaryContractBuilders.ValidityProgramConstructor
extends java.lang.Object

This class is used to construct block' from block (see Wacker 2012, 3.3).

See Also:

construct()

Field Summary

Fields

Modifier and Type	Field and Description
private AuxiliaryContract.Variables	alreadyDeclared The subset of variables that have already been declared.
private StatementBlock	block
private ProgramVariable	exceptionParameter The exception variable.
private java.lang.Iterable<Label>	labels
private Services	services Services.
private java.util.List<Statement>	statements Statements in the program.
private AuxiliaryContract.Variables	variables

Constructor Summary

Constructors

Constructor and Description
ValidityProgramConstructor(java.lang.Iterable<Label> labels, StatementBlock block, AuxiliaryContract.Variables variables, ProgramVariable exceptionParameter, Services services)
ValidityProgramConstructor(java.lang.Iterable<Label> labels, StatementBlock block, AuxiliaryContract.Variables variables, ProgramVariable exceptionParameter, Services services, AuxiliaryContract.Variables alreadyDeclared)

Method Summary

Modifier and Type	Method and Description
StatementBlock	construct()
private void	declareExceptionNull() Adds a statement that declares the exception variable if necessary and set its value to null.
private void	declareFlagsFalse() Adds statements to declare all flags that have not yet been declared and set their values to false.
private void	declareResultDefault() Adds a statement that declares the result variable if necessary and set its value to the default for its type.
private void	executeBlockSafely() Makes sure that the block never terminates abruptly.
private Statement	label(StatementBlock block, java.lang.Iterable<Label> labels)
private boolean	occursReturnAndIsReturnTypeNotVoid()
private StatementBlock	replaceOuterBreaksContinuesAndReturns(StatementBlock block, Label breakOutLabel)
private Statement	wrapInTryCatch(Statement labeledBlock, ProgramVariable exceptionParameter)

Methods inherited from class java.lang.Object

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

Field Detail

labels

private final java.lang.Iterable<Label> labels

See Also:

AuxiliaryContract.getLabels()

block

private final StatementBlock block

See Also:

AuxiliaryContract.getBlock()

variables

private final AuxiliaryContract.Variables variables

See Also:

AuxiliaryContract.getVariables()

alreadyDeclared

private final AuxiliaryContract.Variables alreadyDeclared

The subset of variables that have already been declared.

services

private final Services services

Services.

statements

private final java.util.List<Statement> statements

Statements in the program.

exceptionParameter

private final ProgramVariable exceptionParameter

The exception variable.

Constructor Detail

ValidityProgramConstructor

public ValidityProgramConstructor(java.lang.Iterable<Label> labels,
                                  StatementBlock block,
                                  AuxiliaryContract.Variables variables,
                                  ProgramVariable exceptionParameter,
                                  Services services)

Parameters:

labels - all labels belonging to the block.

block - the block.

variables - the variables.

exceptionParameter - the exception variable.

services - services.

ValidityProgramConstructor

public ValidityProgramConstructor(java.lang.Iterable<Label> labels,
                                  StatementBlock block,
                                  AuxiliaryContract.Variables variables,
                                  ProgramVariable exceptionParameter,
                                  Services services,
                                  AuxiliaryContract.Variables alreadyDeclared)

Parameters:

labels - all labels belonging to the block.

block - the block.

variables - the variables.

exceptionParameter - the exception variable.

services - services.

alreadyDeclared - the subset of variables that have already been declared.

Method Detail

construct

public StatementBlock construct()

Returns:

block'

declareFlagsFalse

private void declareFlagsFalse()

Adds statements to declare all flags that have not yet been declared and set their values to false.

declareResultDefault

private void declareResultDefault()

Adds a statement that declares the result variable if necessary and set its value to the default for its type.

occursReturnAndIsReturnTypeNotVoid

private boolean occursReturnAndIsReturnTypeNotVoid()

Returns:

true iff there is a result.

declareExceptionNull

private void declareExceptionNull()

Adds a statement that declares the exception variable if necessary and set its value to null.

executeBlockSafely

private void executeBlockSafely()

Makes sure that the block never terminates abruptly.

label

private Statement label(StatementBlock block,
                        java.lang.Iterable<Label> labels)

Parameters:

block - a block.

labels - labels that should be added to the block.

Returns:

a labeled statement.

replaceOuterBreaksContinuesAndReturns

private StatementBlock replaceOuterBreaksContinuesAndReturns(StatementBlock block,
                                                             Label breakOutLabel)

Parameters:

block - a block.

breakOutLabel - a label belonging to the block.

Returns:

the block with all outer breaks, continues, and returns replaced.

See Also:

OuterBreakContinueAndReturnReplacer

wrapInTryCatch

private Statement wrapInTryCatch(Statement labeledBlock,
                                 ProgramVariable exceptionParameter)

Parameters:

labeledBlock - the labeled block.

exceptionParameter - the exception variable.

Returns:

wraps the labeled block in a try-catch structure