diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-11-03 10:36:15 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-11-03 10:36:15 +0000 |
commit | dcb9f48f51cec5e864565862a700c27df2a1a7e6 (patch) | |
tree | b453b51b7406d3b1cf7191729637446a23ffc92c /Changelog | |
parent | bd93aa7ef9c19a4def8aa64c32faeb04ab2607e9 (diff) | |
download | compcert-dcb9f48f51cec5e864565862a700c27df2a1a7e6.tar.gz compcert-dcb9f48f51cec5e864565862a700c27df2a1a7e6.zip |
Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2065 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Changelog')
-rw-r--r-- | Changelog | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -1,6 +1,11 @@ Release 1.12 ======================== +Improvements in confidence: +- Floating-point literals are now parsed and converted to IEEE-754 binary + FP numbers using a provably-correct conversion function implemented on + top of the Flocq library. + Language semantics: - The "&&" and "||" operators are now primitive in CompCert C and are given explicit semantic rules, instead of being expressed in terms |