Skip to content

Commit 406a6c4

Browse files
smowtonsmowton
authored
Merge pull request #1059 from smowton/smowton/fix/structured_trace_output
Add preformatted message flag
2 parents 7583da2 + 20e4def commit 406a6c4

File tree

7 files changed

+96
-42
lines changed

7 files changed

+96
-42
lines changed

‎src/cbmc/bmc.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ void bmct::error_trace()
6666
{
6767
xmlt xml;
6868
convert(ns, goto_trace, xml);
69-
status() << xml << eom;
69+
status() << preformatted_output << xml << eom;
7070
}
7171
break;
7272

@@ -83,7 +83,7 @@ void bmct::error_trace()
8383
result["status"]=json_stringt("failed");
8484
jsont &json_trace=result["trace"];
8585
convert(ns, goto_trace, json_trace);
86-
status() << ",\n" << json_result << eom;
86+
status() << preformatted_output << json_result << eom;
8787
}
8888
break;
8989
}

‎src/util/cout_message.cpp

+9-6
Original file line numberDiff line numberDiff line change
@@ -31,9 +31,10 @@ cerr_message_handlert::cerr_message_handlert():
3131

3232
void console_message_handlert::print(
3333
unsigned level,
34-
const std::string &message)
34+
const std::string &message,
35+
bool preformatted)
3536
{
36-
message_handlert::print(level, message);
37+
message_handlert::print(level, message, preformatted);
3738

3839
if(verbosity<level)
3940
return;
@@ -101,7 +102,8 @@ void gcc_message_handlert::print(
101102
unsigned level,
102103
const std::string &message,
103104
int sequence_number,
104-
const source_locationt &location)
105+
const source_locationt &location,
106+
bool preformatted)
105107
{
106108
const irep_idt file=location.get_file();
107109
const irep_idt line=location.get_line();
@@ -139,14 +141,15 @@ void gcc_message_handlert::print(
139141

140142
dest+=message;
141143

142-
print(level, dest);
144+
print(level, dest, preformatted);
143145
}
144146

145147
void gcc_message_handlert::print(
146148
unsigned level,
147-
const std::string &message)
149+
const std::string &message,
150+
bool preformatted)
148151
{
149-
message_handlert::print(level, message);
152+
message_handlert::print(level, message, preformatted);
150153

151154
// gcc appears to send everything to cerr
152155
if(verbosity>=level)

‎src/util/cout_message.h

+6-3
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,8 @@ class console_message_handlert:public ui_message_handlert
3232
// level 4 and upwards go to cout, level 1-3 to cerr
3333
virtual void print(
3434
unsigned level,
35-
const std::string &message) override;
35+
const std::string &message,
36+
bool preformatted) override;
3637

3738
virtual void flush(unsigned level) override;
3839
};
@@ -43,13 +44,15 @@ class gcc_message_handlert:public ui_message_handlert
4344
// aims to imitate the messages gcc prints
4445
virtual void print(
4546
unsigned level,
46-
const std::string &message) override;
47+
const std::string &message,
48+
bool preformatted) override;
4749

4850
virtual void print(
4951
unsigned level,
5052
const std::string &message,
5153
int sequence_number,
52-
const source_locationt &location) override;
54+
const source_locationt &location,
55+
bool preformatted) override;
5356
};
5457

5558
#endif // CPROVER_UTIL_COUT_MESSAGE_H

‎src/util/message.cpp

+5-3
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@ void message_handlert::print(
1313
unsigned level,
1414
const std::string &message,
1515
int sequence_number,
16-
const source_locationt &location)
16+
const source_locationt &location,
17+
bool preformatted)
1718
{
1819
std::string dest;
1920

@@ -51,12 +52,13 @@ void message_handlert::print(
5152
dest+=": ";
5253
dest+=message;
5354

54-
print(level, dest);
55+
print(level, dest, preformatted);
5556
}
5657

5758
void message_handlert::print(
5859
unsigned level,
59-
const std::string &message)
60+
const std::string &message,
61+
bool preformatted)
6062
{
6163
if(level>=message_count.size())
6264
message_count.resize(level+1, 0);

‎src/util/message.h

+33-11
Original file line numberDiff line numberDiff line change
@@ -23,13 +23,17 @@ class message_handlert
2323
{
2424
}
2525

26-
virtual void print(unsigned level, const std::string &message) = 0;
26+
virtual void print(
27+
unsigned level,
28+
const std::string &message,
29+
bool preformatted) = 0;
2730

2831
virtual void print(
2932
unsigned level,
3033
const std::string &message,
3134
int sequence_number,
32-
const source_locationt &location);
35+
const source_locationt &location,
36+
bool preformatted);
3337

