Skip to content

Commit 0b62971

Browse files
author
Daniel Kroening
authored
Merge pull request #166 from tautschnig/messaget
Migrate all uses of message_streamt to messaget
2 parents 7f8efa0 + c183996 commit 0b62971

33 files changed

+282
-232
lines changed

‎regression/ansi-c/message_handling1/main.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
int main()
2+
{
3+
goto bla;
4+
5+
for(int i=0; i<5; ++i)
6+
{
7+
bla: i=10;
8+
}
9+
}

‎regression/ansi-c/message_handling1/test.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--verbosity 2
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
encountered goto `bla' that enters one or more lexical blocks

‎src/ansi-c/ansi_c_typecheck.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,9 @@ bool ansi_c_typecheck(
7272
message_handlert &message_handler,
7373
const namespacet &ns)
7474
{
75+
const unsigned errors_before=
76+
message_handler.get_message_count(messaget::M_ERROR);
77+
7578
symbol_tablet symbol_table;
7679
ansi_c_parse_treet ansi_c_parse_tree;
7780

@@ -99,5 +102,5 @@ bool ansi_c_typecheck(
99102
ansi_c_typecheck.error() << e << messaget::eom;
100103
}
101104

102-
return ansi_c_typecheck.get_error_found();
105+
return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
103106
}

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -658,7 +658,7 @@ int cbmc_parse_optionst::get_goto_program(
658658

659659
language->set_message_handler(get_message_handler());
660660

661-
status("Parsing", filename);
661+
status() << "Parsing " << filename << eom;
662662

663663
if(language->parse(infile, filename))
664664
{

‎src/clobber/clobber_parse_options.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -326,7 +326,7 @@ bool clobber_parse_optionst::get_goto_program(
326326

327327
language->set_message_handler(get_message_handler());
328328

329-
status("Parsing", filename);
329+
status() << "Parsing " << filename << eom;
330330

331331
if(language->parse(infile, filename))
332332
{

‎src/cpp/cpp_typecheck.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -178,6 +178,9 @@ bool cpp_typecheck(
178178
message_handlert &message_handler,
179179
const namespacet &ns)
180180
{
181+
const unsigned errors_before=
182+
message_handler.get_message_count(messaget::M_ERROR);
183+
181184
symbol_tablet symbol_table;
182185
cpp_parse_treet cpp_parse_tree;
183186

@@ -204,7 +207,7 @@ bool cpp_typecheck(
204207
cpp_typecheck.error() << e << messaget::eom;
205208
}
206209

207-
return cpp_typecheck.get_error_found();
210+
return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
208211
}
209212

210213
/*******************************************************************\

‎src/goto-cc/armcc_mode.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ int armcc_modet::doit()
4646

4747
unsigned int verbosity=1;
4848

49-
compilet compiler(cmdline);
49+
compilet compiler(cmdline, message_handler, cmdline.isset("diag_error="));
5050

5151
#if 0
5252
bool act_as_ld=

‎src/goto-cc/as_mode.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -159,8 +159,7 @@ int as_modet::doit()
159159
config.set(cmdline);
160160

161161
// determine actions to be undertaken
162-
compilet compiler(cmdline);
163-
compiler.ui_message_handler.set_verbosity(verbosity);
162+
compilet compiler(cmdline, message_handler, cmdline.isset("fatal-warnings"));
164163

165164
if(cmdline.isset('b')) // as86 only
166165
{

‎src/goto-cc/compile.cpp

Lines changed: 22 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -121,6 +121,9 @@ bool compilet::doit()
121121
return true;
122122
}
123123

124+
const unsigned warnings_before=
125+
get_message_handler().get_message_count(messaget::M_WARNING);
126+
124127
if(source_files.size()>0)
125128
if(compile())
126129
return true;
@@ -133,7 +136,10 @@ bool compilet::doit()
133136
return true;
134137
}
135138

136-
return false;
139+
return
140+
warning_is_fatal &&
141+
get_message_handler().get_message_count(messaget::M_WARNING)!=
142+
warnings_before;
137143
}
138144

139145
/*******************************************************************\
@@ -156,8 +162,8 @@ bool compilet::add_input_file(const std::string &file_name)
156162
std::ifstream in(file_name);
157163
if(!in)
158164
{
159-
error() << "failed to open file `" << file_name << "'" << eom;
160-
return false; // generously ignore
165+
warning() << "failed to open file `" << file_name << "'" << eom;
166+
return warning_is_fatal; // generously ignore unless -Werror
161167
}
162168
}
163169

@@ -168,7 +174,7 @@ bool compilet::add_input_file(const std::string &file_name)
168174
// a file without extension; will ignore
169175
warning() << "input file `" << file_name
170176
<< "' has no extension, not considered" << eom;
171-
return false;
177+
return warning_is_fatal;
172178
}
173179

