Ensure @AssumeAssertion and -AassumeAssertionsAreEnabled/Disabled do not interact and add test coverage to this effect

[GoogleCodeExporter]

Ensure @AssumeAssertion and -AassumeAssertionsAreEnabled/Disabled do not 
interact and add test coverage to ensure this is maintained.

Original issue reported on code.google.com by jtha...@cs.washington.edu on 19 Mar 2015 at 9:45

[GoogleCodeExporter]

The fix for this in CFGBuilder.java is already pushed. However, while adding 
test coverage for this, I discovered a bug in NullnessVisitor.java :

    @Override
    public Void visitAssert(AssertTree node, Void p) {
        if (checker.hasOption("assumeAssertionsAreDisabled")) {
            // If the assert is assumed to be disabled, don't check anything in it.
            return null;
        } else {
            checkForNullability(node.getCondition(), CONDITION_NULLABLE);
            return super.visitAssert(node, p);
        }
    }

This is the wrong behavior as it assumes that assumeAssertionsAreDisabled takes 
precedence - it doesn't. However the code that determined whether a particular 
assertion was enabled (looking at both command-line options and looking for 
@AssumeAssertion) lives in CFGBuilder. That is called before NullnessVisitor, 
and the information is not readily available to NullnessVisitor. A potential 
solution would be to factor out the code that determines this into a utility 
method and call it from both locations.

Original comment by jtha...@cs.washington.edu on 9 Apr 2015 at 6:21

[GoogleCodeExporter]

Hi Javier,
thanks for catching this error. I agree that a helper method that can be used 
to check whether a particular AssertTree should be handled would be best.
cu, WMD.

Original comment by wdi...@gmail.com on 10 Apr 2015 at 12:38

[GoogleCodeExporter]

Original comment by jtha...@cs.washington.edu on 13 Apr 2015 at 9:18

• Changed state: Pushed

[GoogleCodeExporter]

Original comment by jtha...@cs.washington.edu on 18 Apr 2015 at 6:42

• Changed state: Fixed