@@ -68,34 +68,37 @@ bool compilet::doit()
68
68
{
69
69
if (!find_library (library))
70
70
// GCC is going to complain if this doesn't exist
71
- debug () << " Library not found: " << library << " (ignoring)" << eom;
71
+ log.debug () << " Library not found: " << library << " (ignoring)"
72
+ << messaget::eom;
72
73
}
73
74
74
- statistics () << " No. of source files: " << source_files.size () << eom;
75
- statistics () << " No. of object files: " << object_files.size () << eom;
75
+ log.statistics () << " No. of source files: " << source_files.size ()
76
+ << messaget::eom;
77
+ log.statistics () << " No. of object files: " << object_files.size ()
78
+ << messaget::eom;
76
79
77
80
// Work through the given source files
78
81
79
82
if (source_files.empty () && object_files.empty ())
80
83
{
81
- error () << " no input files" << eom;
84
+ log. error () << " no input files" << messaget:: eom;
82
85
return true ;
83
86
}
84
87
85
88
if (mode==LINK_LIBRARY && !source_files.empty ())
86
89
{
87
- error () << " cannot link source files" << eom;
90
+ log. error () << " cannot link source files" << messaget:: eom;
88
91
return true ;
89
92
}
90
93
91
94
if (mode==PREPROCESS_ONLY && !object_files.empty ())
92
95
{
93
- error () << " cannot preprocess object files" << eom;
96
+ log. error () << " cannot preprocess object files" << messaget:: eom;
94
97
return true ;
95
98
}
96
99
97
- const unsigned warnings_before=
98
- get_message_handler ().get_message_count (messaget::M_WARNING);
100
+ const unsigned warnings_before =
101
+ log. get_message_handler ().get_message_count (messaget::M_WARNING);
99
102
100
103
auto symbol_table_opt = compile ();
101
104
if (!symbol_table_opt.has_value ())
@@ -109,10 +112,8 @@ bool compilet::doit()
109
112
return true ;
110
113
}
111
114
112
- return
113
- warning_is_fatal &&
114
- get_message_handler ().get_message_count (messaget::M_WARNING)!=
115
- warnings_before;
115
+ return warning_is_fatal && log.get_message_handler ().get_message_count (
116
+ messaget::M_WARNING) != warnings_before;
116
117
}
117
118
118
119
enum class file_typet
@@ -169,22 +170,23 @@ static file_typet detect_file_type(
169
170
// / \return false on success, true on error.
170
171
bool compilet::add_input_file (const std::string &file_name)
171
172
{
172
- switch (detect_file_type (file_name, get_message_handler ()))
173
+ switch (detect_file_type (file_name, log. get_message_handler ()))
173
174
{
174
175
case file_typet::FAILED_TO_OPEN_FILE:
175
- warning () << " failed to open file '" << file_name
176
- << " ': " << std::strerror (errno) << eom;
176
+ log. warning () << " failed to open file '" << file_name
177
+ << " ': " << std::strerror (errno) << messaget:: eom;
177
178
return warning_is_fatal; // generously ignore unless -Werror
178
179
179
180
case file_typet::UNKNOWN:
180
181
// unknown extension, not a goto binary, will silently ignore
181
- debug () << " unknown file type in '" << file_name << " '" << eom;
182
+ log.debug () << " unknown file type in '" << file_name << " '"
183
+ << messaget::eom;
182
184
return false ;
183
185
184
186
case file_typet::ELF_OBJECT:
185
187
// ELF file without goto-cc section, silently ignore
186
- debug () << " ELF object without goto-cc section: '" << file_name << " '"
187
- << eom;
188
+ log. debug () << " ELF object without goto-cc section: '" << file_name << " '"
189
+ << messaget:: eom;
188
190
return false ;
189
191
190
192
case file_typet::SOURCE_FILE:
@@ -225,7 +227,7 @@ bool compilet::add_files_from_archive(
225
227
run (" ar" , {" ar" , " x" , concat_dir_file (working_directory, file_name)});
226
228
if (ret != 0 )
227
229
{
228
- error () << " Failed to extract archive " << file_name << eom;
230
+ log. error () << " Failed to extract archive " << file_name << messaget:: eom;
229
231
return true ;
230
232
}
231
233
}
@@ -240,7 +242,7 @@ bool compilet::add_files_from_archive(
240
242
" " );
241
243
if (ret != 0 )
242
244
{
243
- error () << " Failed to list archive " << file_name << eom;
245
+ log. error () << " Failed to list archive " << file_name << messaget:: eom;
244
246
return true ;
245
247
}
246
248
@@ -251,10 +253,11 @@ bool compilet::add_files_from_archive(
251
253
{
252
254
std::string t = concat_dir_file (tstr, line);
253
255
254
- if (is_goto_binary (t, get_message_handler ()))
256
+ if (is_goto_binary (t, log. get_message_handler ()))
255
257
object_files.push_back (t);
256
258
else
257
- debug () << " Object file is not a goto binary: " << line << eom;
259
+ log.debug () << " Object file is not a goto binary: " << line
260
+ << messaget::eom;
258
261
}
259
262
260
263
if (!thin_archive)
@@ -282,14 +285,14 @@ bool compilet::find_library(const std::string &name)
282
285
{
283
286
library_file_name = concat_dir_file (library_path, " lib" + name + " .so" );
284
287
285
- switch (detect_file_type (library_file_name, get_message_handler ()))
288
+ switch (detect_file_type (library_file_name, log. get_message_handler ()))
286
289
{
287
290
case file_typet::GOTO_BINARY:
288
291
return !add_input_file (library_file_name);
289
292
290
293
case file_typet::ELF_OBJECT:
291
- warning () << " Warning: Cannot read ELF library " << library_file_name
292
- << eom;
294
+ log. warning () << " Warning: Cannot read ELF library "
295
+ << library_file_name << messaget:: eom;
293
296
return warning_is_fatal;
294
297
295
298
case file_typet::THIN_ARCHIVE:
@@ -310,7 +313,7 @@ bool compilet::find_library(const std::string &name)
310
313
bool compilet::link (optionalt<symbol_tablet> &&symbol_table)
311
314
{
312
315
// "compile" hitherto uncompiled functions
313
- statistics () << " Compiling functions" << eom;
316
+ log. statistics () << " Compiling functions" << messaget:: eom;
314
317
goto_modelt goto_model;
315
318
if (symbol_table.has_value ())
316
319
goto_model.symbol_table = std::move (*symbol_table);
@@ -319,7 +322,7 @@ bool compilet::link(optionalt<symbol_tablet> &&symbol_table)
319
322
// parse object files
320
323
for (const auto &file_name : object_files)
321
324
{
322
- if (read_object_and_link (file_name, goto_model, get_message_handler ()))
325
+ if (read_object_and_link (file_name, goto_model, log. get_message_handler ()))
323
326
return true ;
324
327
}
325
328
@@ -338,7 +341,7 @@ bool compilet::link(optionalt<symbol_tablet> &&symbol_table)
338
341
339
342
const bool error = ansi_c_entry_point (
340
343
goto_model.symbol_table ,
341
- get_message_handler (),
344
+ log. get_message_handler (),
342
345
c_object_factory_parameterst ());
343
346
344
347
if (error)
@@ -351,7 +354,7 @@ bool compilet::link(optionalt<symbol_tablet> &&symbol_table)
351
354
if (keep_file_local)
352
355
{
353
356
function_name_manglert<file_name_manglert> mangler (
354
- get_message_handler (), goto_model, file_local_mangle_suffix);
357
+ log. get_message_handler (), goto_model, file_local_mangle_suffix);
355
358
mangler.mangle ();
356
359
}
357
360
@@ -389,7 +392,7 @@ optionalt<symbol_tablet> compilet::compile()
389
392
std::ifstream in (file_name, std::ios::binary);
390
393
std::ofstream out (debug_outfile, std::ios::binary);
391
394
out << in.rdbuf ();
392
- warning () << " Failed sources in " << debug_outfile << eom;
395
+ log. warning () << " Failed sources in " << debug_outfile << messaget:: eom;
393
396
}
394
397
395
398
return {}; // parser/typecheck error
@@ -422,7 +425,7 @@ optionalt<symbol_tablet> compilet::compile()
422
425
if (keep_file_local)
423
426
{
424
427
function_name_manglert<file_name_manglert> mangler (
425
- get_message_handler (), file_goto_model, file_local_mangle_suffix);
428
+ log. get_message_handler (), file_goto_model, file_local_mangle_suffix);
426
429
mangler.mangle ();
427
430
}
428
431
@@ -434,7 +437,7 @@ optionalt<symbol_tablet> compilet::compile()
434
437
}
435
438
else
436
439
{
437
- if (linking (symbol_table, *file_symbol_table, get_message_handler ()))
440
+ if (linking (symbol_table, *file_symbol_table, log. get_message_handler ()))
438
441
{
439
442
return {};
440
443
}
@@ -467,11 +470,12 @@ bool compilet::parse(
467
470
468
471
if (languagep==nullptr )
469
472
{
470
- error () << " failed to figure out type of file '" << file_name << " '" << eom;
473
+ log.error () << " failed to figure out type of file '" << file_name << " '"
474
+ << messaget::eom;
471
475
return true ;
472
476
}
473
477
474
- languagep->set_message_handler (get_message_handler ());
478
+ languagep->set_message_handler (log. get_message_handler ());
475
479
476
480
if (file_name == " -" )
477
481
return parse_stdin (*languagep);
@@ -484,7 +488,8 @@ bool compilet::parse(
484
488
485
489
if (!infile)
486
490
{
487
- error () << " failed to open input file '" << file_name << " '" << eom;
491
+ log.error () << " failed to open input file '" << file_name << " '"
492
+ << messaget::eom;
488
493
return true ;
489
494
}
490
495
@@ -493,7 +498,7 @@ bool compilet::parse(
493
498
494
499
if (mode==PREPROCESS_ONLY)
495
500
{
496
- statistics () << " Preprocessing: " << file_name << eom;
501
+ log. statistics () << " Preprocessing: " << file_name << messaget:: eom;
497
502
498
503
std::ostream *os = &std::cout;
499
504
std::ofstream ofs;
@@ -505,8 +510,8 @@ bool compilet::parse(
505
510
506
511
if (!ofs.is_open ())
507
512
{
508
- error () << " failed to open output file '" << cmdline.get_value (' o' )
509
- << " '" << eom;
513
+ log. error () << " failed to open output file '" << cmdline.get_value (' o' )
514
+ << " '" << messaget:: eom;
510
515
return true ;
511
516
}
512
517
}
@@ -515,11 +520,11 @@ bool compilet::parse(
515
520
}
516
521
else
517
522
{
518
- statistics () << " Parsing: " << file_name << eom;
523
+ log. statistics () << " Parsing: " << file_name << messaget:: eom;
519
524
520
525
if (lf.language ->parse (infile, file_name))
521
526
{
522
- error () << " PARSING ERROR" << eom;
527
+ log. error () << " PARSING ERROR" << messaget:: eom;
523
528
return true ;
524
529
}
525
530
}
@@ -533,7 +538,7 @@ bool compilet::parse(
533
538
// / \return true on error, false otherwise
534
539
bool compilet::parse_stdin (languaget &language)
535
540
{
536
- statistics () << " Parsing: (stdin)" << eom;
541
+ log. statistics () << " Parsing: (stdin)" << messaget:: eom;
537
542
538
543
if (mode==PREPROCESS_ONLY)
539
544
{
@@ -547,8 +552,8 @@ bool compilet::parse_stdin(languaget &language)
547
552
548
553
if (!ofs.is_open ())
549
554
{
550
- error () << " failed to open output file '" << cmdline.get_value (' o' )
551
- << " '" << eom;
555
+ log. error () << " failed to open output file '" << cmdline.get_value (' o' )
556
+ << " '" << messaget:: eom;
552
557
return true ;
553
558
}
554
559
}
@@ -559,7 +564,7 @@ bool compilet::parse_stdin(languaget &language)
559
564
{
560
565
if (language.parse (std::cin, " " ))
561
566
{
562
- error () << " PARSING ERROR" << eom;
567
+ log. error () << " PARSING ERROR" << messaget:: eom;
563
568
return true ;
564
569
}
565
570
}
@@ -616,7 +621,7 @@ bool compilet::write_bin_object_file(
616
621
optionalt<symbol_tablet> compilet::parse_source (const std::string &file_name)
617
622
{
618
623
language_filest language_files;
619
- language_files.set_message_handler (get_message_handler ());
624
+ language_files.set_message_handler (log. get_message_handler ());
620
625
621
626
if (parse (file_name, language_files))
622
627
return {};
@@ -625,13 +630,13 @@ optionalt<symbol_tablet> compilet::parse_source(const std::string &file_name)
625
630
symbol_tablet file_symbol_table;
626
631
if (language_files.typecheck (file_symbol_table, keep_file_local))
627
632
{
628
- error () << " CONVERSION ERROR" << eom;
633
+ log. error () << " CONVERSION ERROR" << messaget:: eom;
629
634
return {};
630
635
}
631
636
632
637
if (language_files.final (file_symbol_table))
633
638
{
634
- error () << " CONVERSION ERROR" << eom;
639
+ log. error () << " CONVERSION ERROR" << messaget:: eom;
635
640
return {};
636
641
}
637
642
@@ -641,7 +646,7 @@ optionalt<symbol_tablet> compilet::parse_source(const std::string &file_name)
641
646
// / constructor
642
647
// / \return nothing
643
648
compilet::compilet (cmdlinet &_cmdline, message_handlert &mh, bool Werror)
644
- : messaget (mh),
649
+ : log (mh),
645
650
cmdline(_cmdline),
646
651
warning_is_fatal(Werror),
647
652
keep_file_local(
@@ -657,9 +662,12 @@ compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
657
662
working_directory=get_current_working_directory ();
658
663
659
664
if (cmdline.isset (" export-function-local-symbols" ))
660
- warning () << " The `--export-function-local-symbols` flag is deprecated. "
661
- " Please use `--export-file-local-symbols` instead."
662
- << eom;
665
+ {
666
+ log.warning ()
667
+ << " The `--export-function-local-symbols` flag is deprecated. "
668
+ " Please use `--export-file-local-symbols` instead."
669
+ << messaget::eom;
670
+ }
663
671
}
664
672
665
673
// / cleans up temporary files
@@ -695,7 +703,7 @@ void compilet::convert_symbols(goto_modelt &goto_model)
695
703
symbol_table_buildert::wrap (goto_model.symbol_table );
696
704
697
705
goto_convert_functionst converter (
698
- symbol_table_builder, get_message_handler ());
706
+ symbol_table_builder, log. get_message_handler ());
699
707
700
708
// the compilation may add symbols!
701
709
@@ -722,7 +730,7 @@ void compilet::convert_symbols(goto_modelt &goto_model)
722
730
s_it->second .is_function () && !s_it->second .is_compiled () &&
723
731
s_it->second .value .is_not_nil ())
724
732
{
725
- debug () << " Compiling " << s_it->first << eom;
733
+ log. debug () << " Compiling " << s_it->first << messaget:: eom;
726
734
converter.convert_function (
727
735
s_it->first , goto_model.goto_functions .function_map [s_it->first ]);
728
736
symbol_table_builder.get_writeable_ref (symbol).set_compiled ();
@@ -746,10 +754,12 @@ bool compilet::add_written_cprover_symbols(const symbol_tablet &symbol_table)
746
754
747
755
if (!inserted && old->second .type !=new_type)
748
756
{
749
- error () << " Incompatible CPROVER macro symbol types:" << eom
750
- << old->second .type .pretty () << " (at " << old->second .location
751
- << " )" << eom << " and" << eom << new_type.pretty ()
752
- << " (at " << pair.second .location << " )" << eom;
757
+ log.error () << " Incompatible CPROVER macro symbol types:" << ' \n '
758
+ << old->second .type .pretty () << " (at " << old->second .location
759
+ << " )\n "
760
+ << " and\n "
761
+ << new_type.pretty () << " (at " << pair.second .location << " )"
762
+ << messaget::eom;
753
763
return true ;
754
764
}
755
765
}
0 commit comments