Squashed 'benchmarks/LIBRARIES/models/' changes from 1e8b77c83..240236357

240236357 Merge pull request diffblue#581 from diffblue/forejtv/simpler-file
8ef53a50a simplified constructor for java.io.File
d1c08d982 Put non-simple File.java into simple models
13c22a856 Merge pull request diffblue#578 from diffblue/jeannie/UpdateDTUversion
39202a4e5 Merge pull request diffblue#577 from diffblue/allredj/complete-linked-list-documentation
2d94c7b47 Update deeptest-utils version.
ab300bbe2 Complete documentation of LinkedList
4f77b90dd Merge pull request diffblue#544 from diffblue/collections-reverse
e78b7f02c Tests for Collections model
137622bcf Model for java/util/Collections
422197c51 Added java/util/Collections
33c1410b9 Merge pull request diffblue#576 from diffblue/smowton/admin/increase-to-depth-1600
85000a8ac Bump depth to 1600
927fef36d Merge pull request diffblue#571 from diffblue/zgoriely/linked-list-basic
8621e0d71 Addressing reviewer comments
46376144c Add tests for LinkedList methods
e4782ab96 Implement model for remaining basic LinkedList methods
0a32c4de5 Merge pull request diffblue#566 from diffblue/zgoriely/linked-list
7cc397a82 Add tests for new methods
e86ade7cb Implement methods for LinkedList
6fe84d51a Merge pull request diffblue#569 from diffblue/allredj/update-dtu-131
7bf5a1a80 Update DeepTestUtils to 1.3.1
9df72dd93 Merge pull request diffblue#560 from diffblue/zgoriely/arrays-simple-equals
78228133b Re-enable tests depending on Arrays.equals
b011e0cf5 Add Tests for Simple Arrays.equals
1a76bd166 Implement Simple Model for Arrays.equals
4d14a9a57 Merge pull request diffblue#543 from diffblue/linked-list-add-all
27c9f5da6 Merge pull request diffblue#562 from diffblue/zgoriely/arrays-equals-fix
b19e50c71 Tests for LinkedList init(c)|addAll(c)
394db6890 Modelled java/util/LinkedList.(<init>(Collection)|addAll)
950aae85c Merge pull request diffblue#565 from diffblue/zgoriely/hashset-fix
534a85708 Arrays Equals Model fix - Double and Float
74fa617b8 Fixing HashSet.addAll method
dac4774ce Merge pull request diffblue#542 from diffblue/java-util-optional
396f52c45 Tests for Optional model
d11e8faed Tidying Optional Model
3f8e7e19f Modelled java/util/Optional and java/util/function/(Supplier|Consumer)
8db4ad90e Emptied java/util/Optional and java/util/function/(Supplier|Consumer)
4c3781871 Added java/util/Optional and java/util/function/(Supplier|Consumer)
a6cbe0c51 Merge pull request diffblue#564 from diffblue/zgoriely/arrays-comparator-fix
ab7638920 Fix for Comparator sort test-gen failure
13218fec0 Merge pull request diffblue#545 from diffblue/arrays-sort
bd27eeac1 Fixing up tags in Base64 Models
14f7cda29 Tests for Arrays.sort
8c4c1c524 Model java/util/Arrays.sort
edefabb77 Empty java/util/Comparator
5c39ba9e2 Add java/util/Comparator
941eefa80 Merge pull request diffblue#563 from diffblue/allredj/travis-housekeeping
996c4aab8 Travis: Don't save html report
37640904c Travis: install gauge html-report
72330e6ce Linting
3a97f9fa5 Travis: Remove unneeded addon installs
c6d77308b Merge pull request diffblue#556 from diffblue/allredj/update-modeltests-gitignore
11409e1aa Merge pull request diffblue#375 from diffblue/jeannie/setTimeZoneAndOthers
6b4808330 Update .class files
7deac9024 Tag all failing tests with appropriate ticket no.
c832fba9b Mock Calendar and fix some things in the model
726558344 Re-enable fastTime field in Date model
e5f994525 Updates CProver.nondet methods for not modelled functions.
d43a366cf Updates documentation in javadocs for java.util.Date
e65c0f6aa Tests java.text.SimpleDateFormat
798fd0b5e Models java.text.SimpleDateFormat
0499abc91 Models java.text.DateFormat getTimeZone() and setTimeZone()
6d96405f7 Marks all methods as notModelled() in Format classes
477fcc92d Initial commit for java.text.Format, DateFormat and SimpleDateFormat models.
efd6fe8e3 Tests java.util.GregorianCalendar
e4e0d40ff Tests java.util.Calendar
b87c250f8 Models java.util.GregorianCalendar()
e03f25170 Marks all methods as notModelled() for java.util.GregorianCalendar
ce2549199 Initial commit for java.util.GregorianCalendar
9d85399fa Models java.util.Calendar
d0d31e9ed Marks all methods as notModelled() in java.util.Calendar
71d877078 Initial commit for java.util.Calendar
149aa4da6 Models ZoneInfo getRawOffset() and uses it for getOffset()
8d9a9ac67 Merge pull request diffblue#561 from diffblue/zgoriely/model-test-generator-improvement
0a7e92e0d Fixing a couple bugs in model test generator
7ce6d62a9 Merge pull request diffblue#558 from diffblue/antonia/appendable-annotation
562ffb424 Merge pull request diffblue#559 from diffblue/antonia/enable-TG-3905-tests
e32331aa9 Merge pull request diffblue#555 from diffblue/zgoriely/arrays-fill
4d1111fa6 Enable tests for TG-3905
fb5308932 Move Appendable test to appropriate folder
2149e3ad8 Pick StringBuilder as an Appendable implementation
9b2a4a30a Arrays fill model
1fcddca3f Merge pull request diffblue#557 from diffblue/zgoriely/arrays-equals
0ef93d6dd Updated test class names and test method names
c037628e6 Re-Enabling tests that rely on Arrays.equals
8329b761d Merge pull request diffblue#541 from diffblue/emptier-script
bc31d0bdf Merge pull request diffblue#551 from diffblue/zgoriely/arrays-equals
f9f914b8f Update modelTests .gitignore
8469f6c28 Tests for Arrays.equals methods
2eef3d595 Model for Arrays.equals methods
bf7b6f191 Merge pull request diffblue#550 from diffblue/cesaro/java-sync-fix
1a93b39d5 Re-enable tests in PushbackReader.spec, see e21b471
dd8689737 Merge pull request diffblue#547 from diffblue/svorenova/enable_tests_tg3514
5fd67cde8 Use Gauge tear-down steps
e1b2b5241 Update ticket number for disabled tests for mocking with inheritance
9ee355cd5 Merge pull request diffblue#554 from diffblue/allredj/travis-use-obfuscated-build
5fee9930a Use obfuscated test-gen build in models-library
7502e471d Merge pull request diffblue#540 from diffblue/java-concurrency-synchronization-models
e21b471ab Temporary disabled a number of tests in 'PushbackReader.spec'
7f1eb804d Emptier script
d0b941b83 Changes to support PR cbmc#2280
5915ce44d Merge pull request diffblue#536 from diffblue/antonia/unnecessary-gauge-steps
e8b4888f9 Merge pull request diffblue#538 from diffblue/bugfix/TG-1888/put-tests-in-appropriate-packages
8fd5af6eb Tidy up Verify steps in spec files
da8b4ac38 Don't use java or javax packages
4ec167eec Adding test for checking getPackageFromMethod
91ea20ce3 Put tests in to the package that the function under test is in
6e6b59698 Merge pull request diffblue#533 from diffblue/allredj/testrunner-start-with-unwind-2
57b73a8b0 Merge pull request diffblue#504 from diffblue/forejtv/simple-base64
8907ffd20 Simplified model for Base64
8d521d65d Skip some tests that fail due to TG-3981
35621a7e9 Merge pull request diffblue#530 from diffblue/romain/string-init-charset
efebf5cec Use CProverString.substring
d929a005f Use a reversible version of getBytes
c1e020c3d Add test for constructor from byte[] and charset
07004ec1b Model for String constructor from byte[], charset
136326682 Use equality on name for charsets
e45df98d0 Use CProverString.equals instead of ==
61c713714 Define a CProverString.equals function
c0ef4fe7d Merge pull request diffblue#519 from diffblue/allredj/linkedhashset
338a1cdfc Merge pull request diffblue#528 from diffblue/allredj/simple-linkedhashset
cf1f27e96 Added original model for Base64
8676ea6b5 Merge pull request diffblue#535 from diffblue/antonia/stringreader-optimisations
0f051858c Tests for LinkedHashSet (simple model)
d964fa763 Make HashSet fields package-private (simple model)
beaf7d1bf Simple model for LinkedHashSet
01e2b787c Import LinkedHashSet.java from JDK
400db2ba0 Add missing Diffblue Javadoc tags
f50914877 Use more efficient charAt in StringReader
6a60301b0 Clarify differences from JDK StringReader
c95f30f27 Load a StringReader when loading PushbackReader
8290e5b13 Start generating tests with unwind 2
8861b24f1 Tests for LinkedHashSet
81ca53b05 Model for LinkedHashSet
5d9420c1d Import LinkedHashSet.java from JDK
4e22d539b TestRunner: Factor out debug output
9616e1769 Merge pull request diffblue#531 from diffblue/romain/nondet-initialize-file
8553bf0e5 Activate cproverNondetInitialize for file
c0d1c05dc Merge pull request diffblue#532 from diffblue/allredj/fix-stringbuffer-append
71e3b0788 Merge pull request diffblue#534 from diffblue/allredj/use-fornotmodelled-in-simple-models-2
c0f10640b Merge pull request #529 from diffblue/jeannie/TestRunnerImportsUpdate
65b68beeb Merge pull request diffblue#516 from diffblue/allredj/exhibit-mocking-bug-with-inheritance
2588b96c0 Use appropriate header for tests.
fc3f1c53a Use short name for annotation in TestRunner.
0e9da3a50 Avoid using nondet statements where possible
a20e778b4 Build modelling utils with "package"
753eea477 Copy over cprover package from standard models
67199cdb2 Fix StringBuffer.append
3f2ac3406 Disable tests that suffer from TG-3514
d2dabe327 Make tests sensitive to mocking problems
532d146f3 Merge pull request diffblue#515 from diffblue/antonia/implement-annotation
0048a020c Add tests for classes given in annotations
2e6182b10 Annotate common abstract classes
39f6d72f4 Add java.lang.Appendable interface
bc383f3b2 Add java.io.Flushable interface
83dffab13 Add java.lang.AutoCloseable interface
18bd2e55b Add java.io.Closeable interface
f37ca90df Add java.lang.Readable interface
a8369c332 Add implementation annotation to simple models
d06449814 Show "Preferred..." annotations in Javadoc

