public class PostconditionGenerator extends BaseGenerator
Code generator for postconditions.
| Fields inherited from class | Fields |
|---|---|
class BaseGenerator |
INVARIANT_CLOSURE_PREFIX, META_DATA_USE_INLINE_MODE |
| 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 |
getInvariantMethodName, getInvariantMethodNode |
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.