Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit cc07d16

Browse files
committedFeb 11, 2025·
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.
1 parent 6957a04 commit cc07d16

File tree

6 files changed

+32
-13
lines changed

6 files changed

+32
-13
lines changed
 
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
file_with_no_newline.i
3+
4+
^file_with_no_newline\.i:0:1: error: .*$
5+
^EXIT=1$
6+
^SIGNAL=0$
7+
--
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
syntax error, no newline here ->

‎src/ansi-c/ansi_c_parser.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -208,13 +208,13 @@ void ansi_c_parsert::set_pragma_cprover()
208208
for(const auto &pragma : pragma_set)
209209
flattened[pragma.first] = pragma.second;
210210

211-
source_location.remove(ID_pragma);
211+
_source_location.remove(ID_pragma);
212212

213213
for(const auto &pragma : flattened)
214214
{
215215
std::string check_name = id2string(pragma.first);
216216
std::string full_name =
217217
(pragma.second ? "enable:" : "disable:") + check_name;
218-
source_location.add_pragma(full_name);
218+
_source_location.add_pragma(full_name);
219219
}
220220
}

‎src/cpp/cpp_parser.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ class cpp_parsert:public parsert
5656
void add_location()
5757
{
5858
token_buffer.current_token().line_no=get_line_no()-1;
59-
token_buffer.current_token().filename=source_location.get_file();
59+
token_buffer.current_token().filename = source_location().get_file();
6060
}
6161

6262
// scanner

‎src/util/parser.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ void parsert::parse_error(
4040
tmp_source_location.set_column(column-before.size());
4141
print(1, tmp, -1, tmp_source_location);
4242
#else
43-
log.error().source_location = source_location;
43+
log.error().source_location = source_location();
4444
log.error() << tmp << messaget::eom;
4545
#endif
4646
}

‎src/util/parser.h

Lines changed: 20 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
1717

1818
#include <filesystem>
1919
#include <iosfwd>
20+
#include <limits>
2021
#include <string>
2122
#include <vector>
2223

@@ -33,7 +34,7 @@ class parsert
3334
: in(nullptr),
3435
log(message_handler),
3536
line_no(0),
36-
previous_line_no(0),
37+
previous_line_no(std::numeric_limits<unsigned int>::max()),
3738
column(1)
3839
{
3940
}
@@ -82,14 +83,14 @@ class parsert
8283

8384
void set_file(const irep_idt &file)
8485
{
85-
source_location.set_file(file);
86-
source_location.set_working_directory(
86+
_source_location.set_file(file);
87+
_source_location.set_working_directory(
8788
std::filesystem::current_path().string());
8889
}
8990

9091
irep_idt get_file() const
9192
{
92-
return source_location.get_file();
93+
return _source_location.get_file();
9394
}
9495

9596
unsigned get_line_no() const
@@ -107,21 +108,31 @@ class parsert
107108
column=_column;
108109
}
109110

110-
void set_source_location(exprt &e)
111+
const source_locationt &source_location()
111112
{
112113
// Only set line number when needed, as this destroys sharing.
113114
if(previous_line_no!=line_no)
114115
{
115116
previous_line_no=line_no;
116-
source_location.set_line(line_no);
117+
118+
// for the case of a file with no newlines
119+
if(line_no == 0)
120+
_source_location.set_line(1);
121+
else
122+
_source_location.set_line(line_no);
117123
}
118124

119-
e.add_source_location()=source_location;
125+
return _source_location;
126+
}
127+
128+
void set_source_location(exprt &e)
129+
{
130+
e.add_source_location() = source_location();
120131
}
121132

122133
void set_function(const irep_idt &function)
123134
{
124-
source_location.set_function(function);
135+
_source_location.set_function(function);
125136
}
126137

127138
void advance_column(unsigned token_width)
@@ -131,7 +142,7 @@ class parsert
131142

132143
protected:
133144
messaget log;
134-
source_locationt source_location;
145+
source_locationt _source_location;
135146
unsigned line_no, previous_line_no;
136147
unsigned column;
137148
};

0 commit comments

Comments
 (0)
Please sign in to comment.