Correct me if I am wrong, but I thought that ssize_t localVar = 999999999999; is the culprit on 32bit architectures. However, we do not flag an overflow even on
If we let gcc -Wall -c -m32 test.c try with this minimal example, it flags the overflow in that line. Is this what the sv-comp task would require us to do, too?
exp.architecture only applies to preprocessing (which isn't used in SV-COMP anyway) right now. If this is based on 32bit architecture, then it's just another instance of #54 revealing itself.
Straight from
no-overflow
onldv-regression/test_overflow.i
; we are not flagging any overflow here.Correct me if I am wrong, but I thought that
ssize_t localVar = 999999999999;
is the culprit on 32bit architectures. However, we do not flag an overflow even onIf we let
gcc -Wall -c -m32 test.c
try with this minimal example, it flags the overflow in that line. Is this what the sv-comp task would require us to do, too?