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

Class AbstractInfFlowContractAppTacletBuilder.InfFlowContractAppRewriteTacletBuilder

java.lang.Object

de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder<T>

de.uka.ilkd.key.rule.tacletbuilder.FindTacletBuilder<T>

de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletBuilder<InfFlowContractAppTaclet>

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

Enclosing class:

AbstractInfFlowContractAppTacletBuilder

private class AbstractInfFlowContractAppTacletBuilder.InfFlowContractAppRewriteTacletBuilder
extends RewriteTacletBuilder<InfFlowContractAppTaclet>

A normal RewriteTacletBuilder except that an InfFlowContractAppTaclet is returned instead of a normal RewriteTaclet. InfFlowContractAppTaclet's are normal RewriteTaclet's except that the formula which is added by the taclets are also added to the list of formulas contained in the INF_FLOW_CONTRACT_APPL_PROPERTY. The INF_FLOW_CONTRACT_APPL_PROPERTY is used by the macros UseInformationFlowContractMacro and PrepareInfFlowContractPreBranchesMacro to decide how to prepare the formulas resulting from information flow contract applications.

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder

TacletBuilder.TacletBuilderException

Field Summary

Fields inherited from class de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletBuilder

applicationRestriction, surviveSmbExec

Fields inherited from class de.uka.ilkd.key.rule.tacletbuilder.FindTacletBuilder

find

Fields inherited from class de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder

attrs, choices, goal2Choices, goals, ifseq, name, NONAME, ruleSets, taclet, tacletAnnotations, variableConditions, varsNew, varsNewDependingOn, varsNotFreeIn

Constructor Summary

Constructors

Constructor and Description
InfFlowContractAppRewriteTacletBuilder()

Method Summary

Modifier and Type	Method and Description
InfFlowContractAppTaclet	getRewriteTaclet() builds and returns the RewriteTaclet that is specified by former set... / add... methods.

Methods inherited from class de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletBuilder

addGoalTerm, addTacletGoalTemplate, getTaclet, setApplicationRestriction, setFind, setSurviveSmbExec

Methods inherited from class de.uka.ilkd.key.rule.tacletbuilder.FindTacletBuilder

checkBoundInIfAndFind, getFind

Methods inherited from class de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder

addGoal2ChoicesMapping, addRuleSet, addVariableCondition, addVarsNew, addVarsNew, addVarsNew, addVarsNew, addVarsNewDependingOn, addVarsNotFreeIn, addVarsNotFreeIn, addVarsNotFreeIn, addVarsNotFreeIn, getChoices, getGoal2Choices, getName, getTacletWithoutInactiveGoalTemplates, goalTemplates, ifSequent, setAnnotations, setChoices, setDisplayName, setHelpText, setIfSequent, setName, setRuleSets, setTacletGoalTemplates, setTrigger, varsNotFreeIn

Methods inherited from class java.lang.Object

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

Constructor Detail

InfFlowContractAppRewriteTacletBuilder

InfFlowContractAppRewriteTacletBuilder()

Method Detail

getRewriteTaclet

public InfFlowContractAppTaclet getRewriteTaclet()

Description copied from class: RewriteTacletBuilder

builds and returns the RewriteTaclet that is specified by former set... / add... methods. If no name is specified then an Taclet with an empty string name is build. No specifications for variable conditions, goals or heuristics imply that the corresponding parts of the Taclet are empty. No specification for the if-sequent is represented as a sequent with two empty semisequents. No specification for the interactive or recursive flags imply that the flags are not set. No specified find part causes an TacletBuilderException. Throws an TacletBuilderException if a bound SchemaVariable occurs more than once in if and find or an InvalidPrefixException if the building of the Taclet Prefix fails.

Overrides:

getRewriteTaclet in class RewriteTacletBuilder<InfFlowContractAppTaclet>