diff --git a/regression/cbmc/long_assertion_line_number/main.c b/regression/cbmc/long_assertion_line_number/main.c new file mode 100644 index 00000000000..4bc6c9f013d --- /dev/null +++ b/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; +} diff --git a/regression/cbmc/long_assertion_line_number/test.desc b/regression/cbmc/long_assertion_line_number/test.desc new file mode 100644 index 00000000000..140c9c946fc --- /dev/null +++ b/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. diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index 570d62c4db9..dc40fc4225d 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -93,7 +93,7 @@ bool ansi_c_languaget::parse( if(!result) { - ansi_c_parser.set_line_no(0); + ansi_c_parser.set_line_no(1); ansi_c_parser.set_file(path); ansi_c_parser.in=&i_preprocessed; ansi_c_scanner_init(ansi_c_parser); diff --git a/src/goto-instrument/contracts/contracts_wrangler.cpp b/src/goto-instrument/contracts/contracts_wrangler.cpp index e66d6f52421..b0367d615af 100644 --- a/src/goto-instrument/contracts/contracts_wrangler.cpp +++ b/src/goto-instrument/contracts/contracts_wrangler.cpp @@ -140,7 +140,6 @@ void contracts_wranglert::mangle( // Parse the fake function. std::istringstream is(pr.str()); ansi_c_parsert ansi_c_parser{message_handler}; - ansi_c_parser.set_line_no(0); ansi_c_parser.set_file(""); ansi_c_parser.in = &is; ansi_c_parser.for_has_scope = config.ansi_c.for_has_scope; diff --git a/src/statement-list/statement_list_language.cpp b/src/statement-list/statement_list_language.cpp index d1cc36b7b5b..db871437507 100644 --- a/src/statement-list/statement_list_language.cpp +++ b/src/statement-list/statement_list_language.cpp @@ -62,7 +62,6 @@ bool statement_list_languaget::parse( { statement_list_parsert statement_list_parser{message_handler}; parse_path = path; - statement_list_parser.set_line_no(0); statement_list_parser.set_file(path); statement_list_parser.in = &instream; bool result = statement_list_parser.parse(); diff --git a/src/util/parser.h b/src/util/parser.h index eeec3b469a0..f4a5bf7ab1f 100644 --- a/src/util/parser.h +++ b/src/util/parser.h @@ -33,9 +33,10 @@ class parsert explicit parsert(message_handlert &message_handler) : in(nullptr), log(message_handler), - line_no(0), + line_no(1), previous_line_no(std::numeric_limits::max()), - column(1) + column(1), + last_input_ended_with_newline(false) { } @@ -114,12 +115,7 @@ class parsert if(previous_line_no!=line_no) { previous_line_no=line_no; - - // for the case of a file with no newlines - if(line_no == 0) - _source_location.set_line(1); - else - _source_location.set_line(line_no); + _source_location.set_line(line_no); } return _source_location; @@ -150,6 +146,12 @@ class parsert source_locationt _source_location; unsigned line_no, previous_line_no; unsigned column; + +public: + // Accessed by YY_INPUT macro; tracks whether the last YY_INPUT call + // ended with a newline so that the line-number increment can be + // deferred to the start of the next call. + bool last_input_ended_with_newline; }; exprt &_newstack(parsert &parser, unsigned &x); @@ -161,29 +163,35 @@ exprt &_newstack(parsert &parser, unsigned &x); #define stack_type(x) \ (static_cast(static_cast(PARSER.stack[x]))) -#define YY_INPUT(buf, result, max_size) \ - do { \ - for(result=0; result