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 |