git-subtree-dir: benchmarks/LIBRARIES/models
git-subtree-split: 240236357fc9fb1cb87bf5adacaa1b27786ff84b

Author: smowton

.travis.yml

@@ -4,14 +4,6 @@ os: linux
 sudo: required
 dist: trusty
 
-addons:
-  apt:
-    sources:
-      - ubuntu-toolchain-r-test
-    packages:
-      - g++-5
-      - elinks
-
 cache:
   directories:
   - "$HOME/google-cloud-sdk/"
@@ -34,7 +26,7 @@ before_install:
 
 install:
   # Check that modelling utilities are building and run unit tests
-  - mvn -f scripts/modelling-utils/pom.xml install
+  - mvn -f scripts/modelling-utils/pom.xml package
   # First build simple models.
   - cd model-simple
   - mvn package
@@ -43,7 +35,7 @@ install:
   - cd model
   - mvn package
   - cd modelTests
-  - gsutil cp gs://travis-artifacts/test-gen/${TEST_GEN_BUILD:-"latest-develop-ubuntu"}.tar.gz cbmc-testgen-latest.tar.gz
+  - gsutil cp gs://travis-artifacts/test-gen/${TEST_GEN_BUILD:-"latest-develop-static"}.tar.gz cbmc-testgen-latest.tar.gz
   - tar -zxvf cbmc-testgen-latest.tar.gz -C under_test
   - mv ../target/models.jar under_test
   - mv ../../model-simple/target/models-simple-overlay.jar under_test
