de.uka.ilkd.key.speclang

Class AuxiliaryContract.Variables

java.lang.Object

de.uka.ilkd.key.speclang.AuxiliaryContract.Variables

Enclosing interface:

AuxiliaryContract

public static class AuxiliaryContract.Variables
extends java.lang.Object

This class contains all new variables that are introduced during a AuxiliaryContract's instantiation.

Field Summary

Fields

Modifier and Type	Field and Description
java.util.Map<Label,ProgramVariable>	breakFlags Boolean flags that are set to true when the block terminates by a break label; statement with the specified label.
java.util.Map<Label,ProgramVariable>	continueFlags Boolean flags that are set to true when the block terminates by a continue label; statement with the specified label.
ProgramVariable	exception Exception variable to set when the block terminates by an uncaught throw statement.
java.util.Map<LocationVariable,LocationVariable>	outerRemembranceHeaps A map from every heap heap that is accessible inside the block to heap_Before_METHOD.
java.util.Map<LocationVariable,LocationVariable>	outerRemembranceVariables A map from every variable var that is accessible inside the block to var_Before_METHOD.
java.util.Map<LocationVariable,LocationVariable>	remembranceHeaps A map from every heap heap to heap_Before_BLOCK.
java.util.Map<LocationVariable,LocationVariable>	remembranceLocalVariables A map from every variable var that is assignable inside the block to var_Before_BLOCK.
ProgramVariable	result Result variable to set when the block terminates by a return statement.
ProgramVariable	returnFlag Boolean flag that is set to true when the block terminates by a return statement.
ProgramVariable	self self
private TermServices	services Services.

Constructor Summary

Constructors

Constructor and Description

Variables(ProgramVariable self, java.util.Map<Label,ProgramVariable> breakFlags, java.util.Map<Label,ProgramVariable> continueFlags, ProgramVariable returnFlag, ProgramVariable result, ProgramVariable exception, java.util.Map<LocationVariable,LocationVariable> remembranceHeaps, java.util.Map<LocationVariable,LocationVariable> remembranceLocalVariables, java.util.Map<LocationVariable,LocationVariable> outerRemembranceHeaps, java.util.Map<LocationVariable,LocationVariable> outerRemembranceVariables, TermServices services) You should use #create() instead of this constructor.

Method Summary

Modifier and Type	Method and Description
java.util.Map<LocationVariable,LocationVariable>	combineOuterRemembranceVariables()
java.util.Map<LocationVariable,LocationVariable>	combineRemembranceVariables()
static AuxiliaryContract.Variables	create(LoopStatement loop, java.util.List<Label> labels, IProgramMethod method, Services services) Creates a new instance.
static AuxiliaryContract.Variables	create(StatementBlock block, java.util.List<Label> labels, IProgramMethod method, Services services) Creates a new instance.
boolean	equals(java.lang.Object obj)
int	hashCode()
AuxiliaryContract.Terms	termify(Term self)
private java.util.Map<Label,Term>	termifyFlags(java.util.Map<Label,ProgramVariable> flags)
private java.util.Map<LocationVariable,Term>	termifyRemembranceVariables(java.util.Map<LocationVariable,LocationVariable> remembranceVariables)
private Term	termifyVariable(ProgramVariable variable)
Contract.OriginalVariables	toOrigVars()

Methods inherited from class java.lang.Object

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

Field Detail

self

public final ProgramVariable self

self

breakFlags

public final java.util.Map<Label,ProgramVariable> breakFlags

Boolean flags that are set to true when the block terminates by a break label; statement with the specified label.

continueFlags

public final java.util.Map<Label,ProgramVariable> continueFlags

Boolean flags that are set to true when the block terminates by a continue label; statement with the specified label.

returnFlag

public final ProgramVariable returnFlag

Boolean flag that is set to true when the block terminates by a return statement.

result

public final ProgramVariable result

Result variable to set when the block terminates by a return statement.

exception

public final ProgramVariable exception

Exception variable to set when the block terminates by an uncaught throw statement.

remembranceHeaps

public final java.util.Map<LocationVariable,LocationVariable> remembranceHeaps

A map from every heap heap to heap_Before_BLOCK.

remembranceLocalVariables

