rtc violation precondition : args[..].toString == []

[markro49]

Several of the test cases run the rtc test to completion, but the rtc-violations.txt file contains:

Violations:
violated on entry of main(java.lang.String[]) : precondition : args[..].toString == []
violated on exit of main(java.lang.String[]) : postcondition : args[..].toString == []

Here is an email thread from 6/8/2015:

Mark-

There seems to be two separate problems here:

1. Quant.collectObject is expecting the second argument to be a Field
   not a Method. ("toString()" is passed in)

Thanks for teasing the problem apart and figuring out the pieces.
Handling method invocations should be relatively straightforward to add as an enhancement to Quant.collectObject, right?

2. While the comments suggest that Quant.collectObject can deal with
   the object being an array, it cannot. True, there is code that tests
   if
   fieldObject.getClass().isArray() but we will never get there because
   the code that sets fieldObject fails if the passed in object is an array.

I don't interpret the comments as saying that the passed-in object can be an array, but I agree that it would be better if it could.

When there are more fields to access (comment "// recursive case: more fields to access after this one", there are 3 cases:

• list implementor
• array
• neither (ie, normal object)

However, the very first think that happens (in the try clause) handles just one of these cases: the last one. It would be better for it to be able to handle any of the cases.

One way to do this would be to restructure the current loop: set fieldObj to object at the very beginning and iterate n times rather than treating the first dereference specially and iterating n-1 more times.

Another way to do this would be to abstract out the code that takes an object and returns fields of it.

When working with this code, you might find it helpful to focus on one specific case (such as boolean type) and get that working first, together with test cases, before trying to edit the .jpp file.

                 -Mike

Subject: RE: rtc-violations.txt
From: "Mark Roberts" [email protected]
To: "'Michael Ernst'" [email protected]
Date: Fri, 5 Jun 2015 14:12:15 -0700

There seems to be two separate problems here:

1. Quant.collectObject is expecting the second argument to be a Field
   not a Method. ("toString()" is passed in)

2. While the comments suggest that Quant.collectObject can deal with
   the object being an array, it cannot. True, there is code that tests
   if
   fieldObject.getClass().isArray() but we will never get there because
   the code that sets fieldObject fails if the passed in object is an array.
   I'm
   not sure how to correct this, but I suspect that we need something
   like

if (object.getClass().isArray())
Class<?> component_object =
object.getClass().getComponentType();

I'm not sure how this might integrate with the non-array case.

Ideas?

Thank you,
Mark

-----Original Message-----
From: Michael Ernst [mailto:[email protected]]
Sent: Tuesday, June 02, 2015 5:59 AM
To: Mark Roberts
Subject: Re: rtc-violations.txt

Mark-

The problem is that

daikon.Quant.collectObject(args, "toString()")

is evaluating to null. I have not yet figured out why that is
happening, though.

                 -Mike

[monperrus]

Together with @SophieHYe, we hit this bug. Any idea on how to fix it?

Thanks! --Martin