@@ -53,8 +45,7 @@ install:
   - sudo apt-get update
   - sudo apt-get install gauge
   - gauge install java
-    # Temporarily disable html-report (installing this plugin might not be required anyway)
-    # gauge install html-report
+  - gauge install html-report
   - gauge config plugin_kill_timeout 20000
   - gauge telemetry off
   - export MAVEN_OPTS="-XX:+TieredCompilation -XX:TieredStopAtLevel=1"
@@ -69,20 +60,6 @@ before_cache:
     # Upgrade pyopenssl (signurl prereq) via pip
   - sudo pip install pyopenssl --upgrade
 
-  - |
-    # Save the html report
-    ( set -euo pipefail
-      if [[ -d reports/html-report ]]
-      then
-        REPORT_FILE=html-report-$(git describe --tags --always).tar.gz
-        tar -zcvf ${REPORT_FILE} reports/html-report
-        gsutil -h "Content-Disposition:attachment; filename=models-${TRAVIS_BUILD_NUMBER}-report.tar.gz" \
-          cp ${REPORT_FILE} gs://travis-artifacts/models-library/models-${TRAVIS_BUILD_NUMBER}-report.tar.gz
-        echo Link to html report:
-        echo "https://console.cloud.google.com/storage/browser/travis-artifacts/models-library?project=diffblue-cr&prefix=models-${TRAVIS_BUILD_NUMBER}"
-      fi
-    )
-
 after_success:
   - |
     set -euo pipefail
@@ -118,4 +95,3 @@ notifications:
     on_start: never
     on_cancel: never
     on_error: always
-    

model-simple/src/main/java/com/diffblue/annotation/PreferredConcreteImplementation.java

@@ -0,0 +1,13 @@
+package com.diffblue.annotation;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Target;
+
+@Documented
+@Target(ElementType.TYPE)
+public @interface PreferredConcreteImplementation {
+
+    Class<?> value();
+
+}