Open Quuxplusone opened 14 years ago
Attached main.c
(676 bytes, application/octet-stream): Code exhibiting issue
I think we lose the control-dependency here because 'N' is assigned a conjured value. We aren't modeling the field value because it is a double.
Attached minimal.c
(155 bytes, text/plain): Minimal example not using doubles
I can't get an error for the case without floating-point involvement on ToT. For the one with, here's what I see as the main problem, or at least a low-hanging fruit: if you perform the same cast twice, you get the same result. Is there any way we can model that?
Indeed, I can confirm that my example doesn't give an error anymore. Thanks to whoever fixed it :)
Attached main.c
(460 bytes, text/plain): ```
Similar false positive after casting array of uint16_t to uint8_t*
main.c
(676 bytes, application/octet-stream)minimal.c
(155 bytes, text/plain)main.c
(460 bytes, text/plain)