174180
std::string ext = file_name.substr(r+1, file_name.length());
@@ -329,7 +335,7 @@ bool compilet::find_library(const std::string &name)
329335
else if(is_elf_file(libname))
330336
{
331337
warning() << "Warning: Cannot read ELF library " << libname << eom;
332-
return false;
338+
return warning_is_fatal;
333339
}
334340
}
335341
}
@@ -383,7 +389,7 @@ Function: compilet::link
383389
bool compilet::link()
384390
{
385391
// "compile" hitherto uncompiled functions
386-
print(8, "Compiling functions");
392+
statistics() << "Compiling functions" << eom;
387393
convert_symbols(compiled_functions);
388394

389395
// parse object files
@@ -409,7 +415,7 @@ bool compilet::link()
409415
symbol_table.remove(goto_functionst::entry_point());
410416
compiled_functions.function_map.erase(goto_functionst::entry_point());
411417

412-
if(ansi_c_entry_point(symbol_table, "main", ui_message_handler))
418+
if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
413419
return true;
414420

415421
// entry_point may (should) add some more functions.
@@ -554,7 +560,7 @@ bool compilet::parse(const std::string &file_name)
554560

555561
if(mode==PREPROCESS_ONLY)
556562
{
557-
print(8, "Preprocessing: "+file_name);
563+
statistics() << "Preprocessing: " << file_name << eom;
558564

559565
std::ostream *os = &std::cout;
560566
std::ofstream ofs;
@@ -576,7 +582,7 @@ bool compilet::parse(const std::string &file_name)
576582
}
577583
else
578584
{
579-
print(8, "Parsing: "+file_name);
585+
statistics() << "Parsing: " << file_name << eom;
580586

581587
if(language.parse(infile, file_name))
582588
{
@@ -608,7 +614,7 @@ bool compilet::parse_stdin()
608614

609615
language.set_message_handler(get_message_handler());
610616

611-
print(8, "Parsing: (stdin)");
617+
statistics() << "Parsing: (stdin)" << eom;
612618

613619
if(mode==PREPROCESS_ONLY)
614620
{
@@ -752,11 +758,11 @@ Function: compilet::compilet
752758
753759
\*******************************************************************/
754760

755-
compilet::compilet(cmdlinet &_cmdline):
756-
language_uit(_cmdline, ui_message_handler),
757-
ui_message_handler(_cmdline, "goto-cc " CBMC_VERSION),
761+
compilet::compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror):
762+
language_uit(_cmdline, mh),
758763
ns(symbol_table),
759-
cmdline(_cmdline)
764+
cmdline(_cmdline),
765+
warning_is_fatal(Werror)
760766
{
761767
mode=COMPILE_LINK_EXECUTABLE;
762768
echo_file_name=false;
@@ -842,7 +848,7 @@ Function: compilet::convert_symbols
842848

843849
void compilet::convert_symbols(goto_functionst &dest)
844850
{
845-
goto_convert_functionst converter(symbol_table, dest, ui_message_handler);
851+
goto_convert_functionst converter(symbol_table, dest, get_message_handler());
846852

847853
// the compilation may add symbols!
848854

@@ -872,7 +878,7 @@ void compilet::convert_symbols(goto_functionst &dest)
872878
s_it->second.value.id()!="compiled" &&
873879
s_it->second.value.is_not_nil())
874880
{
875-
print(9, "Compiling "+id2string(s_it->first));
881+
debug() << "Compiling " << s_it->first << eom;
876882
converter.convert_function(s_it->first);
877883
s_it->second.value=exprt("compiled");
878884
}

‎src/goto-cc/compile.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@ Date: June 2006
2020
class compilet:public language_uit
2121
{
2222
public:
23-
ui_message_handlert ui_message_handler;
2423
namespacet ns;
2524
goto_functionst compiled_functions;
2625
bool echo_file_name;
@@ -45,7 +44,7 @@ class compilet:public language_uit
4544
std::string object_file_extension;
4645
std::string output_file_object, output_file_executable;
4746

48-
explicit compilet(cmdlinet &_cmdline);
47+
compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror);
4948

5049
~compilet();
5150

@@ -72,6 +71,7 @@ class compilet:public language_uit
7271

7372
protected:
7473
cmdlinet &cmdline;
74+
bool warning_is_fatal;
7575

7676
unsigned function_body_count(const goto_functionst &);
7777

‎src/goto-cc/cw_mode.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ int cw_modet::doit()
4646

4747
unsigned int verbosity=1;
4848

49-
compilet compiler(cmdline);
49+
compilet compiler(cmdline, message_handler, cmdline.isset("Werror"));
5050

5151
#if 0
5252
bool act_as_ld=

‎src/goto-cc/gcc_mode.cpp

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -353,7 +353,7 @@ int gcc_modet::doit()
353353
return EX_OK;
354354
}
355355

356-
if(cmdline.isset("Wall"))
356+
if(cmdline.isset("Wall") || cmdline.isset("Wextra"))
357357
verbosity=2;
358358

359359
if(cmdline.isset("verbosity"))
@@ -483,8 +483,11 @@ int gcc_modet::doit()
483483
config.ansi_c.double_width=config.ansi_c.single_width;
484484

485485
// determine actions to be undertaken
486-
compilet compiler(cmdline);
487-
compiler.set_message_handler(get_message_handler());
486+
compilet compiler(cmdline,
487+
gcc_message_handler,
488+
cmdline.isset("Werror") &&
489+
cmdline.isset("Wextra") &&
490+
!cmdline.isset("Wno-error"));
488491

489492
if(act_as_ld)
490493
compiler.mode=compilet::LINK_LIBRARY;

‎src/goto-cc/ms_cl_mode.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ int ms_cl_modet::doit()
5959

6060
unsigned int verbosity=1;
6161

62-
compilet compiler(cmdline);
62+
compilet compiler(cmdline, message_handler, cmdline.isset("WX"));
6363

6464
#if 0
6565
bool act_as_ld=

‎src/goto-programs/goto_convert.cpp

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2866,6 +2866,9 @@ void goto_convert(
28662866
goto_programt &dest,
28672867
message_handlert &message_handler)
28682868
{
2869+
const unsigned errors_before=
2870+
message_handler.get_message_count(messaget::M_ERROR);
2871+
28692872
goto_convertt goto_convert(symbol_table, message_handler);
28702873

28712874
try
@@ -2876,20 +2879,20 @@ void goto_convert(
28762879
catch(int)
28772880
{
28782881
goto_convert.error();
2879-
throw 0;
28802882
}
28812883

28822884
catch(const char *e)
28832885
{
28842886
goto_convert.error() << e << messaget::eom;
2885-
throw 0;
28862887
}
28872888

28882889
catch(const std::string &e)
28892890
{
28902891
goto_convert.error() << e << messaget::eom;
2891-
throw 0;
28922892
}
2893+
2894+
if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
2895+
throw 0;
28932896
}
28942897

28952898
/*******************************************************************\

‎src/goto-programs/goto_convert_functions.cpp

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -330,6 +330,9 @@ void goto_convert(
330330
goto_functionst &functions,
331331
message_handlert &message_handler)
332332
{
333+
const unsigned errors_before=
334+
message_handler.get_message_count(messaget::M_ERROR);
335+
333336
goto_convert_functionst goto_convert_functions(
334337
symbol_table, functions, message_handler);
335338

@@ -341,20 +344,20 @@ void goto_convert(
341344
catch(int)
342345
{
343346
goto_convert_functions.error();
344-
throw 0;
345347
}
346348

347349
catch(const char *e)
348350
{
349351
goto_convert_functions.error() << e << messaget::eom;
350-
throw 0;
351352
}
352353

353354
catch(const std::string &e)
354355
{
355356
goto_convert_functions.error() << e << messaget::eom;
356-
throw 0;
357357
}
358+
359+
if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
360+
throw 0;
358361
}
359362

360363
/*******************************************************************\
@@ -375,6 +378,9 @@ void goto_convert(
375378
goto_functionst &functions,
376379
message_handlert &message_handler)
377380
{
381+
const unsigned errors_before=
382+
message_handler.get_message_count(messaget::M_ERROR);
383+
378384
goto_convert_functionst goto_convert_functions(
379385
symbol_table, functions, message_handler);
380386

@@ -386,18 +392,18 @@ void goto_convert(
386392
catch(int)
387393
{
388394
goto_convert_functions.error();
389-
throw 0;
390395
}
391396

392397
catch(const char *e)
393398
{
394399
goto_convert_functions.error() << e << messaget::eom;
395-
throw 0;
396400
}
397401

398402
catch(const std::string &e)
399403
{
400404
goto_convert_functions.error() << e << messaget::eom;
401-
throw 0;
402405
}
406+
407+
if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
408+
throw 0;
403409
}

‎src/goto-programs/initialize_goto_model.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,10 @@ bool initialize_goto_model(
9191

9292
if(lf.language==NULL)
9393
{
94-
msg.error("failed to figure out type of file", filename);
94+
source_locationt location;
95+
location.set_file(filename);
96+
msg.error().source_location=location;
97+
msg.error() << "failed to figure out type of file" << messaget::eom;
9598
return true;
9699
}
97100

0 commit comments

Comments
 (0)