Daikon version 5.2.4, released May 1, 2015; http://plse.cs.washington.edu/daikon. Reading declaration files [20:13:04]: Processing trace data; reading 1 dtrace file: [20:13:05]: Checking size of D:\workshop\t2framework\repos\experiments\strucOra [20:13:06]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:13:07]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:13:08]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:13:09]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:13:10]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:13:11]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:13:12]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:13:13]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:13:14]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:13:17]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:13:18]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:13:19]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:13:20]: Finished reading D:\workshop\t2framework\repos\experiments\strucOra The --output_num_samples debugging flag is on. Some of the debugging output may only make sense to Daikon programmers. =========================================================================== add(double):::ENTER 12320 samples Variables: arg0 arg0 != 0 (12320 samples) =========================================================================== add(double):::EXIT 12320 samples Variables: arg0 exception return orig(arg0) Unmodified variables: arg0 arg0 == orig(arg0) (12320 samples) arg0 != 0 (12320 samples) exception == "" (12320 samples) return != null (12320 samples) [No samples for classValue():::ENTER] =========================================================================== classValue():::EXIT 11233 samples Variables: exception return exception == "" (11233 samples) return != null (11233 samples) [No samples for clear():::ENTER] =========================================================================== clear():::EXIT 11154 samples Variables: exception return exception == "" (11154 samples) return != null (11154 samples) =========================================================================== containsKey(Object):::ENTER 1432 samples Variables: arg0 =========================================================================== containsKey(Object):::EXIT 1432 samples Variables: arg0 exception return return.TRUE return.FALSE return.TYPE orig(arg0) Modified variables: arg0 exception == "" (1432 samples) return.TRUE == true (1432 samples) return.FALSE == false (1432 samples) return.TYPE has only one value (1432 samples) return.TYPE != null (1432 samples) =========================================================================== containsValue(Object):::ENTER 1387 samples Variables: arg0 arg0 != null (1387 samples) =========================================================================== containsValue(Object):::EXIT 1387 samples Variables: arg0 exception return return.TRUE return.FALSE return.TYPE orig(arg0) Modified variables: arg0 arg0 != null (1387 samples) exception == "" (1387 samples) return.TRUE == true (1387 samples) return.FALSE == false (1387 samples) return.TYPE has only one value (1387 samples) return.TYPE != null (1387 samples) [No samples for copy():::ENTER] =========================================================================== copy():::EXIT 22706 samples Variables: exception return exception == "" (22706 samples) return != null (22706 samples) =========================================================================== divide(double):::ENTER 12412 samples Variables: arg0 arg0 != 0 (12412 samples) =========================================================================== divide(double):::EXIT 12412 samples Variables: arg0 exception return orig(arg0) Unmodified variables: arg0 arg0 == orig(arg0) (12412 samples) arg0 != 0 (12412 samples) exception == "" (12412 samples) return != null (12412 samples) [No samples for entrySet():::ENTER] =========================================================================== entrySet():::EXIT 11319 samples Variables: exception return[] size(return[]) size(return[])-1 exception == "" (11319 samples) =========================================================================== equals(Object):::ENTER 1171 samples Variables: arg0 arg0 != null (1171 samples) =========================================================================== equals(Object):::EXIT 1171 samples Variables: arg0 exception return return.TRUE return.FALSE return.TYPE orig(arg0) Modified variables: arg0 arg0 != null (1171 samples) exception == "" (1171 samples) return.TRUE == true (1171 samples) return.FALSE == false (1171 samples) return.TYPE has only one value (1171 samples) return.TYPE != null (1171 samples) =========================================================================== get(Object):::ENTER 2789 samples Variables: arg0 =========================================================================== get(Object):::EXIT 2789 samples Variables: arg0 exception return return.POSITIVE_INFINITY return.NEGATIVE_INFINITY return.NaN return.MAX_VALUE return.MIN_NORMAL return.MIN_VALUE return.MAX_EXPONENT return.MIN_EXPONENT return.SIZE return.BYTES return.TYPE orig(arg0) Modified variables: arg0 return.POSITIVE_INFINITY one of { 0.0, Infinity } (2789 samples) return.NEGATIVE_INFINITY one of { -Infinity, 0.0 } (2789 samples) return.NaN one of { 0.0, Double.NaN } (2789 samples) return.MAX_VALUE one of { 0.0, 1.7976931348623157E308 } (2789 samples) return.MIN_NORMAL == 0.0 (2789 samples) return.MIN_VALUE == 0.0 (2789 samples) return.MAX_EXPONENT one of { 0, 1023 } (2789 samples) return.MIN_EXPONENT one of { -1022, 0 } (2789 samples) return.SIZE one of { 0, 64 } (2789 samples) return.BYTES one of { 0, 8 } (2789 samples) return.TYPE != null (2789 samples) return <= return.POSITIVE_INFINITY (2789 samples) return >= return.NEGATIVE_INFINITY (2789 samples) return <= return.MAX_VALUE (2789 samples) return.POSITIVE_INFINITY >= return.NEGATIVE_INFINITY (2789 samples) return.POSITIVE_INFINITY >= return.MAX_VALUE (2789 samples) return.POSITIVE_INFINITY >= return.MIN_NORMAL (2789 samples) return.POSITIVE_INFINITY >= return.MIN_VALUE (2789 samples) return.NEGATIVE_INFINITY <= return.MAX_VALUE (2789 samples) return.NEGATIVE_INFINITY <= return.MIN_NORMAL (2789 samples) return.NEGATIVE_INFINITY <= return.MIN_VALUE (2789 samples) return.MAX_VALUE >= return.MIN_NORMAL (2789 samples) return.MAX_VALUE >= return.MIN_VALUE (2789 samples) return.MAX_EXPONENT >= return.MIN_EXPONENT (2789 samples) return.MAX_EXPONENT >= return.SIZE (2789 samples) return.MAX_EXPONENT >= return.BYTES (2789 samples) return.MIN_EXPONENT <= return.SIZE (2789 samples) return.MIN_EXPONENT <= return.BYTES (2789 samples) return.SIZE >= return.BYTES (2789 samples) [No samples for getID():::ENTER] =========================================================================== getID():::EXIT 1359 samples Variables: exception return return.MIN_VALUE return.MAX_VALUE return.TYPE return.SIZE return.BYTES exception == "" (1359 samples) return.MIN_VALUE == -2147483648 (1359 samples) return.MAX_VALUE == 2147483647 (1359 samples) return.TYPE has only one value (1359 samples) return.TYPE != null (1359 samples) return.SIZE == 32 (1359 samples) return.BYTES == 4 (1359 samples) return > return.MIN_VALUE (1359 samples) return < return.MAX_VALUE (1359 samples) return != return.SIZE (1359 samples) return > return.BYTES (1359 samples) [No samples for hashCode():::ENTER] =========================================================================== hashCode():::EXIT 1375 samples Variables: exception return return.MIN_VALUE return.MAX_VALUE return.TYPE return.SIZE return.BYTES exception == "" (1375 samples) return != 0 (1375 samples) return.MIN_VALUE == -2147483648 (1375 samples) return.MAX_VALUE == 2147483647 (1375 samples) return.TYPE has only one value (1375 samples) return.TYPE != null (1375 samples) return.SIZE == 32 (1375 samples) return.BYTES == 4 (1375 samples) return > return.MIN_VALUE (1375 samples) return < return.MAX_VALUE (1375 samples) return != return.BYTES (1375 samples) [No samples for isEmpty():::ENTER] =========================================================================== isEmpty():::EXIT 1404 samples Variables: exception return return.TRUE return.FALSE return.TYPE return == return.FALSE (1404 samples) exception == "" (1404 samples) return == false (1404 samples) return.TRUE == true (1404 samples) return.TYPE has only one value (1404 samples) return.TYPE != null (1404 samples) [No samples for iterator():::ENTER] =========================================================================== iterator():::EXIT 11185 samples Variables: exception return exception == "" (11185 samples) return != null (11185 samples) [No samples for keySet():::ENTER] =========================================================================== keySet():::EXIT 22370 samples Variables: exception return[] size(return[]) size(return[])-1 exception == "" (22370 samples) =========================================================================== minus(double):::ENTER 12380 samples Variables: arg0 arg0 != 0 (12380 samples) =========================================================================== minus(double):::EXIT 12380 samples Variables: arg0 exception return orig(arg0) Unmodified variables: arg0 arg0 == orig(arg0) (12380 samples) arg0 != 0 (12380 samples) exception == "" (12380 samples) return != null (12380 samples) =========================================================================== multiply(double):::ENTER 12177 samples Variables: arg0 =========================================================================== multiply(double):::EXIT 12177 samples Variables: arg0 exception return orig(arg0) Unmodified variables: arg0 arg0 == orig(arg0) (12177 samples) exception == "" (12177 samples) return != null (12177 samples) =========================================================================== net.sf.javaml.core.DenseInstance(double[]):::ENTER 13609 samples Variables: arg0[] size(arg0[]) size(arg0[])-1 arg0[] elements != null (13609 samples) =========================================================================== net.sf.javaml.core.DenseInstance(double[]):::EXIT 13609 samples Variables: arg0[] exception return orig(arg0[]) size(arg0[]) size(arg0[])-1 orig(size(arg0[])) orig(size(arg0[]))-1 Unmodified variables: arg0[] size(arg0[]) arg0[] == orig(arg0[]) (13609 samples) arg0[] elements != null (13609 samples) exception == "" (13609 samples) return != null (13609 samples) =========================================================================== net.sf.javaml.core.DenseInstance(double[],Object):::ENTER 13764 samples Variables: arg0[] arg1 size(arg0[]) size(arg0[])-1 arg0[] elements != null (13764 samples) arg1 != null (13764 samples) =========================================================================== net.sf.javaml.core.DenseInstance(double[],Object):::EXIT 13764 samples Variables: arg0[] arg1 exception return orig(arg0[]) orig(arg1) size(arg0[]) size(arg0[])-1 orig(size(arg0[])) orig(size(arg0[]))-1 Modified variables: arg1 Unmodified variables: arg0[] size(arg0[]) arg0[] == orig(arg0[]) (13764 samples) arg0[] elements != null (13764 samples) arg1 != null (13764 samples) exception one of { "", "java.lang.NullPointerException" } (13764 samples) return != null (13764 samples) =========================================================================== net.sf.javaml.core.DenseInstance(int):::ENTER 10395 samples Variables: arg0 =========================================================================== net.sf.javaml.core.DenseInstance(int):::EXIT 10395 samples Variables: arg0 exception return orig(arg0) Unmodified variables: arg0 arg0 == orig(arg0) (10395 samples) exception one of { "", "java.lang.NegativeArraySizeException" } (10395 samples) return != null (10395 samples) [No samples for noAttributes():::ENTER] =========================================================================== noAttributes():::EXIT 11304 samples Variables: exception return return.MIN_VALUE return.MAX_VALUE return.TYPE return.SIZE return.BYTES exception == "" (11304 samples) return >= 0 (11304 samples) return.MIN_VALUE == -2147483648 (11304 samples) return.MAX_VALUE == 2147483647 (11304 samples) return.TYPE has only one value (11304 samples) return.TYPE != null (11304 samples) return.SIZE == 32 (11304 samples) return.BYTES == 4 (11304 samples) return > return.MIN_VALUE (11304 samples) return < return.MAX_VALUE (11304 samples) return != return.SIZE (11304 samples) =========================================================================== put(Integer,Double):::ENTER 7068 samples Variables: arg0 arg1 =========================================================================== put(Integer,Double):::EXIT 7068 samples Variables: arg0 arg1 exception return return.POSITIVE_INFINITY return.NEGATIVE_INFINITY return.NaN return.MAX_VALUE return.MIN_NORMAL return.MIN_VALUE return.MAX_EXPONENT return.MIN_EXPONENT return.SIZE return.BYTES return.TYPE orig(arg0) orig(arg1) Unmodified variables: arg0 arg1 arg0 == orig(arg0) (7068 samples) arg1 == orig(arg1) (7068 samples) exception one of { "", "java.lang.ArrayIndexOutOfBoundsException", "java.lang.NullPointerException" } (7068 samples) return.POSITIVE_INFINITY one of { 0.0, Infinity } (7068 samples) return.NEGATIVE_INFINITY one of { -Infinity, 0.0 } (7068 samples) return.NaN one of { 0.0, Double.NaN } (7068 samples) return.MAX_VALUE one of { 0.0, 1.7976931348623157E308 } (7068 samples) return.MIN_NORMAL == 0.0 (7068 samples) return.MIN_VALUE == 0.0 (7068 samples) return.MAX_EXPONENT one of { 0, 1023 } (7068 samples) return.MIN_EXPONENT one of { -1022, 0 } (7068 samples) return.SIZE one of { 0, 64 } (7068 samples) return.BYTES one of { 0, 8 } (7068 samples) return.TYPE != null (7068 samples) return <= return.POSITIVE_INFINITY (7068 samples) return >= return.NEGATIVE_INFINITY (7068 samples) return <= return.MAX_VALUE (7068 samples) return.POSITIVE_INFINITY >= return.NEGATIVE_INFINITY (7068 samples) return.POSITIVE_INFINITY >= return.MAX_VALUE (7068 samples) return.POSITIVE_INFINITY >= return.MIN_NORMAL (7068 samples) return.POSITIVE_INFINITY >= return.MIN_VALUE (7068 samples) return.NEGATIVE_INFINITY <= return.MAX_VALUE (7068 samples) return.NEGATIVE_INFINITY <= return.MIN_NORMAL (7068 samples) return.NEGATIVE_INFINITY <= return.MIN_VALUE (7068 samples) return.MAX_VALUE >= return.MIN_NORMAL (7068 samples) return.MAX_VALUE >= return.MIN_VALUE (7068 samples) return.MAX_EXPONENT >= return.MIN_EXPONENT (7068 samples) return.MAX_EXPONENT >= return.SIZE (7068 samples) return.MAX_EXPONENT >= return.BYTES (7068 samples) return.MIN_EXPONENT <= return.SIZE (7068 samples) return.MIN_EXPONENT <= return.BYTES (7068 samples) return.SIZE >= return.BYTES (7068 samples) =========================================================================== put(Object,Object):::ENTER 4829 samples Variables: arg0 arg1 arg0 != null (4829 samples) arg1 != null (4829 samples) =========================================================================== put(Object,Object):::EXIT 4829 samples Variables: arg0 arg1 exception return orig(arg0) orig(arg1) Modified variables: arg0 arg1 arg0 != null (4829 samples) arg1 != null (4829 samples) exception one of { "java.lang.ClassCastException", "java.lang.NullPointerException" } (4829 samples) return != null (4829 samples) =========================================================================== putAll(Map):::ENTER 6272 samples Variables: arg0 =========================================================================== putAll(Map):::EXIT 6272 samples Variables: arg0 exception return orig(arg0) Modified variables: arg0 exception one of { "", "java.lang.ArrayIndexOutOfBoundsException", "java.lang.NullPointerException" } (6272 samples) return != null (6272 samples) =========================================================================== remove(Object):::ENTER 7288 samples Variables: arg0 =========================================================================== remove(Object):::EXIT 7288 samples Variables: arg0 exception return orig(arg0) Modified variables: arg0 exception == "java.lang.UnsupportedOperationException" (7288 samples) return != null (7288 samples) =========================================================================== removeAttribute(int):::ENTER 5592 samples Variables: arg0 =========================================================================== removeAttribute(int):::EXIT 5592 samples Variables: arg0 exception return orig(arg0) Unmodified variables: arg0 arg0 == orig(arg0) (5592 samples) exception one of { "", "java.lang.ArrayIndexOutOfBoundsException", "java.lang.NegativeArraySizeException" } (5592 samples) return != null (5592 samples) =========================================================================== removeAttributes(Set):::ENTER 7504 samples Variables: arg0[] size(arg0[]) size(arg0[])-1 =========================================================================== removeAttributes(Set):::EXIT 7504 samples Variables: arg0[] exception return orig(arg0[]) size(arg0[]) size(arg0[])-1 orig(size(arg0[])) orig(size(arg0[]))-1 Unmodified variables: arg0[] size(arg0[]) arg0[] == orig(arg0[]) (7504 samples) return != null (7504 samples) =========================================================================== setClassValue(Object):::ENTER 12344 samples Variables: arg0 arg0 != null (12344 samples) =========================================================================== setClassValue(Object):::EXIT 12344 samples Variables: arg0 exception return orig(arg0) Modified variables: arg0 arg0 != null (12344 samples) exception == "" (12344 samples) return != null (12344 samples) [No samples for size():::ENTER] =========================================================================== size():::EXIT 1387 samples Variables: exception return return.MIN_VALUE return.MAX_VALUE return.TYPE return.SIZE return.BYTES exception == "" (1387 samples) return >= 0 (1387 samples) return.MIN_VALUE == -2147483648 (1387 samples) return.MAX_VALUE == 2147483647 (1387 samples) return.TYPE has only one value (1387 samples) return.TYPE != null (1387 samples) return.SIZE == 32 (1387 samples) return.BYTES == 4 (1387 samples) return > return.MIN_VALUE (1387 samples) return < return.MAX_VALUE (1387 samples) return != return.SIZE (1387 samples) [No samples for sqrt():::ENTER] =========================================================================== sqrt():::EXIT 11235 samples Variables: exception return exception == "" (11235 samples) return != null (11235 samples) [No samples for toString():::ENTER] =========================================================================== toString():::EXIT 1295 samples Variables: exception return return.CASE_INSENSITIVE_ORDER exception == "" (1295 samples) return.CASE_INSENSITIVE_ORDER has only one value (1295 samples) return.CASE_INSENSITIVE_ORDER != null (1295 samples) exception < return (1295 samples) =========================================================================== value(int):::ENTER 5566 samples Variables: arg0 =========================================================================== value(int):::EXIT 5566 samples Variables: arg0 exception return return.POSITIVE_INFINITY return.NEGATIVE_INFINITY return.NaN return.MAX_VALUE return.MIN_NORMAL return.MIN_VALUE return.MAX_EXPONENT return.MIN_EXPONENT return.SIZE return.BYTES return.TYPE orig(arg0) Unmodified variables: arg0 arg0 == orig(arg0) (5566 samples) exception one of { "", "java.lang.ArrayIndexOutOfBoundsException" } (5566 samples) return.POSITIVE_INFINITY one of { 0.0, Infinity } (5566 samples) return.NEGATIVE_INFINITY one of { -Infinity, 0.0 } (5566 samples) return.NaN one of { 0.0, Double.NaN } (5566 samples) return.MAX_VALUE one of { 0.0, 1.7976931348623157E308 } (5566 samples) return.MIN_NORMAL == 2.2250738585072014E-308 (5566 samples) return.MIN_VALUE == 4.9E-324 (5566 samples) return.MAX_EXPONENT one of { 0, 1023 } (5566 samples) return.MIN_EXPONENT one of { -1022, 0 } (5566 samples) return.SIZE one of { 0, 64 } (5566 samples) return.BYTES one of { 0, 8 } (5566 samples) return.TYPE != null (5566 samples) return <= return.POSITIVE_INFINITY (5566 samples) return >= return.NEGATIVE_INFINITY (5566 samples) return <= return.MAX_VALUE (5566 samples) return.POSITIVE_INFINITY >= return.NEGATIVE_INFINITY (5566 samples) return.POSITIVE_INFINITY >= return.MAX_VALUE (5566 samples) return.POSITIVE_INFINITY >= return.MIN_NORMAL (5566 samples) return.POSITIVE_INFINITY >= return.MIN_VALUE (5566 samples) return.NEGATIVE_INFINITY <= return.MAX_VALUE (5566 samples) return.NEGATIVE_INFINITY <= return.MIN_NORMAL (5566 samples) return.NEGATIVE_INFINITY <= return.MIN_VALUE (5566 samples) return.MAX_VALUE >= return.MIN_NORMAL (5566 samples) return.MAX_VALUE >= return.MIN_VALUE (5566 samples) return.MAX_EXPONENT >= return.MIN_EXPONENT (5566 samples) return.MAX_EXPONENT >= return.SIZE (5566 samples) return.MAX_EXPONENT >= return.BYTES (5566 samples) return.MIN_EXPONENT <= return.SIZE (5566 samples) return.MIN_EXPONENT <= return.BYTES (5566 samples) return.SIZE >= return.BYTES (5566 samples) [No samples for values():::ENTER] =========================================================================== values():::EXIT 11332 samples Variables: exception return[] size(return[]) size(return[])-1 exception == "" (11332 samples) =========================================================================== Variables: non_canonical_variables = 0 can_be_missing_variables = 0 canonical_variables = 0 total variables = 0 Derivation: derived_variables = 24 suppressed derived variables = 0 nonsensical_suppressed_derived_variables = 0 tautological_suppressed_derived_variables = 0 Inference: Non-instantiated: 0 true = 0 implied_noninstantiated_invariants = 0 subexact_noninstantiated_invariants = 0 false = 0 implied_false_noninstantiated_invariants = 0 partially_implied_invariants = 0 Instantiated: 4080 = 3072 falsified_invariants = 1833 non_falsified_invariants = 1239 = 230 unjustified = 0 too_few_samples_invariants = 0 unjustified_invariants = 0 implied = 0 non_canonical_invariants = 0 obvious_invariants = 0 reported_invariants = 230 Exiting Daikon.