3438
virtual void flush(unsigned level)
3539
{
@@ -59,18 +63,22 @@ class message_handlert
5963
class null_message_handlert:public message_handlert
6064
{
6165
public:
62-
virtual void print(unsigned level, const std::string &message)
66+
virtual void print(
67+
unsigned level,
68+
const std::string &message,
69+
bool preformatted)
6370
{
64-
message_handlert::print(level, message);
71+
message_handlert::print(level, message, preformatted);
6572
}
6673

6774
virtual void print(
6875
unsigned level,
6976
const std::string &message,
7077
int sequence_number,
71-
const source_locationt &location)
78+
const source_locationt &location,
79+
bool preformatted)
7280
{
73-
print(level, message);
81+
print(level, message, preformatted);
7482
}
7583
};
7684

@@ -81,9 +89,12 @@ class stream_message_handlert:public message_handlert
8189
{
8290
}
8391

84-
virtual void print(unsigned level, const std::string &message)
92+
virtual void print(
93+
unsigned level,
94+
const std::string &message,
95+
bool preformatted)
8596
{
86-
message_handlert::print(level, message);
97+
message_handlert::print(level, message, preformatted);
8798

8899
if(verbosity>=level)
89100
out << message << '\n';
@@ -157,20 +168,23 @@ class messaget
157168
unsigned _message_level,
158169
messaget &_message):
159170
message_level(_message_level),
160-
message(_message)
171+
message(_message),
172+
preformatted(false)
161173
{
162174
}
163175

164176
mstreamt(const mstreamt &other):
165177
message_level(other.message_level),
166178
message(other.message),
167-
source_location(other.source_location)
179+
source_location(other.source_location),
180+
preformatted(false)
168181
{
169182
}
170183

171184
unsigned message_level;
172185
messaget &message;
173186
source_locationt source_location;
187+
bool preformatted;
174188

175189
template <class T>
176190
mstreamt &operator << (const T &x)
@@ -196,15 +210,23 @@ class messaget
196210
m.message_level,
197211
m.str(),
198212
-1,
199-
m.source_location);
213+
m.source_location,
214+
m.preformatted);
200215
m.message.message_handler->flush(m.message_level);
201216
}
217+
m.preformatted=false;
202218
m.clear(); // clears error bits
203219
m.str(std::string()); // clears the string
204220
m.source_location.clear();
205221
return m;
206222
}
207223

