Numeric overflow modifying invariant discovery

[Dylan Wilson]

Hi - First thanks for addressing the two bugs I put on Github.  Owe ya'll a beer or whatever you prefer.

So - I'm playing with joda-time code that adds two longs and throws exception on overflow.

If I take care not to cause overflow, I get the correct Invariant: " return - orig(val1) - orig(val2) == 0".

If overflow happens, I don't get the desired invariant, even if I remove the throw exception bit.

Is this expected behavior?   Can I customize or extend?  

What is the view on Exceptions in general - have you entertained Pre/Post conditions associated with Exceptions (e.g. treating exceptions as special exit?). 

A smaller issue - I can also get a grumpy Daikon under some circumstances - perhaps related but I'm not primarily concerned about this.  

I've attached relevant files: Source code of unit, unit test and failure modes.

[Michael Ernst]

Thanks for your message.  I'm sorry you are having trouble.

You said:

> If overflow happens, I don't get the desired invariant

I think that the reason for this is that the invariant is not true if overflow happens.  Daikon only reports true invariants.  Can you confirm this?  In that case, Daikon is correct, and I'm not sure why you desire a different invariant.

To help us investigate and fix the problems you encountered, could you please provide a reproducible test case?  You provided only code snippets that do not compile, and you gave an English description of making some changes.  We often waste significant time trying to reproduce vague descriptions, so it is better for you to give a reproducible test case.  Please see http://plse.cs.washington.edu/daikon/download/doc/daikon.html#Reporting-problems and provide all the information that it requests.  Opening an issue in the issue tracker is a good way to collect all the information, and isa better place for bug reports than the general discussion mailing list.  Please open a different issue for each problem.  Thanks!

> What is the view on Exceptions in general - have you entertained Pre/Post conditions associated with Exceptions (e.g. treating exceptions as special exit?).

Daikon reports so-called "normal postconditions", which describe behavior when a method returns without an exception.
Daikon warns when a method throws an exception.  You can see that at the top of the log file that you attached:

> No return from procedure observed 2540 times.  Unmatched entries are ignored!
> Unterminated calls:
>   org.joda.time.field.FieldUtils.safeAdd(long, long) : 2540 invocations
> End of report for procedures not returned from.  Unmatched entries are ignored!

There is a discussion at http://plse.cs.washington.edu/daikon/download/doc/daikon.html#No-return-from-procedure .

There are two pull requests to produce invariants about exceptional execution (https://github.com/codespecs/daikon/pull/56, https://github.com/codespecs/daikon/pull/91).  The two pull requests have been reviewed but the reviews have not been addressed.  One problem is that each has code but not a formal description and justification of the meaning of the invariants and their relationship to one another.

                    -Mike

--
You received this message because you are subscribed to the Google Groups "Daikon discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to daikon-discus...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/daikon-discuss/1f630b08-0c51-4569-b782-476658b8f106n%40googlegroups.com.