CBMC 5.95.1 reporting wrong line number if assertion is long

[christina1993]

Hi,
if you invoke cbmc without any options on

#define __CBMC_assert(cond) __CPROVER_assert((cond), "assertion"); __CPROVER_assume(cond)
extern int __VERIFIER_nondet_int();
int main() {
  int A[1];
    A[0] = __VERIFIER_nondet_int();
__CBMC_assert((A[0] < (-1) && A[0] < ~(4294967294U) && A[0] < 0LL && (A[0] > -214748647LL && ((((A[0] < 20158765) && A[0] > 2147483648U && A[0] > 1929301145 && (A[0] > 1944729020 && A[0] < 0 && A[0] < -1LL && A[0] > 4294967294ULL && A[0] != ~(2147483647U)) && A[0] > ~(4294967294U) && A[0] < ~(4294967295U))) && (A[0] > ~(2147483646U) && (A[0] < 1L && A[0] > 1ULL && A[0] > 1LL && A[0] < ~(-1) && A[0] < 2147483647ULL) && (A[0] < 0U) && (A[0] < 2147483647L && (A[0] < 0U && (A[0] < 1UL)) && (((A[0] > ~(0U) || A[0] < ~(1U)) || A[0] > 1321734560)) && A[0] < 4294967294ULL) && (A[0] < 1UL && ((A[0] > 2147483646U && A[0] <= 1U) && A[0] < 1U) && A[0] > 1U) && A[0] > 1ULL) && A[0] > 1L && (A[0] < 4294967295UL && A[0] < 4294967294UL && A[0] < 1L && (A[0] > ~(2147483647) && A[0] < 2147483647UL && A[0] < 2147483647L && A[0] < 0U) && ((A[0] > ~(1) && (A[0] > 1UL) && (A[0] > 2147483648U) && A[0] <= 2147483647) && A[0] > 1L)) && (A[0] < 4294967294UL && A[0] < ~(4294967294U) && A[0] > -1453357121 && A[0] < 1U) && A[0] < 2147483646U && (A[0] > 1L && (((A[0] < 1UL)) && A[0] < ~(0) && A[0] != ~(-1)) && A[0] < 4294967294ULL) && (A[0] < ~(4294967295U)) && A[0] <= 2147483647LL) && ((A[0] < 0U && ((A[0] > ~(2147483646U) && ((A[0] < ~(-2147483647)) && A[0] > ~(0) && A[0] > -1 && A[0] < -1L && (A[0] < 2147483646LL && (A[0] < -1) && ((A[0] < 2))) && (A[0] < 2147483647L && (A[0] < 2147483646LL && A[0] < 4294967295U) && A[0] > ~(4294967294U))) && ((A[0] > ~(1U)) && ((A[0] < 1U && (A[0] < 0 && A[0] < 2147483647U && (A[0] > 4294967294ULL)) && (A[0] < 2147483647ULL || A[0] < ~(1)))) && A[0] < -1LL && (((A[0] > 4294967295ULL && (((A[0] > 2147483648ULL)) && A[0] >= 4294967295U)) && A[0] < 2147483646ULL && A[0] <= 0L))) && A[0] > 0U && ((A[0] > 552237804 && A[0] > 4294967294UL) && (((A[0] < 0L && (A[0] > -2147483648) && ((((((((A[0] > -2147483647))))) && A[0] >= -2147483648) || (A[0] <= ~(1) && (A[0] >= 4294967295UL))) && A[0] <= 2147483646LL)) && A[0] != 100000) || (A[0] < -1L)) && A[0] != 4294967294U))) && A[0] < 0 && A[0] > ~(1U) && A[0] > -62844098 && A[0] < ~(-2147483647) && A[0] > 0UL && A[0] < 1U && A[0] > 0) && (A[0] < ~(0) && (A[0] > 4294967295UL) && (A[0] < 0UL) && (A[0] > 1ULL && (A[0] > 1UL) && (A[0] > 2056281653) && A[0] < 4294967294UL) && A[0] > 4294967294U && A[0] > 4294967294U && (A[0] > -1) && A[0] <= ~(1U)) && A[0] < 2147483646L && (A[0] > ~(0U) && A[0] > -1LL && (A[0] > ~(2147483647)) && A[0] > -2147483647L && ((A[0] < -2147483648 && (A[0] >= ~(2147483646))))) && A[0] > 4294967295ULL && (A[0] > -2147483648L && (A[0] < ~(1) && A[0] < 2147483646LL) && A[0] > ~(-1)) && ((A[0] < 4294967295UL) || (((A[0] > 4294967295UL && (((A[0] < 0 && ((A[0] < 2147483646ULL) && ((A[0] < 1)))))) && A[0] > ~(0U) && (((A[0] >= -1)) && A[0] > -2147483648)) && A[0] < 2147483646ULL && A[0] != 0L))) && A[0] > 1UL) && A[0] > 4294967294ULL && (A[0] < 2147483646U && A[0] < -2147483647L && A[0] > -1485823147 && A[0] < 1U && A[0] > 1L && (((A[0] < 2147483647ULL && A[0] > 2147483646ULL)))) && A[0] < 4294967294UL && ((A[0] != 2147483647ULL || A[0] > 0))) && (A[0] < ~(1U) && (A[0] < 1ULL && (A[0] > ~(4294967295U) && A[0] > 1U && (A[0] > 2147483646U && A[0] > -1LL && A[0] > ~(1) && A[0] < 2147483646L && A[0] > 1UL && A[0] < 0 && A[0] < -1L && A[0] != ~(1)) && (((((A[0] > -2147483647LL) && A[0] < 1L && (A[0] > -2147483648L) && A[0] < 4294967294ULL && A[0] > -2147483648L)) && A[0] > -82984055 && A[0] > -1 && ((A[0] < 2147483646LL) && A[0] < 2147483646LL) && A[0] < 2147483646UL) && (((A[0] > -2147483647L))) && A[0] < 2147483646 && A[0] < 100000) && A[0] < 1LL && A[0] < ~(2147483648U) && (A[0] >= 1U || A[0] != 2147483647ULL)) && A[0] < 2147483646U && A[0] < 2147483647L) && (A[0] < 4294967294UL && A[0] < 2147483646U && ((A[0] < ~(4294967295U))) && A[0] <= ~(0)) && ((((A[0] < 2147483646ULL && A[0] > -1 && A[0] < ~(2147483648U) && A[0] < 0UL) && A[0] > -2147483647L && A[0] > ~(-1)) && A[0] < 1U && A[0] <= ~(4294967294U)) && A[0] > ~(4294967295U)) && A[0] < 0) && (((A[0] > -390958390)) && (A[0] < 0UL) && (A[0] < ~(2147483648U)) && A[0] <= 4294967294UL) && A[0] >= 0ULL));
  return 0;
}

you get

test.c function main
[main.assertion.1] line 5 assertion: FAILURE

The fact that the assertion fails is correct, but the line number '5' does not match, because the assertion is on line 6.
Notice that, this bug disappears if I delete a character from the asserted condition. Did I hit a hidden limit on the maximum string length of an assertion?

[tautschnig]

It seems we need to review how YY_INPUT in src/util/parser.h detects newlines. Flex will read chunks of at most 8192 bytes (except for IA64). For lines longer than this I still need to understand what we need to do to pick up the newline.

[kroening]

I wanted to move the line counting out of that parser base class for a while. E.g., look at the SMT2 front-end.