class BasicSnippetData
extends java.lang.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 java.util.EnumMap<BasicSnippetData.Key,java.lang.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(LoopSpecification invariant,
ExecutionContext context,
Term guardTerm,
Services services) |
Modifier and Type | Method and Description |
---|---|
(package private) java.lang.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 java.util.EnumMap<BasicSnippetData.Key,java.lang.Object> contractContents
BasicSnippetData(FunctionalOperationContract contract, Services services)
BasicSnippetData(LoopSpecification 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)
java.lang.Object get(BasicSnippetData.Key contentKey)