Add validate() methods to (components of) goto models

Author: danpoe

src/goto-programs/goto_function.h

@@ -110,6 +110,16 @@ class goto_functiont
     parameter_identifiers = std::move(other.parameter_identifiers);
     return *this;
   }
+
+  /// 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 validate(const namespacet &ns, const validation_modet vm) const
+  {
+    body.validate(ns, vm);
+    validate_type_full_pick(type, ns, vm);
+  }
 };
 
 void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);

src/goto-programs/goto_functions.h

@@ -118,6 +118,19 @@ class goto_functionst
     for(const auto &fun : other.function_map)
       function_map[fun.first].copy_from(fun.second);
   }
+
+  /// Check that the goto functions are well-formed
+  ///
+  /// 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
+  {
+    for(const auto &entry : function_map)
+    {
+      const goto_functiont &goto_function = entry.second;
+      goto_function.validate(ns, vm);
+    }
+  }
 };
 
 #define Forall_goto_functions(it, functions) \

src/goto-programs/goto_model.h

@@ -95,6 +95,16 @@ class goto_modelt : public abstract_goto_modelt
     return goto_functions.function_map.find(id) !=
            goto_functions.function_map.end();
   }
+
+  /// Check that the goto model is well-formed
+  ///
+  /// 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
+  {
+    goto_functions.validate(ns, vm);
+    symbol_table.validate();
+  }
 };
 
 /// Class providing the abstract GOTO model interface onto an unrelated

src/goto-programs/goto_program.h

@@ -398,6 +398,16 @@ class goto_programt
     /// only be evaluated in the context of a goto_programt (see
     /// goto_programt::equals).
     bool equals(const instructiont &other) const;
+
+    /// Check that the instruction is well-formed
+    ///
+    /// 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
+    {
+      validate_code_full_pick(code, ns, vm);
+      validate_expr_full_pick(guard, ns, vm);
+    }
   };
 
   // Never try to change this to vector-we mutate the list while iterating
@@ -677,6 +687,18 @@ class goto_programt
   /// the same number of instructions, each pair of instructions compares equal,
   /// and relative jumps have the same distance.
   bool equals(const goto_programt &other) const;
+
+  /// Check that the goto program is well-formed
+  ///
+  /// 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
+  {
+    for(const instructiont &ins : instructions)
+    {
+      ins.validate(ns, vm);
+    }
+  }
 };
 
 /// Get control-flow successors of a given instruction. The instruction is

src/util/symbol_table.h

@@ -109,6 +109,10 @@ class symbol_tablet : public symbol_table_baset
   {
     return iteratort(internal_symbols.end());
   }
+
+  void validate() const
+  {
+  }
 };
 
 #endif // CPROVER_UTIL_SYMBOL_TABLE_H