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 Todd.Sch...@gmail.com 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 melonhea...@gmail.com 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 t...@cs.washington.edu on 7 Jan 2014 at 8:18