public final java.util.Map<LocationVariable,LocationVariable> remembranceLocalVariables

A map from every variable var that is assignable inside the block to var_Before_BLOCK.

outerRemembranceHeaps

public final java.util.Map<LocationVariable,LocationVariable> outerRemembranceHeaps

A map from every heap heap that is accessible inside the block to heap_Before_METHOD.

outerRemembranceVariables

public final java.util.Map<LocationVariable,LocationVariable> outerRemembranceVariables

A map from every variable var that is accessible inside the block to var_Before_METHOD.

services

private final TermServices services

Services.

Constructor Detail

Variables

public Variables(ProgramVariable self,
                 java.util.Map<Label,ProgramVariable> breakFlags,
                 java.util.Map<Label,ProgramVariable> continueFlags,
                 ProgramVariable returnFlag,
                 ProgramVariable result,
                 ProgramVariable exception,
                 java.util.Map<LocationVariable,LocationVariable> remembranceHeaps,
                 java.util.Map<LocationVariable,LocationVariable> remembranceLocalVariables,
                 java.util.Map<LocationVariable,LocationVariable> outerRemembranceHeaps,
                 java.util.Map<LocationVariable,LocationVariable> outerRemembranceVariables,
                 TermServices services)

You should use #create() instead of this constructor.

Parameters:

self - self

breakFlags - boolean flags that are set to true when the block terminates by a break label; statement with the specified label.

continueFlags - boolean flags that are set to true when the block terminates by a continue label; statement with the specified label.

returnFlag - boolean flag that is set to true when the block terminates by a return statement.

result - result variable to set when the block terminates by a return statement.

exception - exception variable to set when the block terminates by an uncaught throw statement.

remembranceHeaps - a map from every heap heap to heap_Before_BLOCK.

remembranceLocalVariables - a map from every variable var that is assignable inside the block to var_Before_BLOCK.

outerRemembranceHeaps - a map from every heap heap that is accessible inside the block to heap_Before_METHOD.

outerRemembranceVariables - a map from every variable var that is accessible inside the block to var_Before_METHOD.

services - services.

Method Detail

create

public static AuxiliaryContract.Variables create(StatementBlock block,
                                                 java.util.List<Label> labels,
                                                 IProgramMethod method,
                                                 Services services)

Creates a new instance.

Parameters:

block - the block for which this instance is created.

labels - all labels that belong to the block.

method - the method containing the block.

services - services.

Returns:

a new instance.

create

public static AuxiliaryContract.Variables create(LoopStatement loop,
                                                 java.util.List<Label> labels,
                                                 IProgramMethod method,
                                                 Services services)

Creates a new instance.

Parameters:

loop - the loop for which this instance is created.

labels - all labels that belong to the block.

method - the method containing the block.

services - services.

Returns:

a new instance.

combineRemembranceVariables

public java.util.Map<LocationVariable,LocationVariable> combineRemembranceVariables()

Returns:

the union of remembranceHeaps and remembranceLocalVariables.

combineOuterRemembranceVariables

public java.util.Map<LocationVariable,LocationVariable> combineOuterRemembranceVariables()

Returns:

the union of outerRemembranceHeaps and outerRemembranceVariables.

termify

public AuxiliaryContract.Terms termify(Term self)

Parameters:

self - the self term to use.

Returns:

a Terms object containing these variables in term form.

termifyFlags

private java.util.Map<Label,Term> termifyFlags(java.util.Map<Label,ProgramVariable> flags)

Parameters:

flags - a map containing the variables to termify.

Returns:

a map with all the same keys with termified values.

termifyRemembranceVariables

private java.util.Map<LocationVariable,Term> termifyRemembranceVariables(java.util.Map<LocationVariable,LocationVariable> remembranceVariables)

Parameters:

remembranceVariables - a map containing the variables to termify.

Returns:

a map with all the same keys with termified values.

termifyVariable

private Term termifyVariable(ProgramVariable variable)

Parameters:

variable - a variable.

Returns:

a term containing the specified variable.

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

equals

public boolean equals(java.lang.Object obj)

Overrides:

equals in class java.lang.Object

toOrigVars

public Contract.OriginalVariables toOrigVars()

Returns:

a conversion of this object to OriginalVariables.