de.uka.ilkd.key.informationflow.rule.tacletbuilder

Class AbstractInfFlowTacletBuilder

java.lang.Object

de.uka.ilkd.key.logic.TermBuilder

de.uka.ilkd.key.informationflow.rule.tacletbuilder.AbstractInfFlowTacletBuilder

Direct Known Subclasses:

AbstractInfFlowContractAppTacletBuilder, AbstractInfFlowUnfoldTacletBuilder

abstract class AbstractInfFlowTacletBuilder
extends TermBuilder

Builds the rule which inserts information flow contract applications.

Author:

christoph

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) class	AbstractInfFlowTacletBuilder.QuantifiableVariableVisitor

Field Summary

Fields

Modifier and Type	Field and Description
private static Name	EQUAL_LOCS Constant name for eqAtLocs function.
private static Name	EQUAL_LOCS_POST Constant name for eqAtLocsPost function.

Fields inherited from class de.uka.ilkd.key.logic.TermBuilder

services, WD_ANY, WD_FORMULA

Constructor Summary

Constructors

Constructor and Description
AbstractInfFlowTacletBuilder(Services services)

Method Summary

Modifier and Type	Method and Description
(package private) void	addVarconds(RewriteTacletBuilder<? extends RewriteTaclet> tacletBuilder, java.lang.Iterable<SchemaVariable> quantifiableSVs)
(package private) java.util.Map<QuantifiableVariable,SchemaVariable>	collectQuantifiableVariables(Term replaceWithTerm, Services services)
(package private) ImmutableList<Term>	createTermSV(ImmutableList<Term> ts, java.lang.String schemaPrefix, Services services)
(package private) Term	createTermSV(Term t, java.lang.String schemaPrefix, Services services)
(package private) SchemaVariable	createVariableSV(QuantifiableVariable v, java.lang.String schemaPrefix, Services services)
Term	eqAtLocs(Services services, Term heap1, Term locset1, Term heap2, Term locset2) Get eqAtLocs function as a term.
Term	eqAtLocsPost(Services services, Term heap1Pre, Term heap1Post, Term locset1, Term heap2Pre, Term heap2Post, Term locset2) Get eqAtLocsPost function as a term.

Methods inherited from class de.uka.ilkd.key.logic.TermBuilder

acc, add, addLabel, addLabel, all, all, allClose, allFields, allLocs, allObjects, and, and, and, andPreserveLabels, andPreserveLabels, andSC, andSC, andSC, anon, anonUpd, apply, apply, apply, applyElementary, applyElementary, applyElementary, applyParallel, applyParallel, applyParallel, applySequential, applySequential, applyUpdatePairsSequential, arr, arrayRange, arrayStore, box, bprod, bsum, cast, classErroneous, classInitializationInProgress, classInitialized, classPrepared, convertToBoolean, convertToFormula, create, created, created, createdInHeap, createdLocs, cTerm, deepNonNull, dia, disjoint, dot, dot, dot, dotArr, dotLength, elementary, elementary, elementOf, empty, equals, ex, ex, exactInstance, excVar, excVar, FALSE, ff, fieldStore, forallHeaps, frame, frameStrictlyEmpty, freshLocs, func, func, func, func, func, func, geq, getBaseHeap, getMeasuredByEmpty, getSorts, goBelowUpdates, goBelowUpdates2, gt, heapAtPreVar, heapAtPreVar, ife, ifEx, ifEx, imp, imp, impPreserveLabels, inByte, inChar, index, indexOf, infiniteUnion, infiniteUnion, inInt, initialized, inLong, inShort, instance, intersect, intersect, intersect, inv, inv, label, label, leq, lt, max, measuredBy, measuredByCheck, measuredByEmpty, min, newName, newName, newName, not, notPreserveLabels, NULL, one, open, or, or, or, orPreserveLabels, orPreserveLabels, orSC, orSC, orSC, pair, parallel, parallel, parallel, parallel, parallel, paramVars, paramVars, parseTerm, parseTerm, permissionsFor, permissionsFor, prec, prod, prog, prog, reach, reachableValue, reachableValue, reachableValue, resultVar, resultVar, select, select, selfVar, selfVar, selfVar, selfVar, seq, seq, seqConcat, seqDef, seqEmpty, seqGet, seqLen, seqReverse, seqSingleton, seqSub, sequential, sequential, sequential, setComprehension, setComprehension, setMinus, shortBaseName, shortcut, singleton, skip, staticDot, staticDot, staticFieldStore, staticInv, staticInv, store, strictlyNothing, subset, subst, subst, sum, tf, TRUE, tt, union, union, union, unionToSet, unlabel, unlabelRecursive, values, var, var, var, var, var, var, wd, wd, wd, wellFormed, wellFormed, zero, zTerm, zTerm

Methods inherited from class java.lang.Object

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

Field Detail

EQUAL_LOCS

private static final Name EQUAL_LOCS

Constant name for eqAtLocs function.

EQUAL_LOCS_POST

private static final Name EQUAL_LOCS_POST

Constant name for eqAtLocsPost function.

Constructor Detail

AbstractInfFlowTacletBuilder

public AbstractInfFlowTacletBuilder(Services services)

Method Detail

createTermSV

ImmutableList<Term> createTermSV(ImmutableList<Term> ts,
                                 java.lang.String schemaPrefix,
                                 Services services)

createTermSV

Term createTermSV(Term t,
                  java.lang.String schemaPrefix,
                  Services services)

createVariableSV

SchemaVariable createVariableSV(QuantifiableVariable v,
                                java.lang.String schemaPrefix,
                                Services services)

addVarconds

void addVarconds(RewriteTacletBuilder<? extends RewriteTaclet> tacletBuilder,
                 java.lang.Iterable<SchemaVariable> quantifiableSVs)
          throws java.lang.IllegalArgumentException

Throws:

java.lang.IllegalArgumentException

collectQuantifiableVariables

java.util.Map<QuantifiableVariable,SchemaVariable> collectQuantifiableVariables(Term replaceWithTerm,
                                                                                Services services)

eqAtLocs

public Term eqAtLocs(Services services,
                     Term heap1,
                     Term locset1,
                     Term heap2,
                     Term locset2)

Get eqAtLocs function as a term.

Parameters:

services - the Services object.

heap1 - the first heap term.

locset1 - the first location set term.

heap2 - the first heap term.

locset2 - the first location set term.

Returns:

The eqAtLocs function term.

eqAtLocsPost

public Term eqAtLocsPost(Services services,
                         Term heap1Pre,
                         Term heap1Post,
                         Term locset1,
                         Term heap2Pre,
                         Term heap2Post,
                         Term locset2)

Get eqAtLocsPost function as a term.

Parameters:

services - the Services object.

heap1Pre - the first pre-heap term.

heap1Post - the first post-heap term.

locset1 - the first location set term.

heap2Pre - the second pre-heap term.

heap2Post - the second post-heap term.

locset2 - the second location set term.

Returns:

The eqAtLocsPost function term.