Skip to content

Commit

Permalink
line number for files with no newline
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
kroening committed Jan 6, 2025
1 parent 1e99418 commit 3e90cae
Show file tree
Hide file tree
Showing 6 changed files with 32 additions and 13 deletions.
7 changes: 7 additions & 0 deletions regression/ansi-c/errors/file_with_no_newline.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE
file_with_no_newline.i

^file file_with_no_newline\.i line 1 function syntax: .*$
^EXIT=6$
^SIGNAL=0$
--
1 change: 1 addition & 0 deletions regression/ansi-c/errors/file_with_no_newline.i
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
syntax error, no newline here ->
4 changes: 2 additions & 2 deletions src/ansi-c/ansi_c_parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}
2 changes: 1 addition & 1 deletion src/cpp/cpp_parser.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/util/parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
29 changes: 20 additions & 9 deletions src/util/parser.h
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]

#include <filesystem>
#include <iosfwd>
#include <limits>
#include <string>
#include <vector>

Expand All @@ -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)
{
}
Expand Down Expand Up @@ -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
Expand All @@ -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)
Expand All @@ -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;
};
Expand Down

0 comments on commit 3e90cae

Please sign in to comment.