…6357 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

error failed to add string literal symbol to symbol table on CBMC/java #504

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

error `failed to add string literal symbol to symbol table` on CBMC/java #504