Formatting and Filtering Improvements

[GoogleCodeExporter]

When going through the Daikon output, I noticed a few things that you might 
want to change or suppress:

* I got invariants that enum values are non-null. That’s a property of C# and 
does not have to be reported as invariant.
* I got postconditions of the form T.val == OlvValue(T.val), where T is an enum 
type. Since T.val is a constant, this does not have to be reported.
* I got postconditions of the form this.left==OldValue(l), where l is a formal 
parameter. I suggest dropping the OldValue around l; taking the old value is 
the code contracts semantics anyway.
* For a method with return type int, I got a contract for the exceptional case 
about Contract.Result<System.Exception>(). This is not a valid expression, 
neither in a normal nor in an exceptional postcondition (ccrewrite fails).
* I got preconditions on out-parameters, which is neither valid in code 
contracts nor meaningful.
* I got a forall-expression over an array a, where the upper bound was written 
as a.Count() instead of a.Length.
* I got output of the form (“one of.java.jpp: SEQUENCE unimplemented” != 
null).
*  For a constructor that does not assign to an integer field “value”, I 
got a postcondition this.value == System.Char.MinValue. This is weird since the 
value should be zero and since the field is an int, not a char.

Original issue reported on code.google.com by [email protected] on 31 Dec 2013 at 7:59

[GoogleCodeExporter]

Hey Todd,

Are you going to triage/prioritize these? Seems like a lot of these will need 
updates in Daikon will flags created by Celeriac. For example the 
"preconditions on out-parameters" problem could probably be solved by including 
an additional flag for out parameters in the Celeriac output. A modified Daikon 
would need to notice this flag then omit invariants on preconditions about 
these variables.

Original comment by [email protected] on 7 Jan 2014 at 1:35

[GoogleCodeExporter]

I haven't triaged them yet since I haven't had time to work on Celeriac. They 
will be triaged as we work on the new Contract Inserter add-in and need to fix 
them. Additionally, the ones that belong on the Daikon-fork's issue tracker 
will be moved at that point as well.

These issues were actually reported by Peter in November. They weren't blocking 
his work at the time.

Original comment by [email protected] on 7 Jan 2014 at 8:18