224+
static mstreamt &preformatted_output(mstreamt &m)
225+
{
226+
m.preformatted=true;
227+
return m;
228+
}
229+
208230
// in lieu of std::endl
209231
static mstreamt &endl(mstreamt &m)
210232
{

‎src/util/ui_message.cpp

+31-12
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,8 @@ const char *ui_message_handlert::level_string(unsigned level)
8989

9090
void ui_message_handlert::print(
9191
unsigned level,
92-
const std::string &message)
92+
const std::string &message,
93+
bool preformatted)
9394
{
9495
if(verbosity>=level)
9596
{
@@ -98,7 +99,7 @@ void ui_message_handlert::print(
9899
case uit::PLAIN:
99100
{
100101
console_message_handlert console_message_handler;
101-
console_message_handler.print(level, message);
102+
console_message_handler.print(level, message, preformatted);
102103
}
103104
break;
104105

@@ -107,7 +108,7 @@ void ui_message_handlert::print(
107108
{
108109
source_locationt location;
109110
location.make_nil();
110-
print(level, message, -1, location);
111+
print(level, message, -1, location, preformatted);
111112
}
112113
break;
113114
}
@@ -118,17 +119,18 @@ void ui_message_handlert::print(
118119
unsigned level,
119120
const std::string &message,
120121
int sequence_number,
121-
const source_locationt &location)
122+
const source_locationt &location,
123+
bool preformatted)
122124
{
123-
message_handlert::print(level, message);
125+
message_handlert::print(level, message, preformatted);
124126

125127
if(verbosity>=level)
126128
{
127129
switch(get_ui())
128130
{
129131
case uit::PLAIN:
130132
message_handlert::print(
131-
level, message, sequence_number, location);
133+
level, message, sequence_number, location, preformatted);
132134
break;
133135

134136
case uit::XML_UI:
@@ -144,7 +146,7 @@ void ui_message_handlert::print(
144146
std::string sequence_number_str=
145147
sequence_number>=0?std::to_string(sequence_number):"";
146148

147-
ui_msg(type, tmp_message, sequence_number_str, location);
149+
ui_msg(type, tmp_message, sequence_number_str, location, preformatted);
148150
}
149151
break;
150152
}
@@ -155,19 +157,20 @@ void ui_message_handlert::ui_msg(
155157
const std::string &type,
156158
const std::string &msg1,
157159
const std::string &msg2,
158-
const source_locationt &location)
160+
const source_locationt &location,
161+
bool preformatted)
159162
{
160163
switch(get_ui())
161164
{
162165
case uit::PLAIN:
163166
break;
164167

165168
case uit::XML_UI:
166-
xml_ui_msg(type, msg1, msg2, location);
169+
xml_ui_msg(type, msg1, msg2, location, preformatted);
167170
break;
168171

169172
case uit::JSON_UI:
170-
json_ui_msg(type, msg1, msg2, location);
173+
json_ui_msg(type, msg1, msg2, location, preformatted);
171174
break;
172175
}
173176
}
@@ -176,8 +179,16 @@ void ui_message_handlert::xml_ui_msg(
176179
const std::string &type,
177180
const std::string &msg1,
178181
const std::string &msg2,
179-
const source_locationt &location)
182+
const source_locationt &location,
183+
bool preformatted)
180184
{
185+
if(preformatted)
186+
{
187+
// Expect the message is already an XML fragment.
188+
std::cout << msg1 << '\n';
189+
return;
190+
}
191+
181192
xmlt result;
182193
result.name="message";
183194

@@ -196,8 +207,16 @@ void ui_message_handlert::json_ui_msg(
196207
const std::string &type,
197208
const std::string &msg1,
198209
const std::string &msg2,
199-
const source_locationt &location)
210+
const source_locationt &location,
211+
bool preformatted)
200212
{
213+
if(preformatted)
214+
{
215+
// Expect the message is already a JSON fragment.
216+
std::cout << ",\n" << msg1;
217+
return;
218+
}
219+
201220
json_objectt result;
202221

203222
#if 0

‎src/util/ui_message.h

+10-5
Original file line numberDiff line numberDiff line change
@@ -44,32 +44,37 @@ class ui_message_handlert:public message_handlert
4444
// overloading
4545
virtual void print(
4646
unsigned level,
47-
const std::string &message);
47+
const std::string &message,
48+
bool preformatted);
4849

4950
// overloading
5051
virtual void print(
5152
unsigned level,
5253
const std::string &message,
5354
int sequence_number,
54-
const source_locationt &location);
55+
const source_locationt &location,
56+
bool preformatted);
5557

5658
virtual void xml_ui_msg(
5759
const std::string &type,
5860
const std::string &msg1,
5961
const std::string &msg2,
60-
const source_locationt &location);
62+
const source_locationt &location,
63+
bool preformatted);
6164

6265
virtual void json_ui_msg(
6366
const std::string &type,
6467
const std::string &msg1,
6568
const std::string &msg2,
66-
const source_locationt &location);
69+
const source_locationt &location,
70+
bool preformatted);
6771

6872
virtual void ui_msg(
6973
const std::string &type,
7074
const std::string &msg1,
7175
const std::string &msg2,
72-
const source_locationt &location);
76+
const source_locationt &location,
77+
bool preformatted);
7378

7479
const char *level_string(unsigned level);
7580
};

0 commit comments

Comments
 (0)