Skip to content

Commit 04e7ff7

Browse files
tautschnigtautschnig
authored
Merge pull request #3637 from tautschnig/cl-message-handler
CL message handler
2 parents 0181841 + 8edd464 commit 04e7ff7

18 files changed

+257
-138
lines changed

‎regression/ansi-c/const1/array-of-const.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
CORE
22
array-of-const.c
3-
^.*: .* is constant$
3+
4+
^.*: .* is constant$
45
^EXIT=(1|64)$
56
^SIGNAL=0$
67
--

‎regression/ansi-c/const1/const-array.desc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
1-
KNOWNBUG
1+
CORE
22
const-array.c
3-
^.*: .* is constant$
4-
^ array\[1\] = 2;$
3+
4+
^.*: .* is constant$
5+
array\[1\] = 2;$
56
^EXIT=(1|64)$
67
^SIGNAL=0$
78
--

‎regression/ansi-c/const1/const-member.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
KNOWNBUG
1+
CORE
22
const-member.c
33

44
^.*: .* is constant$
5-
^ const_struct_ptr->field = 123;$
5+
const_struct_ptr->field = 123;$
66
^EXIT=(1|64)$
77
^SIGNAL=0$
88
--

‎src/goto-cc/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,11 @@ SRC = armcc_cmdline.cpp \
44
as_cmdline.cpp \
55
as_mode.cpp \
66
bcc_cmdline.cpp \
7+
cl_message_handler.cpp \
78
compile.cpp \
89
cw_mode.cpp \
910
gcc_cmdline.cpp \
11+
gcc_message_handler.cpp \
1012
gcc_mode.cpp \
1113
gcc_version.cpp \
1214
goto_cc_cmdline.cpp \

‎src/goto-cc/armcc_mode.h

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,9 @@ Date: June 2006
1414
#ifndef CPROVER_GOTO_CC_ARMCC_MODE_H
1515
#define CPROVER_GOTO_CC_ARMCC_MODE_H
1616

17-
#include <util/cout_message.h>
18-
19-
#include "goto_cc_mode.h"
2017
#include "armcc_cmdline.h"
18+
#include "gcc_message_handler.h"
19+
#include "goto_cc_mode.h"
2120

