| Class | Description |
|---|---|
| AbstractInfFlowContractAppTacletBuilder |
Builds the rule which inserts information flow contract applications.
|
| AbstractInfFlowTacletBuilder |
Builds the rule which inserts information flow contract applications.
|
| AbstractInfFlowUnfoldTacletBuilder |
Builds the rule which inserts information flow contract applications.
|
| BlockInfFlowUnfoldTacletBuilder | |
| InfFlowBlockContractTacletBuilder |
Implements the rule which inserts operation contracts for a method call.
|
| InfFlowLoopInvariantTacletBuilder |
Implements the rule which inserts loop invariants for a method call.
|
| InfFlowMethodContractTacletBuilder |
Implements the rule which inserts operation contracts for a method call.
|
| LoopInfFlowUnfoldTacletBuilder | |
| MethodInfFlowUnfoldTacletBuilder |