public static class BlockContract.Variables extends Object
Modifier and Type | Field and Description |
---|---|
Map<Label,ProgramVariable> |
breakFlags |
Map<Label,ProgramVariable> |
continueFlags |
ProgramVariable |
exception |
Map<LocationVariable,LocationVariable> |
remembranceHeaps |
Map<LocationVariable,LocationVariable> |
remembranceLocalVariables |
ProgramVariable |
result |
ProgramVariable |
returnFlag |
ProgramVariable |
self |
private TermServices |
services |
Constructor and Description |
---|
Variables(ProgramVariable self,
Map<Label,ProgramVariable> breakFlags,
Map<Label,ProgramVariable> continueFlags,
ProgramVariable returnFlag,
ProgramVariable result,
ProgramVariable exception,
Map<LocationVariable,LocationVariable> remembranceHeaps,
Map<LocationVariable,LocationVariable> remembranceLocalVariables,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
Map<LocationVariable,LocationVariable> |
combineRemembranceVariables() |
static BlockContract.Variables |
create(StatementBlock block,
List<Label> labels,
IProgramMethod method,
Services services) |
boolean |
equals(Object obj) |
int |
hashCode() |
BlockContract.Terms |
termify(Term self) |
private Map<Label,Term> |
termifyFlags(Map<Label,ProgramVariable> flags) |
private Map<LocationVariable,Term> |
termifyRemembranceVariables(Map<LocationVariable,LocationVariable> remembranceVariables) |
private Term |
termifyVariable(ProgramVariable variable) |
private final TermServices services
public final ProgramVariable self
public final Map<Label,ProgramVariable> breakFlags
public final Map<Label,ProgramVariable> continueFlags
public final ProgramVariable returnFlag
public final ProgramVariable result
public final ProgramVariable exception
public final Map<LocationVariable,LocationVariable> remembranceHeaps
public final Map<LocationVariable,LocationVariable> remembranceLocalVariables
public Variables(ProgramVariable self, Map<Label,ProgramVariable> breakFlags, Map<Label,ProgramVariable> continueFlags, ProgramVariable returnFlag, ProgramVariable result, ProgramVariable exception, Map<LocationVariable,LocationVariable> remembranceHeaps, Map<LocationVariable,LocationVariable> remembranceLocalVariables, TermServices services)
public static BlockContract.Variables create(StatementBlock block, List<Label> labels, IProgramMethod method, Services services)
public Map<LocationVariable,LocationVariable> combineRemembranceVariables()
public BlockContract.Terms termify(Term self)
private Map<LocationVariable,Term> termifyRemembranceVariables(Map<LocationVariable,LocationVariable> remembranceVariables)
private Term termifyVariable(ProgramVariable variable)