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 /driver | |
| parent | c0e121ceef1484ff3ad74fadb0b781ec1282690e (diff) | |
| download | compcert-12f7b21e6e1bafe895680108e75311c678a22ac1.tar.gz compcert-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 'driver')
0 files changed, 0 insertions, 0 deletions