de.uka.ilkd.key.informationflow.po.snippet

Class BasicSnippetData

java.lang.Object

de.uka.ilkd.key.informationflow.po.snippet.BasicSnippetData

class BasicSnippetData
extends java.lang.Object

Immutable class.

Author:

christoph

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) static class	BasicSnippetData.Key Keys to access the unified contract content.

Field Summary

Fields

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 Summary

Constructors

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)

Method Summary

Modifier and Type	Method and Description
(package private) java.lang.Object	get(BasicSnippetData.Key contentKey)
private ImmutableList<Term>	toTermList(ImmutableSet<ProgramVariable> vars)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

hasMby

final boolean hasMby

Tells whether the contract contains a measured_by clause.

origVars

final StateVars origVars

Variables originally used during parsing.

tb

final TermBuilder tb

TermBuilder used by the FactoryMethods.

services

final Services services

contractContents

private final java.util.EnumMap<BasicSnippetData.Key,java.lang.Object> contractContents

Unified contract content.

Constructor Detail

BasicSnippetData

BasicSnippetData(FunctionalOperationContract contract,
                 Services services)

BasicSnippetData

BasicSnippetData(LoopSpecification invariant,
                 ExecutionContext context,
                 Term guardTerm,
                 Services services)

BasicSnippetData

BasicSnippetData(InformationFlowContract contract,
                 Services services)

BasicSnippetData

BasicSnippetData(BlockContract contract,
                 ExecutionContext context,
                 Services services)

Method Detail

toTermList

private ImmutableList<Term> toTermList(ImmutableSet<ProgramVariable> vars)

get

java.lang.Object get(BasicSnippetData.Key contentKey)