public static class AuxiliaryContract.Terms
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
java.util.Map<Label,Term> |
breakFlags |
java.util.Map<Label,Term> |
continueFlags |
Term |
exception |
java.util.Map<LocationVariable,Term> |
outerRemembranceHeaps |
java.util.Map<LocationVariable,Term> |
outerRemembranceVariables |
java.util.Map<LocationVariable,Term> |
remembranceHeaps |
java.util.Map<LocationVariable,Term> |
remembranceLocalVariables |
Term |
result |
Term |
returnFlag |
Term |
self |
Constructor and Description |
---|
Terms(AuxiliaryContract.Variables variables,
TermBuilder tb) |
Terms(Term self,
java.util.Map<Label,Term> breakFlags,
java.util.Map<Label,Term> continueFlags,
Term returnFlag,
Term result,
Term exception,
java.util.Map<LocationVariable,Term> remembranceHeaps,
java.util.Map<LocationVariable,Term> remembranceLocalVariables,
java.util.Map<LocationVariable,Term> outerRemembranceHeaps,
java.util.Map<LocationVariable,Term> outerRemembranceVariables)
Creates a new instance.
|
Modifier and Type | Method and Description |
---|---|
private static java.util.Map<Label,Term> |
convertFlagMap(java.util.Map<Label,ProgramVariable> map,
TermBuilder tb) |
private static java.util.Map<LocationVariable,Term> |
convertHeapMap(java.util.Map<LocationVariable,LocationVariable> map,
TermBuilder tb) |
public final Term self
AuxiliaryContract.Variables.self
public final java.util.Map<Label,Term> breakFlags
AuxiliaryContract.Variables.breakFlags
public final Term returnFlag
AuxiliaryContract.Variables.returnFlag
public final Term result
AuxiliaryContract.Variables.result
public final Term exception
AuxiliaryContract.Variables.exception
public final java.util.Map<LocationVariable,Term> remembranceHeaps
public final java.util.Map<LocationVariable,Term> remembranceLocalVariables
public final java.util.Map<LocationVariable,Term> outerRemembranceHeaps
public final java.util.Map<LocationVariable,Term> outerRemembranceVariables
public Terms(Term self, java.util.Map<Label,Term> breakFlags, java.util.Map<Label,Term> continueFlags, Term returnFlag, Term result, Term exception, java.util.Map<LocationVariable,Term> remembranceHeaps, java.util.Map<LocationVariable,Term> remembranceLocalVariables, java.util.Map<LocationVariable,Term> outerRemembranceHeaps, java.util.Map<LocationVariable,Term> outerRemembranceVariables)
AuxiliaryContract.Variables.termify(Term)
or
Terms#Terms(Variables, TermBuilder)
should be used instead of this.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
.public Terms(AuxiliaryContract.Variables variables, TermBuilder tb)
variables
- the variables to termify.tb
- the term builder to use.private static java.util.Map<LocationVariable,Term> convertHeapMap(java.util.Map<LocationVariable,LocationVariable> map, TermBuilder tb)
map
- a map containing heaps as values.tb
- a term builder.private static java.util.Map<Label,Term> convertFlagMap(java.util.Map<Label,ProgramVariable> map, TermBuilder tb)
map
- a map containing boolean variables as values.tb
- a term builder.