Integer overflow checks on bitwise AND operator
During a comparison of integer overflow checks in Mopsa and Goblint, we noticed several cases where overflow checks are reported for bitwise AND and OR operations by Mopsa.
As @sim642 checked from the C standard, it does not define any undefined behavior associated with bitwise AND operations. Thus, these checks should probably not be reported under (Signed|Unsigned) integer overflow in arithmetic operator
Examples (a total of about ~1500 checks) reported by Mopsa:
title,file,expr,line
Signed integer overflow in arithmetic operator,/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_rand_square_22_bad.i,rand() & 1, data = ((int)(rand() & 1 ? (((unsigned)rand()<<30) ^ ((unsigned)rand()<<15) ^ rand()) : -(((unsigned)rand()<<30) ^ ((unsigned)rand()<<15) ^ rand()) - 1));
Signed integer overflow in arithmetic operator,/sv-benchmarks/c/bitvector/num_conversion_2.c,x & i, unsigned char bit = x & i;