Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix local var frame #185

Merged
merged 16 commits into from
Aug 22, 2016
Merged

Fix local var frame #185

merged 16 commits into from
Aug 22, 2016

Conversation

mgudemann
Copy link
Contributor

@mgudemann mgudemann commented Jul 25, 2016

This corrects local variable usage which depends on local frames. If present, the LocalVarTable contains information about the local variable scope. This scope is defined for a variable with index n via start_pc and length.

Instead of variablet, the expanding_vector variables now contains a std::vector<variablet> for each index. For an instruction at address a, the corresponding variable is searched as the valid variable for the frame start_pc <= a + length(instruction) < start_pc + length.

resolve #177

@mgudemann
Copy link
Contributor Author

The change also parses and stores the StackMapTable code attribute, but this is not necessary and could be removed.

@mgudemann
Copy link
Contributor Author

Is not yet correctly implemented, fails e.g. if indices 0,1,2,4 are in the local variable table, but 3 is unnamed local var.

@kroening kroening self-assigned this Aug 2, 2016
@mgudemann
Copy link
Contributor Author

should be correct now, partially fixes #162

void java_bytecode_parsert::read_verification_type_info(methodt::verification_type_infot& v)
{
u1 tag = read_u1();
if(tag == 0)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks like a use-case for switch(tag){ ... }

@kroening
Copy link
Member

Could you do a rebase, please?

@mgudemann
Copy link
Contributor Author

should be ok

@kroening kroening merged commit 61d4157 into diffblue:master Aug 22, 2016
@mgudemann mgudemann deleted the fix_local_var_frame branch August 22, 2016 14:07
smowton pushed a commit to smowton/cbmc that referenced this pull request May 9, 2018
…ction-loading

SEC-20: Lazy function loading
smowton pushed a commit to smowton/cbmc that referenced this pull request May 9, 2018
cc8db21 Merge pull request diffblue#367 from diffblue/allredj/optional-test-runner-timeout
54f278e Merge pull request diffblue#355 from diffblue/allredj/string-exceptions
80e17d8 Add tests for StringBuffer exceptions
50fe786 Add tests for StringBuilder exceptions
403bb47 Add tests for String exceptions
5f20fa8 Add exceptions to String models
f06c5dd Merge pull request diffblue#353 from diffblue/allredj/SecureRandom
2357fb1 TestRunner: Set global process timeout to 500 secs
a1e9bc0 TestRunner: Add optional timeout
d2d0e1e TestRunner: Prevent deadlock on output streams
8c2f6ec Merge pull request diffblue#363 from diffblue/antonia/public-static-fields
b0d1038 Allow custom javadoc tags in all places in models
91b51cb Add new restriction on static fields to readme
5d5237b Update 'Writing models' section in readme
cea6f14 Model for SecureRandom
53b572b Force SecureRandom mock in TestRunner
1c50faa Empty Random and SecureRandom models
7653be1 Import Random and SecureRandom from JDK
79d7e50 Update File javadoc to take bugs into account
0bd4ffb Add tests for File fields
5f714c8 Prepare File.spec for new test format
419bb11 Enable public static fields in File and String
ac47de9 Merge pull request diffblue#361 from diffblue/antonia/public-System-fields
31c934c Add tests for public static fields of System
1489356 Prepare existing System tests for new format
2b4f4a8 Re-enable out, in and err fields in System model
c8bd0eb Merge pull request diffblue#362 from diffblue/jeannie/DisableTestsDueToTG2098
2b183fa Updates javadocs for java.util.Properties for TG-2098.
da777b5 Renames spec files to remove spaces and make consistent.
7005075 Disables tests in java.util.Properties due to TG-2098
5c9652b Merge pull request diffblue#360 from diffblue/antonia/gcloud-comment
bbfa9f9 Merge pull request diffblue#354 from diffblue/antonia/model-common-Date-methods
6ddfee0 Add ticket number to commented out gcloud line
c2f5bf5 Add @diffblue.mock java tag
8c032d8 Delete legacy Date tests
fa15801 Add tests for Date
1f7a722 Mock Date in TestRunner
cdd4037 Simple model for Date with constant timestamp
e0b859f Copy jdk version of Date
af0c931 Merge pull request diffblue#358 from diffblue/allredj/tmp-gcloud-fix
6c3baf8 Temporarily disable GCloud update
e188f92 Merge pull request diffblue#349 from diffblue/allredj/gauge-dump-mvn-error-to-stdout
d8f016b Gauge: Dump mvn error message into stdout
7137e47 Merge pull request diffblue#324 from diffblue/feature/TG-2020/deeptest-utils-update
216248a Updating runner to use the new deeptest-utils repo
0aeeac3 Merge pull request diffblue#352 from diffblue/allredj/buffered-writer-missing-null-check
67b76b1 Fix missing null check in BufferedWriter's nondet-init
b0a3882 Merge pull request diffblue#350 from diffblue/jeannie/DisableSometimesFailingHashtableTest
b8cf2df Disables tests that use nondet key/value for Hashtable due to TG-2098.
0714583 Adding a noop for Hashtable tests (no testing scope change).
459a3ce Merge pull request diffblue#337 from diffblue/jeannie/EnableHashtablePropertiesTests
5918596 Enables tests for Properties and Hashtable that require custom initialisers.
8c0b6ab Merge pull request diffblue#348 from diffblue/antonia/disable-TG-2098-tests
1ecfffe Merge pull request diffblue#347 from diffblue/allredj/lower-initial-capacity-bound
8b5e399 Disable test with varying running time
2e75972 Lower max initialCapacity to prevent JVM runtime failures
82cf0a8 Merge pull request diffblue#328 from diffblue/jeannie/Properties
85c5380 Merge pull request diffblue#346 from diffblue/jeannie/DisableFailingTestsDueToTG2356
df669a7 Adds tests for java.util.Properties model. TG-2067
9a840e5 Adds javadocs for java.util.Properties model; TG-2067.
b1c480c Adds model for java.util.Properties. TG-2067
546c4b8 Marks all methods as notModelled(). TG-2067
15f7a4f Makes initial commit for Properties.java. TG-2067
453919a Updates javadocs for java.util.Arrays.
c054c05 Merge pull request diffblue#345 from diffblue/antonia/mockito-powermock-versions
3b37fe6 Disabling tests that fail due to TG-2356 / TG-1404.
ce082f6 Update remaining pom files into new format
57dcf33 Use compatible Mockito and Powermock versions
226fa3e Merge pull request diffblue#340 from diffblue/romain/QA_HashSet_iterator
c38cac1 Level1 tests for iterators on HashSets
ebd5043 Merge pull request diffblue#344 from diffblue/jeannie/DisableHashSetTests
5b79203 Disables failing tests due to TG-2327.
525a731 Merge pull request diffblue#343 from diffblue/romain/fix-test-clone-arraylist
673792f Deactivate test with HashSet of ArrayList
aa1ca7e Merge pull request diffblue#339 from diffblue/jeannie/FixCustomEqualsHashMap
acfc29b Merge pull request diffblue#331 from diffblue/romain/regression/TG-1245
7f7d3ff Merge pull request diffblue#335 from diffblue/romain/QA_HashSet_clone
5c9cd0f Disables HashMap test regarding TG-2315.
b751a09 Fixes HashMap test regarding TG-2018.
12336a7 Level 1 tests for HashSet.clone
19a38e8 Regression test for TG-1245 (Object.getClass)
992437b Merge pull request diffblue#341 from diffblue/romain/update-class-files
38be638 Correction of a test
6bfc2b2 Forgotten class file
18d1cc0 Merge pull request diffblue#319 from diffblue/romain/QA-HashSet
6ba37d1 Merge pull request diffblue#338 from diffblue/bugfix/TG1877-Bugfix-regressiontest
1d596b2 Merge pull request diffblue#327 from diffblue/jeannie/Hashtable
f682e28 Tag long test of HashSet
080b6aa Remove tests duplicating L1Constructor_Collection
89643ba Level 1 test - HashSet constructor and class tests
9f83291 Remove old tests from ArrayList.spec
3822552 Add tests for TG-1877 to the new bug test suite
8a4e6a8 Adds tests for Hashtable. TG-2176
5c3f51d Merge pull request diffblue#326 from diffblue/allredj/Update-test-header-in-TestRunner
72a9f72 Adds model for Hashtable. TG-2176
d56fbbd Marks all methods as notModelled(). TG-2176
4f0a4ae Make initial commit for Hashtable.java and Dictionary.java. TG-2176
3ab91b8 Merge pull request diffblue#336 from diffblue/antonia/disable-Write12-test
5a7e84a Update test headers according to Platform
27cf91b Move maven configs to master-pom.xml
9907cc2 Merge pull request diffblue#332 from diffblue/feature/TG-2020/centralise-artifact-name
910a6a6 Tag ByteArrayOutputStream.Write12 as 'long'
23dde95 Updating POM file to use property in the master-pom
92b1dca Adding a master POM to specify all dependencies in one place
857bd3c Merge pull request diffblue#333 from diffblue/forejtv/remove-some-codeowners
a475e10 Merge pull request diffblue#330 from diffblue/allredj/enable-TG-656-tests
25ecdfe Remove forejtv and peterschrammel from code owners
1145774 Merge pull request diffblue#325 from diffblue/antonia/HashMap-inner-classes
326482a Clean up model methods spec file
fdf6041 [TG-656] Enable passing exception tests
b029c6f Delete old iterator tests
515f163 Add tests for HashMap$Values
edbe13f Add tests for HashMap$KeySet
7037882 Add tests for HashMap$EntrySet
4a77660 Override Values.remove() in model
0b8cac8 Improve running time of remove() methods
e57e731 Small fixes for null cases in HashMap$EntrySet
b411ef3 Merge pull request diffblue#322 from diffblue/antonia/method-body-tests
e808809 Merge pull request diffblue#323 from diffblue/romain/script-generalize-test
3f1eb24 Put method body tests into new format
e90f611 Update powermock dependencies in new pom.xml
ae460cd Create folder for method body Maven project
0ad8972 Move known-bug method body tests to end of file
b71f824 Move method body tests into separate file
af9f9a5 Merge pull request diffblue#311 from diffblue/allredj/Testrunner-message-on-missing-method
0a70f78 Script specializing method to different types
7f5d25b Improve TestRunner failure messages
4b7c200 Merge pull request diffblue#315 from diffblue/justin/alTestTidyup
9d005ba Addressing review comments progress 2
7fc3602 Merge pull request diffblue#318 from diffblue/allredj/QA-HashMap
4bcc63f Add tests in new format
4c74354 Add constraints on constructors args
f623a6a Merge pull request diffblue#321 from diffblue/allredj/add-constraints-on-capacity
0aa1cde Add constraints on constructors args
85da460 Merge pull request diffblue#320 from diffblue/antonia/prevent-Travis-debug-mode-crashes
c01c883 Addressing review comments progress 1
f965eae Prevent Travis build crashes with set +e
2f5c657 Add and refactor ArrayList tests into new format
a144089 Merge pull request diffblue#317 from diffblue/antonia/disable-ArrayList-test-TG-2098
44b865e Disable ArrayList test affected by TG-2098
950b3cb Merge pull request diffblue#316 from diffblue/antonia/enable-HashSet-tests
52c8aa4 Re-enable HashSet tests for new model/constructor
c1ac42a Merge pull request diffblue#308 from diffblue/antonia/model-HashSet-using-array-field
5f1422f Temporarily disable HashSet tests
898eceb Update limits on method calls in HashSet javadoc
0488845 Update HashSet.spec and limits on number of calls
6ba92bd Add test for HashSet.clone()
03013dc Add new HashSet test using Collection constructor
12b741e Model HashSet using an array instead of a HashMap
1e16b87 Merge pull request diffblue#314 from diffblue/lajw/array-list-arrays-tests
a333fd5 Add test for ArrayList of Arrays
bbbece5 Merge pull request diffblue#312 from diffblue/allredj/testrunner-lush-specs
ac16beb Merge pull request diffblue#306 from diffblue/doc/update-string-doc-TG-1724
75934df Merge pull request diffblue#313 from diffblue/allredj/travis-skip-long-future
019806d Skip long and future tests in Travis
c15a87e TestRunner: Add functionality to simplify specs
dfcfee7 Typo in StringBuilder.java comment
3a84d72 Correcting exception documentation in String.java
b573c7a Document support of String(Builder|Buffer) Classes
4756a96 Document missing exception throws in StringBuffer
40bed6f Document missing exception throws in String model
679d3a3 Merge pull request diffblue#307 from diffblue/jeannie/SystemArrayCopyQA
0fc655c Puts tests into QA format for System.arraycopy.
1adfb51 Merge pull request diffblue#310 from diffblue/jeannie/UpdateGitIgnore
0dc376d Removes tika from the .gitignore file because it was removed.
025d1b2 Removes reference to tika tests in .travis.yml file.
0bf6558 Reinstates .gitignore file after conflict during rebase.
f574057 Merge pull request diffblue#302 from diffblue/justin/newqascript
ecb6d38 Address PR review comments
eedf614 Add bash script that automates some QA workflows along with usage instructions
fc95298 Merge pull request diffblue#304 from diffblue/test/reactivate-tests-deactivated-by-PR301
f2f6786 Revert "Temporarily deactivate a test"
3b40452 Adds tests for StringBuilder append(Object). These are all currently disabled.
07af9e7 Print more useful output about discarded tests
270457d Print more output about line errors
29defd6 Group java.util import statements in TestRunner
16fa02c Temporarily deactivate a test
beab774 Correct test charAt_Fail
f9135af Replace charAt occurences by CProverString.charAt
30df36c Use CProverString to model String.substring
16172f9 Use CProverString.charAt to model String.charAt
68675f7 Add a CProverString class to use internal methods
453a262 Use goal coverage in TestRunner "lines" tests
dc77ad4 Add doc about travis error report on README
6728da0 Don't fail if report is not present
51f95f4 Enable test that was forgotten in PR 295
cea6c05 Add test for floating point precision of floats in custom initalizers
61fb30c Disables test that was randomly failing CI. TG-1891
d9e2c34 Adds more tests for HashMap with generics. TG-1401
a28c379 Adds documentation for HashMap.
646cdb0 Add tests for generics support of ArrayList
67f99ad Make imports and linebreaks consistent in tests
0678c26 Adds more tests for HashSet, namely for custom initialisers and addAll.
c3ee8d3 Adds addAll function separately. Adds documentation.
1fa7e5c Increase Maven compilation speed
66cb693 Factor test verification
2902bac Add error message when bad Maven dir is given
4317579 Compress and save html report on each ML build
b660af6 Adding CProver.notModelled calls in StringBuffer
30eaf5f Add diffblue tags to StringBuffer model
34b607b Comment on internal models of StringBuffer methods
2db6dc5 Moving "modelled internally" comments in methods
ea1b900 Adding diffblue tags to StringBuilder methods
3d64388 Marking notModelled StringBuilder methods
b8d5101 Put original String.contentEquals code in comment
d1d074d Correct model of toUpperCase(Locale)
87dea39 Correct comments for String.getChars
dcb3183 Add untested and todo tags to overview.html
c74e3de Add untested and todo tags to Readme
f90ce62 Comment unused imports
0769e20 Commenting out unused private methods
8366ca7 Marking not modelled String methods
772ce3d Adding tags to method documentations
88b4bda Add diffblue.todo and untested tags
16e957e Modify command to increase gauge plugin timeout
05c4d2e Update README.md
8e5e31a Convert "verify" tests to "generate" tests in specs
e3fe09d Add steps for test generation only
dabdc1a Refactor test verification steps
393eeba Add new Gauge step "Verify Tests in Maven project"
87eb11a Modify spec files for new mvn setup command
d8808f7 Modify Maven setup Gauge command
0da5a56 Typo in StringBuilder model
e02661c Reintroduce doc and code in StringBuffer model
94a8ebf Reintroduce doc and code in StringBuilder
d2b955b Comment about utility functions specific to models
93579f8 Reintroduce String Library documentation and code
54089f8 Enable test verification for BitSet
913ac12 Implements iterator() method for Arrays$ArrayList inner class (Arrays.asList). TG-1727
e08d030 Add test for TG-1786
1fac27d Workaround for bug TG-1786 in HashMap model
f9d5b91 Disables BitSet functional test for clear. TG-1775
38dc647 Disables functional test for ArrayList iterator. TG-1775
1a7e4ac Add verification of tests for BitSet
c1ff99f Model for BitSet
485339a Adding bitset from JDK
3092f08 Add test for handling user-defined type as an element of ArrayList
d93f9a6 verification of tests for DataInputStream
efc186b model for DataInputStream
527d82a JDK version of DataInputStream
811689f java.io.DataInput interface from JDK
8287a56 Marking FilterInputStream as supported, and adding cproverNondetInitialize
f63aa29 JDK version of FilterInputStream
43808d8 Keep all generated test files
a35c96e Add doc to Integer.java
fd68471 Add doc to Boolean.java
cba6e76 Implements model for Arrays.asList()
7d3c23e Marking methods as notModelled() in Arrays.java.
0b30e9b Initial commit for Arrays class file.
19f106a Disables test with Gauge issue on TravisCI.
c5b89f6 Enables tests for HashMap/HashSet as argument or return value.
b2bd7f0 Enables tests for HashMap/HashSet as argument or return value.
4468773 Activate ArrayList return value tests
c0d9006 Add ArrayList test that checks for side effects
aaec548 Comment out custom ArrayList model variable
838f304 Disable test that randomly fails on Travis
9a0f626 Add ArrayList and HashMap constraints for modCount
ee6f284 Add tests for return value check of ArrayList
85592d9 Check for "tested" instead of "covered"
92500be Use new platform parameter in TestRunner.java
3399a22 Modify test to match HashSet's NondetInitialize
ba008ab Add NondetInitialize constraint to Class model
52880ee Add constraint in HashSet to speed up test gen
37c789a Disable PutAllAndGet.test for HashMap
71fe858 Replace validate for HashSet
27e58e7 Replace validate for HashMap
6ed6a99 Replace validate for ArrayList and AbstractList
d38044c Replace validate for BufferedReader and related
a2e6cd5 Enable ByteArrayOutputStream's Write12.test
116d10f Replace validate for ByteArrayOutputStream
1c8e115 Enable PrintStream's Depth.test
269bb28 Replace validate for PrintStream + related classes
09fd660 Correct getPrimitiveClass for String
140e8fa Add tests for Class.toString
1bc6127 Correct Class.isPrimitive model
1fe9d8d Adding Java.lang.Math test scenarios. (diffblue#233)
93ec334 Skip a test until models-library#261 is merged
da5e93b Enables tests for HashSet that require Float and Double equals().
928b4e2 Adds tests for equals() in Double and Float models.
020e400 Implements method equals() in Double and Float models.
e7b4b1e Add new test for custom class without nested class
08affc8 Rename CustomClass to StaticClass, enable test
933a99a Update TestRunner paths
c1c7ed0 Remove redundant test ArrayListObjectToBoolean
ebaa2c2 Renamed tests to more informative filenames
80570cb Test for ArrayList argument possibly null
e5c0330 Additional tests for ArrayList as argument TG-1230
79e86ab Address TODOs that depend on custom initialisers
3492363 Improves constructor that takes collection. Adds iterator, toArray methods.
2ff7175 Adds tests for HashSet.
fcf24d4 Adds model for HashSet.
299851c Initial commit for HashSet model.
4beb116 Increase gauge plugin timeout
3c28f8b Mark test for constructor body as known-bug
97f5df3 Small fixes in HashMap
67f6479 Mark HashMap-as-argument tests as known-bug
69a2d78 Add CODEOWNERS
49f7149 Update README.md
56193b3 Split String test_data file
e61e374 Enable ArrayList tests
07c84df Run tests in verbose mode
e05c5de Add test for arraycopy with ArrayStoreException
9485f07 Add test for arraycopy on itself
0ba83ef Rename test methods as "test"
b761e19 Split tests: 1 method per java file
d4606d6 Add knownbug test for System.arraycopy of char[]
7955d75 Add System.arraycopy test specifications
965045e Add test and test class file for System.arraycopy
34aba57 Model for System.arraycopy
e7df5a9 TG-1394 Setup javadoc
29563a9 All add package information from original JDK
301c209 Correct line numbers covered in OSName2
080ee25 Activate tests for System.getProperty
fa5178b Updates .spec file for StringReaderRead4.java test failing CI.
ca216e0 Mark HashMapValues.test as known-bug
c8aaa80 Add tests for HashMap
acfb0d2 Model for HashMap
629a7e7 Copy map classes and interfaces from jdk
478f28f Test for NPE in getBytes with string argument
cd8ce59 Throw NullPointerException in getBytes of null
2be372a Use develop branch of test-gen in models-lib CI
1e43155 Adds readline() method to BufferedReader model.
15a3e8c Simplifies some code blocks. Adds back in synchronized blocks for Reader, StringReader, BufferedReader.
89122d7 StringReader working apart from next side affect check issue.
76e950b Adding in recompiled SimpleNPE.class.
c8abf9b Removing ambiguously-cased classes for SimpleNPE.class
ce7f8bb Small optimisation in constructor
a7263fe Small fix for an assume statement that wasn't used
da61bb4 Change Object[] to E[] so cbmc will recognise type
ee1c756 Remove documention of plug from Readme.md
2f442f2 Test for getBytes without arguments
be9139e Model for getBytes with no argument
14aa8fc Split Init.java test_data files into separate files
d2aa1c4 Rename specs/jdk to specs/java
22f4cbe Rename test_data/java-library to test_data/functional
2b95dd9 Rename test_data/init to test_data/maven
611e74b Update .gitignore files
ffd6fc9 Move init specs to their repsective location in specs/jdk
faf8c89 Move specs/util into specs/jdk
1526ee5 Remove plug
4571e79 Add a model for String initialization from array
3ce365e Style: delete trailing whitespaces
19c195c Model for String.toCharArray
1e435df Avoid Strings in ArrayList test
f747e81 Enable previously disabled assertion tests
899974e Add tests for most common ArrayList methods
35d05d8 Model for ArrayList and superclasses
7d1ac36 Copy list classes and interfaces from jdk
6259ae1 Mark as knownbug all tests with System.getProperty
87907c8 Update Gauge Maven plugin version in pom.xml
330f242 Add test for getBytes(Charset) with tag knownbug
c561bf3 Adding tests for getBytes
fedcb81 Style: untabify
babfff8 New version of getBytes without static members
d10408c Marking test for System.getProperty as knownbug
7712f7b Adding models for BufferedReader close() and constructors.
c653b66 Removes File(URI) constructor because there is no URI model. Reinstates NullPointerExceptions.
d5a9ad4 Updates models for BufferedReader as notModelled and Reader to model only first constructor.
d4b5231 Add tests for System.exit and System.getProperty
282c935 Model for System: exit and (partial) getProperty
def14b6 Copied System.java from jdk
7e450e7 Model for toString for subclasses of Throwable
d5edf8d Tests for Throwable.toString
071c234 Updated model for Throwable and Exception
4778547 Add line coverage functionality to TestRunner
c79fcbd Remove bad line in spec file
8675619 Adds models for Math.max and Math.min TG-836
4a75655 Initial commit for Math model
f9f94ea Removing tika tests from Travis.
08cc1ff Recompile all test java files as some of the class files were found to be out-of-date
f82552c Run tika tests in travis
f1633fd Tag functions with low coverage as known-bug
ae1f545 Modify TestRunner to detect incomplete coverage
e13ed94 Use CProver implementation in String.replace for Char Sequences
b723273 Java util arrays (diffblue#198)
4397193 Enable skipped tests for ByteArrayOutputStream
1f2b1ef Further simplified the File model so tests pass
882497f Updates models for four File constructors. TG-777
0d04723 Initial commit for File model.
6cdba8d Updated setup script
d401c31 Use cprover functions in long-to-string conversions
aad3499 Tests for new methods in PrintStream
dbf6758 Model for print(ln)(Object) and printf
77fb2ba Cleanup String.java model
51b3144 Update TestRunner.java to use new platform values
443a2cb Add tests for some methods in Character.java
8d9cc57 Model for Character.valueOf
4a4e5fc Add construction tests for ByteArrayOutputStream
f9a7a13 Add constraints to ByteArrayOutputStream
20d14e1 Linting
7ceb450 Adding Java.lang.Math Test scenarios. (diffblue#188)
1597eab Remove unused makefile
0632300 Small improvements to TestRunner
4cd5a90 Merge pull request diffblue#182 from diffblue/allredj/update-testrunner-options
dbaf047 Update Gauge TestRunner options
5c94e8d Skip tests that fail with new platform options
8eeea1e Disable an invalid test
a51c521 Merge pull request diffblue#183 from diffblue/antonia/printstream
893e47b Add tests for PrintStream.print(ln) functions
0d1ddc7 Added empty CharArrayWriter model with constraints
630decb Added empty StreamEncoder model with constraints
40c6cf8 Added constraints for Writer objects
9025e60 Update spec file for PrintStream
e91c9b3 Empty model for OutputStreamWriter with constraints
fb44939 Copy OutputStreamWriter.java from jdk
aa37293 Empty model for FilterOutputStream
ce0a697 Copy FilterOutputStream.java from jdk
4607f8a Empty model for BufferedWriter with constraints
6ac4952 Copy BufferedWriter.java from jdk
1dce5e9 Empty model for Writer
f25b1f0 Copy Writer.java from jdk
1ea396a Model PrintStream.print(ln)
b369b15 Copy PrintStream.java from jdk
6b17714 Merge pull request diffblue#186 from diffblue/lucas/fix/IntegerLong
480f37a Removed the toUnsignedString0 method from the Integer class
0df6efe Merge pull request diffblue#185 from diffblue/lucas/simplify/IntegerLong
0b038d3 The toString methods are implemented internally in cbmc
b10f24a Merge pull request diffblue#178 from diffblue/reuk/multiple-tests-in-class
eb87853 Allow several tests in generated_test class
7e4e92b Merge pull request diffblue#177 from diffblue/reuk/fix-travis
bc4ed2b Fix pip usages in Travis
8ed0590 Fix Travis build issues

git-subtree-dir: benchmarks/LIBRARIES/models
git-subtree-split: cc8db21ff99d5bddf4eb55004b32708129d25d53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants