codespecs / daikon

Dynamic detection of likely invariants
http://plse.cs.washington.edu/daikon/
Other
214 stars 54 forks source link

Runtime check instrumentation fail for EltOneOf invariant #17

Closed mernst closed 8 years ago

mernst commented 9 years ago

Originally reported on Google Code with ID 17

What steps will reproduce the problem?
1. Unzip the attached file
2. java -cp daikon.jar:bin daikon.tools.runtimechecker.Main  instrument DataStructures.QueueArEvoSuiteTest0.inv.gz
src/DataStructures/QueueAr.java
3. javac -cp bin:daikon.jar instrumented-classes/DataStructures/QueueAr.java 

What is the expected output? 
A compiled QueueAr.class 

What do you see instead?
instrumented-classes/DataStructures/QueueAr.java:420: error: incomparable types: boolean
and int
         if ( !((retval_instrument != 0) == (this.currentSize == 0)) )
                                   ^
instrumented-classes/DataStructures/QueueAr.java:989: error: incomparable types: boolean
and int
         if ( !((retval_instrument != 0) == (retval_instrument == true)) )
                                   ^
instrumented-classes/DataStructures/QueueAr.java:1431: error: incompatible types
         if ( !(daikon.Quant.subsetOf(this.theArray, new long[] { null, 1964752463
})) )
                                                                  ^
  required: long
  found:    <null>
instrumented-classes/DataStructures/QueueAr.java:1645: error: incompatible types
         if ( !(daikon.Quant.subsetOf(this.theArray, new long[] { null, 1964752463
})) )
                                                                  ^
  required: long
  found:    <null>
instrumented-classes/DataStructures/QueueAr.java:1850: error: incompatible types
         if ( !(daikon.Quant.subsetOf(this.theArray, new long[] { null, 1096993286
})) )
                                                                  ^
  required: long
  found:    <null>

What version of the product are you using? 
Daikon release 4.7.3

On what operating system?
Darwin dhcp-139.st.cs.uni-saarland.de 11.4.2 Darwin Kernel Version 11.4.2: Thu Aug
23 16:25:48 PDT 2012; root:xnu-1699.32.7~1/RELEASE_X86_64 x86_64

Please provide any additional information below.
I think that the problem is located in 
daikon.inv.unary.sequence.EltOneOf (the null being printed in the new long[] array)
and
daikon.inv.unary.scalar.NonZero

Reported by jgaleotti on 2013-12-04 09:11:59


markro49 commented 8 years ago

No longer fails with current version of Daikon. Compiles without error and also runs runtimecheck.WriteViolationFile without error.