Fix incorrect line number reporting for long assertions in error messages

Removes incorrect line number decrement after processing preprocessor
line directives in `scanner.l`. The `preprocessor_line()` function
already sets the correct line number, and the subsequent decrement was
causing off-by-one errors in line reporting for long expressions.

Fixes: #8257

Author: tautschnig

regression/cbmc/long_assertion_line_number/main.c

@@ -0,0 +1,13 @@
+#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();
+  /* clang-format off */
+  __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));
+  /* clang-format on */
+  return 0;
+}

regression/cbmc/long_assertion_line_number/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^\[main.assertion.1\] line 10 assertion: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test verifies that CBMC correctly reports line numbers for assertions in
+very long expressions.

src/ansi-c/scanner.l

@@ -333,7 +333,7 @@ enable_or_disable ("enable"|"disable")
 <STRING_LITERAL>{whitespace} { /* ignore */ }
 <STRING_LITERAL>{cpplineno} {
                   preprocessor_line(yytext, PARSER);
-                  PARSER.set_line_no(PARSER.get_line_no()-1);
+                  // Line number already set by preprocessor_line
                 }
 <STRING_LITERAL>{cppstart}.* { /* ignore */ }
 <STRING_LITERAL>"/*" { yy_push_state(STRING_LITERAL_COMMENT); /* C comment, ignore */ }
@@ -352,7 +352,7 @@ enable_or_disable ("enable"|"disable")
 
 <GRAMMAR>{cpplineno} {
                   preprocessor_line(yytext, PARSER);
-                  PARSER.set_line_no(PARSER.get_line_no()-1);
+                  // Line number already set by preprocessor_line
                 }
 
 <GRAMMAR>{cppstart}"pragma"{ws}"pack"{ws}"("{ws}"push"{ws}")"{ws}{newline} {
@@ -1620,7 +1620,7 @@ enable_or_disable ("enable"|"disable")
 <GCC_ASM>{
 {cpplineno}     {
                   preprocessor_line(yytext, PARSER);
-                  PARSER.set_line_no(PARSER.get_line_no()-1);
+                  // Line number already set by preprocessor_line
                 }
 {ws}            { /* ignore */ }
 {newline}       { /* ignore */ }
@@ -1639,7 +1639,7 @@ enable_or_disable ("enable"|"disable")
 <GCC_ATTRIBUTE1>{
 {cpplineno}     {
                   preprocessor_line(yytext, PARSER);
-                  PARSER.set_line_no(PARSER.get_line_no()-1);
+                  // Line number already set by preprocessor_line
                 }
 {ws}            { /* ignore */ }
 {newline}       { /* ignore */ }
@@ -1650,7 +1650,7 @@ enable_or_disable ("enable"|"disable")
 <GCC_ATTRIBUTE1a>{
 {cpplineno}     {
                   preprocessor_line(yytext, PARSER);
-                  PARSER.set_line_no(PARSER.get_line_no()-1);
+                  // Line number already set by preprocessor_line
                 }
 "("             { BEGIN(GCC_ATTRIBUTE2); PARSER.parenthesis_counter=0; return yytext[0]; }
 {ws}            { /* ignore */ }
@@ -1711,7 +1711,7 @@ enable_or_disable ("enable"|"disable")
 <GCC_ATTRIBUTE3>{ // an attribute we do process
 {cpplineno}     {
                   preprocessor_line(yytext, PARSER);
-                  PARSER.set_line_no(PARSER.get_line_no()-1);
+                  // Line number already set by preprocessor_line
                 }
 "("             { PARSER.parenthesis_counter++; loc(); return '('; }
 ")"             { if(PARSER.parenthesis_counter==0)
@@ -1774,7 +1774,7 @@ enable_or_disable ("enable"|"disable")
 <GCC_ATTRIBUTE5>{ // end bit: the closing parenthesis
 {cpplineno}     {
                   preprocessor_line(yytext, PARSER);
-                  PARSER.set_line_no(PARSER.get_line_no()-1);
+                  // Line number already set by preprocessor_line
                 }
 ")"             { BEGIN(GRAMMAR); loc(); return yytext[0]; }
 {ws}            { /* Throw away */ }