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-2022 The Apache Software Foundation. All rights reserved.