diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-11-24 10:03:11 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-24 10:03:11 +0100 |
| commit | 12f7b21e6e1bafe895680108e75311c678a22ac1 (patch) | |
| tree | 806a56f967dffd18f9e9041dff1a67397f265a61 /Changelog | |
| parent | c0e121ceef1484ff3ad74fadb0b781ec1282690e (diff) | |
| download | compcert-kvx-12f7b21e6e1bafe895680108e75311c678a22ac1.tar.gz compcert-kvx-12f7b21e6e1bafe895680108e75311c678a22ac1.zip | |
Issue #208: make value analysis of comparisons more conservative w.r.t. pointers (#209)
Comparisons such as "(uintptr_t) &global == 0x1234" are undefined behavior
in CompCert but their status in ISO C is unclear and they may occur in
real-world code. Make sure they are statically analyzed as Btop.
Diffstat (limited to 'Changelog')
| -rw-r--r-- | Changelog | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -1,5 +1,8 @@ Code generation and optimization: - ARM in Thumb mode: simpler instruction sequence for branch through jump table. +- Issue #208: make value analysis of comparisons more conservative for + dubious comparisons such as "(uintptr_t) &global == 0x1234" which are + undefined behavior in CompCert. Usability: - Resurrected support for the Cygwin x86-32 port, which got lost at release 3.0. |