Generate-function-bodies: generate a meaningful assertion

When using --generate-function-body with "assert-false" or
"assert-false-assume-false" make sure we produce a more meaningful
description than "assertion false." Instead, make the comment say
"undefined function should be unreachable."

Fixes: diffblue#6393

Author: tautschnig

src/goto-instrument/generate_function_bodies.cpp

@@ -105,12 +105,8 @@ class assert_false_generate_function_bodiest : public generate_function_bodiest
     };
     auto assert_instruction =
       add_instruction(goto_programt::make_assertion(false_exprt()));
-    const namespacet ns(symbol_table);
-    std::ostringstream comment_stream;
-    comment_stream << id2string(ID_assertion) << " "
-                   << format(assert_instruction->condition());
     assert_instruction->source_location_nonconst().set_comment(
-      comment_stream.str());
+      "undefined function should be unreachable");
     assert_instruction->source_location_nonconst().set_property_class(
       ID_assertion);
     add_instruction(goto_programt::make_end_function());
@@ -136,12 +132,8 @@ class assert_false_then_assume_false_generate_function_bodiest
     };
     auto assert_instruction =
       add_instruction(goto_programt::make_assertion(false_exprt()));
-    const namespacet ns(symbol_table);
-    std::ostringstream comment_stream;
-    comment_stream << id2string(ID_assertion) << " "
-                   << format(assert_instruction->condition());
     assert_instruction->source_location_nonconst().set_comment(
-      comment_stream.str());
+      "undefined function should be unreachable");
     assert_instruction->source_location_nonconst().set_property_class(
       ID_assertion);
     add_instruction(goto_programt::make_assumption(false_exprt()));