public class PostconditionGenerator extends BaseGenerator
Code generator for postconditions.
| Fields inherited from class | Fields | 
|---|---|
| class BaseGenerator | INVARIANT_CLOSURE_PREFIX, META_DATA_USE_INLINE_MODE, source | 
| Constructor and description | 
|---|
| PostconditionGenerator(ReaderSource source) | 
| Type Params | Return Type | Name and description | 
|---|---|---|
|  | public void | addOldVariablesMethod(ClassNode classNode)Adds a synthetic method to the given classNode which can be used to create a map of most instance variables found in this class. | 
|  | public void | generateDefaultPostconditionStatement(ClassNode type, MethodNode method)Adds a default postcondition if a postcondition has already been defined for this MethodNode in a super-class. | 
|  | public void | generatePostconditionAssertionStatement(MethodNode method, Postcondition postcondition)Injects a postcondition assertion statement in the given method, based on the booleanExpression. | 
| Methods inherited from class | Name | 
|---|---|
| class BaseGenerator | addCallsToSuperMethodNodeAnnotationClosure, getInlineModeBlockStatement, getInvariantMethodName, getInvariantMethodNode, wrapAssertionBooleanExpression | 
Adds a synthetic method to the given classNode which can be used to create a map of most instance variables found in this class. Used for the old variable mechanism.
classNode -  the ClassNode to add the synthetic method toAdds a default postcondition if a postcondition has already been defined for this MethodNode in a super-class.
type -    the current ClassNode of the given methodNodemethod -  the MethodNode to create the default postcondition forInjects a postcondition assertion statement in the given method, based on the booleanExpression.
method -         the MethodNode for assertion injectionpostcondition -  the Postcondition the assertion statement should be generated fromCopyright © 2003-2025 The Apache Software Foundation. All rights reserved.