unwindset: Also warn about loops in functions without body

f14cd09 demoted some failures to warnings. This commit does so for
another case: if no body for the function is available, issue a warning
rather than failing an exception.

This situation will typically arise when using an unwindset
specification originally meant for CBMC with goto-instrument, where
library functions might not yet be present.

Author: tautschnig

src/goto-instrument/unwindset.cpp

@@ -71,12 +71,21 @@ void unwindsett::parse_unwindset_one_loop(
       std::string function_id = id.substr(0, last_dot_pos);
       std::string loop_nr_label = id.substr(last_dot_pos + 1);
 
-      if(loop_nr_label.empty() || !goto_model.can_produce_function(function_id))
+      if(loop_nr_label.empty())
       {
         throw invalid_command_line_argument_exceptiont{
           "invalid loop identifier " + id, "unwindset"};
       }
 
+      if(!goto_model.can_produce_function(function_id))
+      {
+        messaget log{message_handler};
+        log.warning() << "loop identifier " << id
+                      << " for non-existent function provided with unwindset"
+                      << messaget::eom;
+        return;
+      }
+
       const goto_functiont &goto_function =
         goto_model.get_goto_function(function_id);
       if(isdigit(loop_nr_label[0]))