diff --git a/regression/ansi-c/errors/file_with_no_newline.desc b/regression/ansi-c/errors/file_with_no_newline.desc new file mode 100644 index 00000000000..bb69d2003c3 --- /dev/null +++ b/regression/ansi-c/errors/file_with_no_newline.desc @@ -0,0 +1,7 @@ +CORE +file_with_no_newline.i + +^file_with_no_newline\.i((:[01]:1)|(\(1\))): error: .*$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- diff --git a/regression/ansi-c/errors/file_with_no_newline.i b/regression/ansi-c/errors/file_with_no_newline.i new file mode 100644 index 00000000000..c35cf87ec86 --- /dev/null +++ b/regression/ansi-c/errors/file_with_no_newline.i @@ -0,0 +1 @@ +syntax error, no newline here -> \ No newline at end of file diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp index c26911d93b0..749d9f92fa5 100644 --- a/src/ansi-c/ansi_c_parser.cpp +++ b/src/ansi-c/ansi_c_parser.cpp @@ -208,13 +208,13 @@ void ansi_c_parsert::set_pragma_cprover() for(const auto &pragma : pragma_set) flattened[pragma.first] = pragma.second; - source_location.remove(ID_pragma); + _source_location.remove(ID_pragma); for(const auto &pragma : flattened) { std::string check_name = id2string(pragma.first); std::string full_name = (pragma.second ? "enable:" : "disable:") + check_name; - source_location.add_pragma(full_name); + _source_location.add_pragma(full_name); } } diff --git a/src/cpp/cpp_parser.h b/src/cpp/cpp_parser.h index 90dd36d4df8..e6db4d3c7cf 100644 --- a/src/cpp/cpp_parser.h +++ b/src/cpp/cpp_parser.h @@ -56,7 +56,7 @@ class cpp_parsert:public parsert void add_location() { token_buffer.current_token().line_no=get_line_no()-1; - token_buffer.current_token().filename=source_location.get_file(); + token_buffer.current_token().filename = source_location().get_file(); } // scanner diff --git a/src/util/parser.cpp b/src/util/parser.cpp index ae2a3289949..04906b04446 100644 --- a/src/util/parser.cpp +++ b/src/util/parser.cpp @@ -40,7 +40,7 @@ void parsert::parse_error( tmp_source_location.set_column(column-before.size()); print(1, tmp, -1, tmp_source_location); #else - log.error().source_location = source_location; + log.error().source_location = source_location(); log.error() << tmp << messaget::eom; #endif } diff --git a/src/util/parser.h b/src/util/parser.h index 32412d3226d..43d2c853d22 100644 --- a/src/util/parser.h +++ b/src/util/parser.h @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -33,7 +34,7 @@ class parsert : in(nullptr), log(message_handler), line_no(0), - previous_line_no(0), + previous_line_no(std::numeric_limits::max()), column(1) { } @@ -82,14 +83,14 @@ class parsert void set_file(const irep_idt &file) { - source_location.set_file(file); - source_location.set_working_directory( + _source_location.set_file(file); + _source_location.set_working_directory( std::filesystem::current_path().string()); } irep_idt get_file() const { - return source_location.get_file(); + return _source_location.get_file(); } unsigned get_line_no() const @@ -107,21 +108,31 @@ class parsert column=_column; } - void set_source_location(exprt &e) + const source_locationt &source_location() { // Only set line number when needed, as this destroys sharing. if(previous_line_no!=line_no) { previous_line_no=line_no; - source_location.set_line(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); } - e.add_source_location()=source_location; + return _source_location; + } + + void set_source_location(exprt &e) + { + e.add_source_location() = source_location(); } void set_function(const irep_idt &function) { - source_location.set_function(function); + _source_location.set_function(function); } void advance_column(unsigned token_width) @@ -131,7 +142,7 @@ class parsert protected: messaget log; - source_locationt source_location; + source_locationt _source_location; unsigned line_no, previous_line_no; unsigned column; };