From a262c00a58b19cc2db42ab90ba17f08431230819 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 6 Jan 2025 10:03:16 +0000
Subject: [PATCH] line number for files with no newline
The parser sets the line number used for error messages once reaching a
newline. This fixes the logic for the case that the input file does not
have a newline.
This is only visible on .i files, as the preprocessor adds a newline when
there isn't one on .c files.
---
.../ansi-c/errors/file_with_no_newline.desc | 7 +++++
.../ansi-c/errors/file_with_no_newline.i | 1 +
src/ansi-c/ansi_c_parser.cpp | 4 +--
src/cpp/cpp_parser.h | 2 +-
src/util/parser.cpp | 2 +-
src/util/parser.h | 29 +++++++++++++------
6 files changed, 32 insertions(+), 13 deletions(-)
create mode 100644 regression/ansi-c/errors/file_with_no_newline.desc
create mode 100644 regression/ansi-c/errors/file_with_no_newline.i
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 <filesystem>
#include <iosfwd>
+#include <limits>
#include <string>
#include <vector>
@@ -33,7 +34,7 @@ class parsert
: in(nullptr),
log(message_handler),
line_no(0),
- previous_line_no(0),
+ previous_line_no(std::numeric_limits<unsigned int>::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;
};