2221
class armcc_modet:public goto_cc_modet
2322
{

‎src/goto-cc/as_mode.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,6 @@ Author: Michael Tautschnig
2424
#include <cstring>
2525

2626
#include <util/config.h>
27-
#include <util/cout_message.h>
2827
#include <util/get_base_name.h>
2928
#include <util/run.h>
3029
#include <util/tempdir.h>

‎src/goto-cc/as_mode.h

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,7 @@ Date: July 2016
1414
#ifndef CPROVER_GOTO_CC_AS_MODE_H
1515
#define CPROVER_GOTO_CC_AS_MODE_H
1616

17-
#include <util/cout_message.h>
18-
17+
#include "gcc_message_handler.h"
1918
#include "goto_cc_mode.h"
2019

2120
class as_modet:public goto_cc_modet

‎src/goto-cc/cl_message_handler.cpp

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
/*******************************************************************\
2+
3+
Module: Print messages like CL.exe does
4+
5+
Author: Michael Tautschnig
6+
7+
\*******************************************************************/
8+
9+
#include "cl_message_handler.h"
10+
11+
#include <util/unicode.h>
12+
13+
#include <fstream>
14+
#include <iostream>
15+
#include <sstream>
16+
17+
void cl_message_handlert::print(
18+
unsigned level,
19+
const std::string &message,
20+
const source_locationt &location)
21+
{
22+
if(verbosity < level || location == source_locationt())
23+
{
24+
console_message_handlert::print(level, message);
25+
return;
26+
}
27+
28+
std::ostringstream formatted_message;
29+
30+
const irep_idt file = location.get_file();
31+
const std::string &line = id2string(location.get_line());
32+
formatted_message << file << '(' << line << "): ";
33+
34+
if(level == messaget::M_ERROR)
35+
formatted_message << "error: ";
36+
else if(level == messaget::M_WARNING)
37+
formatted_message << "warning: ";
38+
39+
formatted_message << message;
40+
41+
const auto full_path = location.full_path();
42+
43+
if(full_path.has_value() && !line.empty())
44+
{
45+
#ifdef _WIN32
46+
std::ifstream in(widen(full_path.value()));
47+
#else
48+
std::ifstream in(full_path.value());
49+
#endif
50+
if(in)
51+
{
52+
const auto line_number = std::stoull(line);
53+
std::string source_line;
54+
for(std::size_t l = 0; l < line_number; l++)
55+
std::getline(in, source_line);
56+
57+
if(in)
58+
{
59+
formatted_message << '\n';
60+
formatted_message << file << '(' << line << "): " << source_line;
61+
}
62+
}
63+
}
64+
65+
console_message_handlert::print(level, formatted_message.str());
66+
}

‎src/goto-cc/cl_message_handler.h

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
/*******************************************************************\
2+
3+
Module: Print messages like CL.exe does
4+
5+
Author: Michael Tautschnig
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_GOTO_CC_CL_MESSAGE_HANDLER_H
10+
#define CPROVER_GOTO_CC_CL_MESSAGE_HANDLER_H
11+
12+
#include <util/cout_message.h>
13+
14+
class cl_message_handlert : public console_message_handlert
15+
{
16+
public:
17+
void print(unsigned, const xmlt &) override
18+
{
19+
}
20+
21+
void print(unsigned, const jsont &) override
22+
{
23+
}
24+
25+
// aims to imitate the messages CL prints
26+
void print(
27+
unsigned level,
28+
const std::string &message,
29+
const source_locationt &location) override;
30+
31+
using console_message_handlert::print;
32+
};
33+
34+
#endif // CPROVER_GOTO_CC_CL_MESSAGE_HANDLER_H

‎src/goto-cc/gcc_message_handler.cpp

Lines changed: 97 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "gcc_message_handler.h"
10+
11+
#include <util/unicode.h>
12+
13+
#include <fstream>
14+
#include <iostream>
15+
16+
void gcc_message_handlert::print(
17+
unsigned level,
18+
const std::string &message,
19+
const source_locationt &location)
20+
{
21+
message_handlert::print(level, message);
22+
23+
if(verbosity >= level)
24+
{
25+
// gcc appears to send everything to cerr
26+
auto &out = std::cerr;
27+
28+
const irep_idt file = location.get_file();
29+
const irep_idt line = location.get_line();
30+
const irep_idt column = location.get_column();
31+
const irep_idt function = location.get_function();
32+
33+
if(!function.empty())
34+
{
35+
if(!file.empty())
36+
out << string(messaget::bold) << file << ':' << string(messaget::reset)
37+
<< ' ';
38+
out << "In function " << string(messaget::bold) << '\'' << function
39+
<< '\'' << string(messaget::reset) << ":\n";
40+
}
41+
42+
if(!line.empty())
43+
{
44+
out << string(messaget::bold);
45+
46+
if(!file.empty())
47+
out << file << ':';
48+
49+
out << line << ':';
50+
51+
if(column.empty())
52+
out << "1: ";
53+
else
54+
out << column << ": ";
55+
56+
if(level == messaget::M_ERROR)
57+
out << string(messaget::red) << "error: ";
58+
else if(level == messaget::M_WARNING)
59+
out << string(messaget::bright_magenta) << "warning: ";
60+
61+
out << string(messaget::reset);
62+
}
63+
64+
out << message << '\n';
65+
66+
const auto file_name = location.full_path();
67+
if(file_name.has_value() && !line.empty())
68+
{
69+
#ifdef _WIN32
70+
std::ifstream in(widen(file_name.value()));
71+
#else
72+
std::ifstream in(file_name.value());
73+
#endif
74+
if(in)
75+
{
76+
const auto line_number = std::stoull(id2string(line));
77+
std::string source_line;
78+
for(std::size_t l = 0; l < line_number; l++)
79+
std::getline(in, source_line);
80+
81+
if(in)
82+
out << ' ' << source_line << '\n'; // gcc adds a space, clang doesn't
83+
}
84+
}
85+
86+
out << std::flush;
87+
}
88+
}
89+
90+
void gcc_message_handlert::print(unsigned level, const std::string &message)
91+
{
92+
message_handlert::print(level, message);
93+
94+
// gcc appears to send everything to cerr
95+
if(verbosity >= level)
96+
std::cerr << message << '\n' << std::flush;
97+
}

‎src/goto-cc/gcc_message_handler.h

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_GOTO_CC_GCC_MESSAGE_HANDLER_H
10+
#define CPROVER_GOTO_CC_GCC_MESSAGE_HANDLER_H
11+
12+
#include <util/cout_message.h>
13+
14+
class gcc_message_handlert : public console_message_handlert
15+
{
16+
public:
17+
void print(unsigned, const xmlt &) override
18+
{
19+
}
20+
21+
void print(unsigned, const jsont &) override
22+
{
23+
}
24+
25+
// aims to imitate the messages gcc prints
26+
void print(unsigned level, const std::string &message) override;
27+
28+
void print(
29+
unsigned level,
30+
const std::string &message,
31+
const source_locationt &location) override;
32+
33+
private:
34+
/// feed a command into a string
35+
std::string string(const messaget::commandt &c) const
36+
{
37+
return command(c.command);
38+
}
39+
};
40+
41+
#endif // CPROVER_GOTO_CC_GCC_MESSAGE_HANDLER_H

‎src/goto-cc/gcc_mode.h

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,11 +15,10 @@ Date: June 2006
1515
#define CPROVER_GOTO_CC_GCC_MODE_H
1616

1717
#include "compile.h"
18+
#include "gcc_message_handler.h"
1819
#include "gcc_version.h"
1920
#include "goto_cc_mode.h"
2021

21-
#include <util/cout_message.h>
22-
2322
#include <set>
2423

2524
class gcc_modet:public goto_cc_modet

‎src/goto-cc/ld_mode.h

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,9 @@ Date: June 2006
1515
#define CPROVER_GOTO_CC_LD_MODE_H
1616

1717
#include "compile.h"
18+
#include "gcc_message_handler.h"
1819
#include "goto_cc_mode.h"
1920

20-
#include <util/cout_message.h>
21-
2221
#include <set>
2322

2423
class ld_modet : public goto_cc_modet

‎src/goto-cc/linker_script_merge.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@
77

88
#include <functional>
99

10-
#include <util/cout_message.h>
1110
#include <util/json.h>
1211

1312
#include "compile.h"

‎src/goto-cc/ms_cl_mode.h

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,7 @@ Date: June 2006
1414
#ifndef CPROVER_GOTO_CC_MS_CL_MODE_H
1515
#define CPROVER_GOTO_CC_MS_CL_MODE_H
1616

17-
#include <util/cout_message.h>
18-
17+
#include "cl_message_handler.h"
1918
#include "goto_cc_mode.h"
2019
#include "ms_cl_cmdline.h"
2120

@@ -35,7 +34,7 @@ class ms_cl_modet:public goto_cc_modet
3534

3635
protected:
3736
ms_cl_cmdlinet &cmdline;
38-
console_message_handlert message_handler;
37+
cl_message_handlert message_handler;
3938
};
4039

4140
#endif // CPROVER_GOTO_CC_MS_CL_MODE_H

‎src/goto-cc/ms_link_mode.h

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,11 +14,10 @@ Date: July 2018
1414
#ifndef CPROVER_GOTO_CC_MS_LINK_MODE_H
1515
#define CPROVER_GOTO_CC_MS_LINK_MODE_H
1616

17+
#include "cl_message_handler.h"
1718
#include "compile.h"
1819
#include "goto_cc_mode.h"
1920

20-
#include <util/cout_message.h>
21-
2221
class ms_link_modet : public goto_cc_modet
2322
{
2423
public:
@@ -28,7 +27,7 @@ class ms_link_modet : public goto_cc_modet
2827
explicit ms_link_modet(goto_cc_cmdlinet &);
2928

3029
protected:
31-
console_message_handlert message_handler;
30+
cl_message_handlert message_handler;
3231
};
3332

3433
#endif // CPROVER_GOTO_CC_MS_LINK_MODE_H

0 commit comments

Comments
 (0)