Mark GOTO instructions with unresolved virtual calls

Matthias Güdemann · Matthias Güdemann · commit 04f2faf29196 · 2018-01-03T15:48:17.000+01:00
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
@@ -192,6 +192,9 @@ void remove_virtual_functionst::remove_virtual_function(
       {
         // No definition for this type; shouldn't be possible...
         t1->make_assertion(false_exprt());
+        t1->source_location.set_comment(
+          ("cannot find calls for " +
+           id2string(code.function().get(ID_identifier))));
       }
       insertit.first->second=t1;
       // goto final

Original file line number	Diff line number	Diff line change
`@@ -192,6 +192,9 @@ void remove_virtual_functionst::remove_virtual_function(`
`192`	`192`	`{`
`193`	`193`	`// No definition for this type; shouldn't be possible...`
`194`	`194`	`t1->make_assertion(false_exprt());`
	`195`	`+ t1->source_location.set_comment(`
	`196`	`+ ("cannot find calls for " +`
	`197`	`+ id2string(code.function().get(ID_identifier))));`
`195`	`198`	`}`
`196`	`199`	`insertit.first->second=t1;`
`197`	`200`	`// goto final`