Address review comments - Kroening

Removed previously disabled checks:
Not every instruction has a code member - so removed checks that both 
instruction sourcelocation and code sourcelocation are set and identical
Remove also remaining check that every instruction have a non-nil 
sourcelocation as this would have to be optional (if enabled fails 
many regression tests). This also simplifies considerably the overall 
validation pass (removes much passing around of the options structure).

Removes check on function return type - this will be preserved (diffblue#4266)

goto_model::validate now has default parameters.

Minor fixes.

Author: Sonny Martin

src/goto-programs/goto_function.cpp

@@ -33,9 +33,8 @@ void get_local_identifiers(
 ///
 /// 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
+void goto_functiont::validate(const namespacet &ns, const validation_modet vm)
+  const
 {
   // function body must end with an END_FUNCTION instruction
   if(body_available())

src/goto-programs/goto_function.h

@@ -119,9 +119,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;
+  void validate(const namespacet &ns, const validation_modet vm) const;
 };
 
 void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);

src/goto-programs/goto_functions.h

@@ -111,9 +111,7 @@ class goto_functionst
   ///
   /// 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
+  void validate(const namespacet &ns, const validation_modet vm) const
   {
     for(const auto &entry : function_map)
     {

unit/goto-programs/goto_program_symbol_type_table_consistency.cpp

@@ -51,8 +51,7 @@ SCENARIO(
 
       THEN("The consistency check succeeds")
       {
-        goto_function.validate(
-          ns, validation_modet::INVARIANT);
+        goto_function.validate(ns, validation_modet::INVARIANT);
 
         REQUIRE(true);
       }
@@ -67,8 +66,7 @@ SCENARIO(
       THEN("The consistency check fails")
       {
         REQUIRE_THROWS_AS(
-          goto_function.validate(
-            ns, validation_modet::EXCEPTION),
+          goto_function.validate(ns, validation_modet::EXCEPTION),
           incorrect_goto_program_exceptiont);
       }
     }

unit/goto-programs/goto_program_table_consistency.cpp

@@ -49,8 +49,7 @@ SCENARIO(
       const namespacet ns(symbol_table);
       THEN("The consistency check succeeds")
       {
-        goto_function.validate(
-          ns, validation_modet::INVARIANT);
+        goto_function.validate(ns, validation_modet::INVARIANT);
         REQUIRE(true);
       }
     }
@@ -60,8 +59,7 @@ SCENARIO(
       THEN("The consistency check fails")
       {
         REQUIRE_THROWS_AS(
-          goto_function.validate(
-            ns, validation_modet::EXCEPTION),
+          goto_function.validate(ns, validation_modet::EXCEPTION),
           incorrect_goto_program_exceptiont);
       }
     }

unit/goto-programs/goto_program_validate.cpp

@@ -357,8 +357,7 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
       namespacet ns(goto_model.symbol_table);
 
       REQUIRE_THROWS_AS(
-        function_f.validate(
-          ns, validation_modet::EXCEPTION),
+        function_f.validate(ns, validation_modet::EXCEPTION),
         incorrect_goto_program_exceptiont);
     }
   }
@@ -372,8 +371,7 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
 
       namespacet ns(goto_model.symbol_table);
 
-      REQUIRE_NOTHROW(function_f.validate(
-        ns, validation_modet::EXCEPTION));
+      REQUIRE_NOTHROW(function_f.validate(ns, validation_modet::EXCEPTION));
     }
   }
 }