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 |
private TermServices |
services
Services.
|
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. |
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
.private final TermServices services
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.private java.util.Map<Label,Term> termifyFlags(java.util.Map<Label,ProgramVariable> flags)
flags
- a map containing the variables to termify.private java.util.Map<LocationVariable,Term> termifyRemembranceVariables(java.util.Map<LocationVariable,LocationVariable> remembranceVariables)
remembranceVariables
- a map containing the variables to termify.private Term termifyVariable(ProgramVariable variable)
variable
- a variable.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
.