Daikon version 5.2.4, released May 1, 2015; http://plse.cs.washington.edu/daikon. Reading declaration files [20:03:50]: Processing trace data; reading 1 dtrace file: [20:03:51]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:03:52]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:03:53]: Reading D:\workshop\t2framework\repos\experiments\strucOracles\daik [20:03:53]: 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. [No samples for Examples.BinarySearchTree():::ENTER] =========================================================================== Examples.BinarySearchTree():::EXIT 2490 samples Variables: exception return exception == "" (2490 samples) return != null (2490 samples) =========================================================================== find(Comparable):::ENTER 4726 samples Variables: arg0 =========================================================================== find(Comparable):::EXIT 4726 samples Variables: arg0 exception return return.MIN_VALUE return.MAX_VALUE return.TYPE return.SIZE return.BYTES return.TRUE return.FALSE orig(arg0) Modified variables: arg0 exception one of { "", "java.lang.ClassCastException", "java.lang.IllegalArgumentException" } (4726 samples) return.MIN_VALUE one of { -2147483648, 0 } (4726 samples) return.MAX_VALUE one of { 0, 2147483647 } (4726 samples) return.TYPE != null (4726 samples) return.SIZE one of { 0, 32 } (4726 samples) return.BYTES one of { 0, 4 } (4726 samples) return.FALSE == false (4726 samples) return.MIN_VALUE <= return.MAX_VALUE (4726 samples) return.MIN_VALUE <= return.SIZE (4726 samples) return.MIN_VALUE <= return.BYTES (4726 samples) return.MAX_VALUE >= return.SIZE (4726 samples) return.MAX_VALUE >= return.BYTES (4726 samples) return.SIZE >= return.BYTES (4726 samples) [No samples for findMax():::ENTER] =========================================================================== findMax():::EXIT 4479 samples Variables: exception return return.MIN_VALUE return.MAX_VALUE return.TYPE return.SIZE return.BYTES return.POSITIVE_INFINITY return.NEGATIVE_INFINITY return.NaN return.MIN_NORMAL return.MAX_EXPONENT return.MIN_EXPONENT return.TRUE return.FALSE exception == "" (4479 samples) return.MIN_VALUE <= 1.4E-45 (4479 samples) return.MAX_VALUE >= 0.0 (4479 samples) return.TYPE != null (4479 samples) return.SIZE >= 0 (4479 samples) return.BYTES >= 0 (4479 samples) return.POSITIVE_INFINITY one of { 0.0, Infinity } (4479 samples) return.NEGATIVE_INFINITY one of { -Infinity, 0.0 } (4479 samples) return.NaN one of { 0.0, Double.NaN } (4479 samples) return.MIN_NORMAL == 0.0 (4479 samples) return.MAX_EXPONENT one of { 0, 127, 1023 } (4479 samples) return.MIN_EXPONENT one of { -1022, -126, 0 } (4479 samples) return.FALSE == false (4479 samples) return.MIN_VALUE <= return.MAX_VALUE (4479 samples) return.MIN_VALUE <= return.POSITIVE_INFINITY (4479 samples) return.MIN_VALUE <= return.MIN_NORMAL (4479 samples) return.MAX_VALUE >= return.NEGATIVE_INFINITY (4479 samples) return.MAX_VALUE >= return.MIN_NORMAL (4479 samples) return.SIZE - 8 * return.BYTES == 0 (4479 samples) return.SIZE >= return.BYTES (4479 samples) return.SIZE >= return.MIN_EXPONENT (4479 samples) return.BYTES >= return.MIN_EXPONENT (4479 samples) return.POSITIVE_INFINITY >= return.NEGATIVE_INFINITY (4479 samples) return.POSITIVE_INFINITY >= return.MIN_NORMAL (4479 samples) return.NEGATIVE_INFINITY <= return.MIN_NORMAL (4479 samples) return.MAX_EXPONENT >= return.MIN_EXPONENT (4479 samples) [No samples for findMin():::ENTER] =========================================================================== findMin():::EXIT 4411 samples Variables: 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 return.TRUE return.FALSE exception == "" (4411 samples) return.POSITIVE_INFINITY one of { 0.0, Infinity } (4411 samples) return.NEGATIVE_INFINITY one of { -Infinity, 0.0 } (4411 samples) return.NaN one of { 0.0, Double.NaN } (4411 samples) return.MAX_VALUE >= 0.0 (4411 samples) return.MIN_NORMAL == 0.0 (4411 samples) return.MIN_VALUE <= 1.4E-45 (4411 samples) return.MAX_EXPONENT one of { 0, 127, 1023 } (4411 samples) return.MIN_EXPONENT one of { -1022, -126, 0 } (4411 samples) return.SIZE >= 0 (4411 samples) return.BYTES >= 0 (4411 samples) return.TYPE != null (4411 samples) return.FALSE == false (4411 samples) return.POSITIVE_INFINITY >= return.NEGATIVE_INFINITY (4411 samples) return.POSITIVE_INFINITY >= return.MIN_NORMAL (4411 samples) return.POSITIVE_INFINITY >= return.MIN_VALUE (4411 samples) return.NEGATIVE_INFINITY <= return.MAX_VALUE (4411 samples) return.NEGATIVE_INFINITY <= return.MIN_NORMAL (4411 samples) return.MAX_VALUE >= return.MIN_NORMAL (4411 samples) return.MAX_VALUE >= return.MIN_VALUE (4411 samples) return.MIN_NORMAL >= return.MIN_VALUE (4411 samples) return.MAX_EXPONENT >= return.MIN_EXPONENT (4411 samples) return.MIN_EXPONENT <= return.SIZE (4411 samples) return.MIN_EXPONENT <= return.BYTES (4411 samples) return.SIZE - 8 * return.BYTES == 0 (4411 samples) return.SIZE >= return.BYTES (4411 samples) =========================================================================== insert(Comparable):::ENTER 4605 samples Variables: arg0 =========================================================================== insert(Comparable):::EXIT 4605 samples Variables: arg0 exception return orig(arg0) Modified variables: arg0 exception one of { "", "java.lang.ClassCastException", "java.lang.IllegalArgumentException" } (4605 samples) return != null (4605 samples) [No samples for isEmpty():::ENTER] =========================================================================== isEmpty():::EXIT 974 samples Variables: exception return return.TRUE return.FALSE return.TYPE exception == "" (974 samples) return.TRUE == true (974 samples) return.FALSE == false (974 samples) return.TYPE has only one value (974 samples) return.TYPE != null (974 samples) [No samples for makeEmpty():::ENTER] =========================================================================== makeEmpty():::EXIT 4355 samples Variables: exception return exception == "" (4355 samples) return != null (4355 samples) =========================================================================== remove(Comparable):::ENTER 4615 samples Variables: arg0 =========================================================================== remove(Comparable):::EXIT 4615 samples Variables: arg0 exception return orig(arg0) Modified variables: arg0 exception one of { "", "java.lang.ClassCastException", "java.lang.IllegalArgumentException" } (4615 samples) return != null (4615 samples) =========================================================================== Variables: non_canonical_variables = 0 can_be_missing_variables = 0 canonical_variables = 0 total variables = 0 Derivation: derived_variables = 0 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: 1191 = 755 falsified_invariants = 470 non_falsified_invariants = 285 = 78 unjustified = 0 too_few_samples_invariants = 0 unjustified_invariants = 0 implied = 0 non_canonical_invariants = 0 obvious_invariants = 0 reported_invariants = 78 Exiting Daikon.