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: #6393

Author: tautschnig

regression/goto-instrument/generate-function-body-assert-false-assume-false/test.desc

@@ -5,4 +5,4 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 ^\[main.assertion.1\] .* assertion 0: SUCCESS$
-^\[crashes_program.assertion.1\] .* assertion false: FAILURE$
+^\[crashes_program.assertion.1\] .* undefined function should be unreachable: FAILURE$

regression/goto-instrument/generate-function-body-assert-false/test.desc

@@ -3,6 +3,6 @@ main.c
 --generate-function-body do_not_call_this --generate-function-body-options assert-false
 ^EXIT=10$
 ^SIGNAL=0$
-^\[do_not_call_this.assertion.1\] .* assertion false: FAILURE$
+^\[do_not_call_this.assertion.1\] .* undefined function should be unreachable: FAILURE$
 --
 ^warning: ignoring

regression/goto-instrument/generate-function-body/test.desc

@@ -5,4 +5,4 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 ^\[main.assertion.1\] .* assertion does_not_get_reached: SUCCESS$
-^\[should_be_generated.assertion.1\] .* assertion false: FAILURE$
+^\[should_be_generated.assertion.1\] .* undefined function should be unreachable: FAILURE$

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()));