Actions
Feature #6546
openGCC replaces boolean conjuction with bit precise analogue
Start date:
01/28/2016
Due date:
% Done:
0%
Estimated time:
Published in build:
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.
Updated by Evgeny Novikov about 8 years ago
- 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.
Actions