public static class AuxiliaryContract.Variables
extends java.lang.Object
AuxiliaryContract
's instantiation.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 |
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. |
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) |
Contract.OriginalVariables |
toOrigVars() |
public final ProgramVariable self
self
public final java.util.Map<Label,ProgramVariable> breakFlags
true
when the block terminates by a
break label;
statement with the specified label.public final java.util.Map<Label,ProgramVariable> continueFlags
true
when the block terminates by a
continue label;
statement with the specified label.public final ProgramVariable returnFlag
true
when the block terminates by a return
statement.public final ProgramVariable result
return
statement.public final ProgramVariable exception
throw
statement.public final java.util.Map<LocationVariable,LocationVariable> remembranceHeaps
heap
to heap_Before_BLOCK
.public final java.util.Map<LocationVariable,LocationVariable> remembranceLocalVariables
var
that is assignable inside the block to
var_Before_BLOCK
.public final java.util.Map<LocationVariable,LocationVariable> outerRemembranceHeaps
heap
that is accessible inside the block to
heap_Before_METHOD
.public final java.util.Map<LocationVariable,LocationVariable> outerRemembranceVariables
var
that is accessible inside the block to
var_Before_METHOD
.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)
#create()
instead of this constructor.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.public static AuxiliaryContract.Variables create(StatementBlock block, java.util.List<Label> labels, IProgramMethod method, Services services)
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.public static AuxiliaryContract.Variables create(LoopStatement loop, java.util.List<Label> labels, IProgramMethod method, Services services)
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.public java.util.Map<LocationVariable,LocationVariable> combineRemembranceVariables()
remembranceHeaps
and remembranceLocalVariables
.public java.util.Map<LocationVariable,LocationVariable> combineOuterRemembranceVariables()
outerRemembranceHeaps
and
outerRemembranceVariables
.public AuxiliaryContract.Terms termify(Term self)
self
- the self
term to use.Terms
object containing these variables in term form.public int hashCode()
hashCode
in class java.lang.Object
public boolean equals(java.lang.Object obj)
equals
in class java.lang.Object
public Contract.OriginalVariables toOrigVars()
OriginalVariables
.Copyright © 2003-2019 The KeY-Project.