Correct validation check for return statements from void functions

Author: chrisr-diffblue

src/goto-programs/goto_function.cpp

@@ -31,3 +31,36 @@ void get_local_identifiers(
       dest.insert(identifier);
   }
 }
+
+/// Check that the goto function is well-formed
+///
+/// The validation mode indicates whether well-formedness check failures are
+/// reported via DATA_INVARIANT violations or exceptions.
+void goto_functiont::validate(const namespacet &ns, const validation_modet vm)
+  const
+{
+  body.validate(ns, vm);
+
+  find_symbols_sett typetags;
+  find_type_symbols(type, typetags);
+  const symbolt *symbol;
+  for(const auto &identifier : typetags)
+  {
+    DATA_CHECK(
+      vm, !ns.lookup(identifier, symbol), id2string(identifier) + " not found");
+  }
+
+  // Check that a void function does not contain any RETURN instructions
+  if(to_code_type(type).return_type().id() == ID_empty)
+  {
+    forall_goto_program_instructions(instruction, body)
+    {
+      DATA_CHECK(
+        vm,
+        !instruction->is_return(),
+        "void function should not return a value");
+    }
+  }
+
+  validate_full_type(type, ns, vm);
+}

src/goto-programs/goto_function.h

@@ -116,23 +116,7 @@ class goto_functiont
   ///
   /// The validation mode indicates whether well-formedness check failures are
   /// reported via DATA_INVARIANT violations or exceptions.
-  void validate(const namespacet &ns, const validation_modet vm) const
-  {
-    body.validate(ns, vm);
-
-    find_symbols_sett typetags;
-    find_type_symbols(type, typetags);
-    const symbolt *symbol;
-    for(const auto &identifier : typetags)
-    {
-      DATA_CHECK(
-        vm,
-        !ns.lookup(identifier, symbol),
-        id2string(identifier) + " not found");
-    }
-
-    validate_full_type(type, ns, vm);
-  }
+  void validate(const namespacet &ns, const validation_modet vm) const;
 };
 
 void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);

src/util/std_code.h

@@ -1135,12 +1135,7 @@ class code_function_callt:public codet
   {
     check(code, vm);
 
-    if(code.op0().id() == ID_nil)
-      DATA_CHECK(
-        vm,
-        to_code_type(code.op1().type()).return_type().id() == ID_empty,
-        "void function should not return value");
-    else
+    if(code.op0().id() != ID_nil)
       DATA_CHECK(
         vm,
         base_type_eq(