Demote goto/destructor interaction to debug message level

tautschnig · tautschnig · commit b7c7e8f2e78e · 2017-05-29T16:40:34.000+01:00
Compilation using goto-cc used to be very noisy. Added source location
information to make messages more comprehensible.
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
@@ -215,17 +215,19 @@ void goto_convertt::finish_gotos(goto_programt &dest)
 
       if(!stack_is_prefix)
       {
-        warning() << "Encountered goto (" << goto_label <<
-          ") that enters one or more lexical blocks;" <<
-          "omitting constructors and destructors." << eom;
+          debug().source_location=i.code.find_source_location();
+          debug() << "encountered goto `" << goto_label
+                  << "' that enters one or more lexical blocks; "
+                  << "omitting constructors and destructors" << eom;
       }
       else
       {
         auto unwind_to_size=label_stack.size();
         if(unwind_to_size<goto_stack.size())
         {
-          status() << "Adding goto-destructor code on jump to " <<
-            goto_label << eom;
+          debug().source_location=i.code.find_source_location();
+          debug() << "adding goto-destructor code on jump to `"
+                  << goto_label << "'" << eom;
           goto_programt destructor_code;
           unwind_destructor_stack(
             i.code.add_source_location(),

Original file line number	Diff line number	Diff line change
`@@ -215,17 +215,19 @@ void goto_convertt::finish_gotos(goto_programt &dest)`
`215`	`215`
`216`	`216`	`if(!stack_is_prefix)`
`217`	`217`	`{`
`218`		`- warning() << "Encountered goto (" << goto_label <<`
`219`		`- ") that enters one or more lexical blocks;" <<`
`220`		`- "omitting constructors and destructors." << eom;`
	`218`	`+ debug().source_location=i.code.find_source_location();`
	`219`	+ debug() << "encountered goto `" << goto_label
	`220`	`+ << "' that enters one or more lexical blocks; "`
	`221`	`+ << "omitting constructors and destructors" << eom;`
`221`	`222`	`}`
`222`	`223`	`else`
`223`	`224`	`{`
`224`	`225`	`auto unwind_to_size=label_stack.size();`
`225`	`226`	`if(unwind_to_size<goto_stack.size())`
`226`	`227`	`{`
`227`		`- status() << "Adding goto-destructor code on jump to " <<`
`228`		`- goto_label << eom;`
	`228`	`+ debug().source_location=i.code.find_source_location();`
	`229`	+ debug() << "adding goto-destructor code on jump to `"
	`230`	`+ << goto_label << "'" << eom;`
`229`	`231`	`goto_programt destructor_code;`
`230`	`232`	`unwind_destructor_stack(`
`231`	`233`	`i.code.add_source_location(),`