private class AbstractInfFlowContractAppTacletBuilder.InfFlowContractAppRewriteTacletBuilder extends RewriteTacletBuilder<InfFlowContractAppTaclet>
TacletBuilder.TacletBuilderException
applicationRestriction, surviveSmbExec
find
attrs, choices, goal2Choices, goals, ifseq, name, NONAME, ruleSets, taclet, tacletAnnotations, variableConditions, varsNew, varsNewDependingOn, varsNotFreeIn
Constructor and Description |
---|
InfFlowContractAppRewriteTacletBuilder() |
Modifier and Type | Method and Description |
---|---|
InfFlowContractAppTaclet |
getRewriteTaclet()
builds and returns the RewriteTaclet that is specified by
former set... / add... methods.
|
addGoalTerm, addTacletGoalTemplate, getTaclet, setApplicationRestriction, setFind, setSurviveSmbExec
checkBoundInIfAndFind, getFind
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
public InfFlowContractAppTaclet getRewriteTaclet()
RewriteTacletBuilder
getRewriteTaclet
in class RewriteTacletBuilder<InfFlowContractAppTaclet>