getRewriteTaclet
public InfFlowContractAppTaclet getRewriteTaclet()
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>