diff --git a/regression/ansi-c/const1/const-array.desc b/regression/ansi-c/const1/const-array.desc index ccd82a57303..d244eaf4c74 100644 --- a/regression/ansi-c/const1/const-array.desc +++ b/regression/ansi-c/const1/const-array.desc @@ -1,6 +1,7 @@ CORE const-array.c ^.*: .* is constant$ +^ array\[1\] = 2;$ ^EXIT=(1|64)$ ^SIGNAL=0$ -- diff --git a/regression/ansi-c/const1/const-member.desc b/regression/ansi-c/const1/const-member.desc index 1e611e403b1..7f3877192c0 100644 --- a/regression/ansi-c/const1/const-member.desc +++ b/regression/ansi-c/const1/const-member.desc @@ -2,6 +2,7 @@ CORE const-member.c ^.*: .* is constant$ +^ const_struct_ptr->field = 123;$ ^EXIT=(1|64)$ ^SIGNAL=0$ -- diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp index 3973d243ed9..d6b0094c0a1 100644 --- a/src/util/cout_message.cpp +++ b/src/util/cout_message.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "cout_message.h" +#include #include #ifdef _WIN32 @@ -185,6 +186,26 @@ void gcc_message_handlert::print( dest+=message; print(level, dest); + + const auto file_name = location.full_path(); + if(file_name.has_value() && !line.empty()) + { +#ifdef _WIN32 + std::ifstream in(widen(file_name.value())); +#else + std::ifstream in(file_name.value()); +#endif + if(in) + { + const auto line_number = std::stoull(id2string(line)); + std::string line; + for(std::size_t l = 0; l < line_number; l++) + std::getline(in, line); + + if(in) + print(level, " " + line); // gcc adds a space, clang doesn't + } + } } void gcc_message_handlert::print( diff --git a/src/util/source_location.cpp b/src/util/source_location.cpp index 46f7f5282d9..b564c4089ec 100644 --- a/src/util/source_location.cpp +++ b/src/util/source_location.cpp @@ -71,6 +71,19 @@ void source_locationt::merge(const source_locationt &from) } } +/// Get a path to the file, including working directory. +/// \return Full path unless the file name is empty or refers +/// to a built-in, in which case {} is returned. +optionalt source_locationt::full_path() const +{ + const auto file = id2string(get_file()); + + if(file.empty() || is_built_in(file)) + return {}; + + return concat_dir_file(id2string(get_working_directory()), file); +} + std::ostream &operator << ( std::ostream &out, const source_locationt &source_location) diff --git a/src/util/source_location.h b/src/util/source_location.h index c7ea9daf804..999a98179e4 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "invariant.h" #include "irep.h" +#include "optional.h" #include "prefix.h" #include @@ -185,6 +186,8 @@ class source_locationt:public irept return static_cast(get_nil_irep()); } + optionalt full_path() const; + protected: std::string as_string(bool print_cwd) const; };