class BasicSnippetData extends Object
Modifier and Type | Class and Description |
---|---|
(package private) static class |
BasicSnippetData.Key
Keys to access the unified contract content.
|
Modifier and Type | Field and Description |
---|---|
private EnumMap<BasicSnippetData.Key,Object> |
contractContents
Unified contract content.
|
(package private) boolean |
hasMby
Tells whether the contract contains a measured_by clause.
|
(package private) StateVars |
origVars
Variables originally used during parsing.
|
(package private) Services |
services |
(package private) TermBuilder |
tb
TermBuilder used by the FactoryMethods.
|
Constructor and Description |
---|
BasicSnippetData(BlockContract contract,
ExecutionContext context,
Services services) |
BasicSnippetData(FunctionalOperationContract contract,
Services services) |
BasicSnippetData(InformationFlowContract contract,
Services services) |
BasicSnippetData(LoopInvariant invariant,
ExecutionContext context,
Term guardTerm,
Services services) |
Modifier and Type | Method and Description |
---|---|
(package private) Object |
get(BasicSnippetData.Key contentKey) |
private ImmutableList<Term> |
toTermList(ImmutableSet<ProgramVariable> vars) |
final boolean hasMby
final StateVars origVars
final TermBuilder tb
final Services services
private final EnumMap<BasicSnippetData.Key,Object> contractContents
BasicSnippetData(FunctionalOperationContract contract, Services services)
BasicSnippetData(LoopInvariant invariant, ExecutionContext context, Term guardTerm, Services services)
BasicSnippetData(InformationFlowContract contract, Services services)
BasicSnippetData(BlockContract contract, ExecutionContext context, Services services)
private ImmutableList<Term> toTermList(ImmutableSet<ProgramVariable> vars)
Object get(BasicSnippetData.Key contentKey)