Feature #6546
open
GCC replaces boolean conjuction with bit precise analogue
Added by Ilja Zakharov over 8 years ago.
Updated about 8 years ago.
Description
GCC replaces expressions like
a == 0 && b == 0
by
(a | b) == 0
The latter expression cannot be processed properly by CPAchecker with default LDV configuration which brings more false positives in results.
- Description updated (diff)
- Status changed from New to Open
- Priority changed from Normal to High
We can meet this in the following ways (ordered by preference and simplicity):
- Replace expressions back in C-backend. I would like to have some option to turn on this behaviour.
- Avoid such expressions as much as possible. For instance this issue appears due to a new environment model and actually can be quite easily fixed there. But we can not guarantee that, say, Linux kernel source code did/does/will not have similar expressions.
- Disable this conversion in GCC internals as well with some option.
- Teach CPAchecker to process such simple bit precise expressions but who will teach other verifiers.
- Tracker changed from Bug to Feature
- Category set to C back-end
Also available in: Atom
PDF