Fix a bug in the bitwise encoding of float to int casting. #359
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
martin-cs
force-pushed
the
fix-cast-float-to-int
branch
from
3c4ee9b to
e23b5ff
Compare
|
Linting failures are all pre-existing and I didn't think fixing them would be appropriate in this patch. @peterschrammel we need this for SV-COMP. |
martin-cs
force-pushed
the
fix-cast-float-to-int
branch
from
e23b5ff to
2186bcf
Compare
This affects cases when a floating-point number is cast to an integer which is longer than the significand of the float and the exponent is greater than the length of the significand. This includes float -> (u)int32_t and double -> (u)int64_t. These were incorrectly converted to 0.
martin-cs
force-pushed
the
fix-cast-float-to-int
branch
from
2186bcf to
066829c
Compare
smowton
pushed a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
67c80fc Merge pull request diffblue#394 from diffblue/jeannie/LinkedHashMapIterators 6667484 Tests that the iteration order is correct. 38301ea Tests other methods and constructor in LinkedHashMap f795b3d Models other methods in LinkedHashMap. 25773a6 Tests entrySet(), keySet() and values() in LinkedHashMap ee8cfad Models keySet(), entrySet() and values() in LinkedHashMap. 02c8271 Merge pull request diffblue#393 from diffblue/jeannie/UpdateReadMeForSpec 81460d3 Update readme.md to include new style for specs 9efcce3 Merge pull request diffblue#396 from diffblue/antonia/clean-up-for-TG-1081 c902c03 Merge pull request diffblue#397 from diffblue/jeannie/ForgotAppendObjectDocs 772a977 Merge pull request diffblue#390 from diffblue/antonia/enable-fixed-tests 5bef2ff Merge pull request diffblue#398 from diffblue/antonia/ticket-references-bugfix ed1dca2 Merge pull request diffblue#395 from diffblue/allredj/disable-tests-failing-on-tg2717 c07841d Add more tests for String.getBytes(Charset) d568e47 Fix array index bug in String.getBytesUTF_16 2218407 Model String.getBytes(Charset) 9c3a8bc Clarify difference of String.getBytes from JDK cf1c23b Merge the two active scenarios in String.spec dd5d2d9 Remove support_v1 tag from String specs 5f9a7e1 Split String tests into Level 0 and Level 1+ f2877b9 Enable Class test that was blocked by TG-1081 034f3e0 Remove reference to TG-1081 from File model 43afde7 Force static initialiser for File model d95ff9e Remove reference to fixed bug from Date model 0807806 Remove references to fixed bugs from Arrays model cde4085 Remove references to fixed bugs from HashMap model d85fe5b Update RaceTimes references to TG-1404 and TG-1523 0e925e5 Update ticket number in HashMap.spec 03a5186 Enable TG-1404 tests fa051dd Delete ArrayList CustomType test file b0e853b Enable HashMap test previously blocked by TG-1877 44bfe0a Merge pull request diffblue#392 from diffblue/lajw/TG-2389-enable-tests 595dd5d Changes CProver helped methods in HashMap to protected. c52771c Merge pull request diffblue#385 from diffblue/jeannie/UpdateTestRunner de0abdc Enable tests fixed by recent test-gen fixes b64357a Remove ticket numbers from resolved bugfix tests 53eca00 Documents StringBuilder and StringBuffer append(Object) baec23f Merge pull request diffblue#389 from diffblue/antonia/enable-TG-2666-test b2f0258 Enable LinkedList test that was blocked by TG-2666 57e79e5 Add knownbug tests for TG-2717 80fa433 Merge pull request diffblue#387 from diffblue/forejtv/unsupportedcharsetexception 990129c Merge pull request diffblue#391 from diffblue/allredj/disable-html-report 97f32f6 Don't write to the Html report 4cb5996 Merge pull request diffblue#382 from diffblue/antonia/address-ArrayList-todos 6749702 Merge pull request diffblue#386 from diffblue/antonia/gauge-telemetry-off 546dfdc Move legacy style tests into main Gauge step 5be886f Mark UnsupportedCharsetException as untested 1c17838 Add regression test for side effects 8c836ab Add tests for ArrayLists w. (non-default) capacity 34a141d Address bugfix TODOs in ArrayList 563b631 Correct bug description in comment 3e7603d Merge pull request diffblue#383 from diffblue/antonia/reformat-HashSet-tests 5d4e013 [TG-2751] Added UnsupportedCharsetException 11b28fb Reformat HashSet.spec f77c3c4 Rename HashSet_L2.spec to HashSet_L0.spec a16a1e7 Move all HashSet Maven tests into HashSet.spec f21a2da Merge pull request diffblue#376 from diffblue/jeannie/LinkedHashMap 820c5f7 Merge pull request diffblue#380 from diffblue/jeannie/AppendObject af65f4d Tests java.lang.StringBuffer append(Object) a554517 Reformat tests in java.util.StringBuilder dd6d3f6 Models append(Object) for StringBuilder and StringBuffer. 8920399 Tests toString() methods on existing models where possible 647f4fe Tests toString() methods on existing models where possible 978273b Documents and implements toString() methods in existing models. 78020ee Documents java.util.LinkedHashMap fb0cf92 Tests java.util.LinkedHashMap 7a9df4e Models java.util.LinkedHashMap 5a8af60 Marks all methods as notModelled() for java.util.LinkedHashMap 8d6b149 Initial commit for java.util.LinkedHashMap 34b7c54 Merge pull request diffblue#359 from diffblue/forejtv/throwable-no-static e2230de Cleanup of unused (mostly static) variables 255013e Merge pull request diffblue#384 from diffblue/jeannie/DisableBoundedGenericHashMap f374d5f Merge pull request diffblue#381 from diffblue/justin/TG2600-Correction ce6328b Turn off Gauge telemetry on Travis 6ab2864 Updates TestRunner.java to mimic platform parameters. 8ee75a4 Disables a HashMap test that depends on bounded generic type. 3677c3a [TG-2600] correct a mistake in the L1RemoveLast test 4511813 Merge pull request diffblue#378 from diffblue/antonia/LinkedList-first-model 6bda7ea Add tests for LinkedList b5d4cbe Model LinkedList methods specified in TG-2600 aa6e90a Empty models for new classes 3c25555 Copy LinkedList and related classes from jdk 5e4d410 Merge pull request diffblue#373 from diffblue/romain/tests/activate-arrays-hashset-test#TG-1404 a0d9289 Activate some Arrays test 27d06b4 Activate tests for Hashset fixed by TG-1404 224962a Merge pull request diffblue#371 from diffblue/romain/tests/activate-after-fix-1404 ed26b28 Activate level 2 tests fixed by TG-1404 b59c1e9 Relabel known-bug for Level2 HashMap test 5c0041b Activate tests for HashMap.values fixed by TG-1404 2777872 Activate tests for HashMap.entrySet 50d3f2c Activate tests for HashMap.keySet fixed by TG-1404 6146215 Activate ArrayList test fixed by TG-1404 bc09fd7 Merge pull request diffblue#365 from diffblue/jeannie/getTimeZone 29cf7e0 Merge pull request diffblue#372 from diffblue/forejtv/bump-up-gauge-v bdd500a Change Gauge Java Maven Plugin to 0.6.6 190aa18 Tests java.util.TimeZone 170a992 Documents java.util.TimeZone in javadocs 9e52664 Models java.util.TimeZone constructor, getID, setID and getTimeZone. eac578e Tests sun.util.calendar.ZoneInfo b4be728 Documents sun.util.calendar.ZoneInfo in javadocs e5ffa98 Models the sun.util.calendar.ZoneInfo constructor and getTimeZone() 6d704ad Marks methods as notModelled() for sun.util.calendar.ZoneInfo d249adb Marks methods as notModelled() for java.util.TimeZone 7f71d8d Initial commit for sun.util.calendar.ZoneInfo. b53d9c1 Initial commit for java.util.TimeZone 056aad2 Merge pull request diffblue#368 from diffblue/allredj/fix-hashtable-spec 8848414 Merge pull request diffblue#370 from diffblue/allredj/stringbuffer-spec-small-correction 1d947e5 Small correction to StringBuffer spec file 42f1a93 Fix typo in hashtable spec file git-subtree-dir: benchmarks/LIBRARIES/models git-subtree-split: 67c80fcdcf82418b5e7099ae63dec3360b153f90
smowton
pushed a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
Update models library
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This affects cases when a floating-point number is cast to an integer
which is longer than the significand of the float and the exponent is
greater than the length of the significand. This includes
float -> (u)int32_t and double -> (u)int64_t. These were incorrectly
converted to 0.