Class PostconditionGenerator

  • public class PostconditionGenerator
    extends BaseGenerator

    Code generator for postconditions.

    • Constructor Detail

      • PostconditionGenerator

        public PostconditionGenerator​(ReaderSource source)
    • Method Detail

      • addOldVariablesMethod

        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. Used for the old variable mechanism.
        classNode - the ClassNode to add the synthetic method to
      • generatePostconditionAssertionStatement

        public void generatePostconditionAssertionStatement​(MethodNode method,
                                                            Postcondition postcondition)
        Injects a postcondition assertion statement in the given method, based on the booleanExpression.
        method - the MethodNode for assertion injection
        postcondition - the Postcondition the assertion statement should be generated from
      • generateDefaultPostconditionStatement

        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.
        type - the current ClassNode of the given methodNode
        method - the MethodNode to create the default postcondition for