Lazy goto model: support validation

This mirrors existing support in goto_modelt.

Author: smowton

src/goto-programs/abstract_goto_model.h

@@ -49,6 +49,12 @@ class abstract_goto_modelt
   /// underneath them, so this should only be used to lend a reference to code
   /// that cannot also call get_goto_function.
   virtual const symbol_tablet &get_symbol_table() const = 0;
+
+  /// 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.
+  virtual void validate(const validation_modet vm) const = 0;
 };
 
 #endif

src/goto-programs/goto_model.h

@@ -94,7 +94,7 @@ class goto_modelt : public abstract_goto_modelt
   ///
   /// The validation mode indicates whether well-formedness check failures are
   /// reported via DATA_INVARIANT violations or exceptions.
-  void validate(const validation_modet vm) const
+  void validate(const validation_modet vm) const override
   {
     symbol_table.validate(vm);
 
@@ -138,6 +138,18 @@ class wrapper_goto_modelt : public abstract_goto_modelt
            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 validation_modet vm) const override
+  {
+    symbol_table.validate(vm);
+
+    const namespacet ns(symbol_table);
+    goto_functions.validate(ns, vm);
+  }
+
 private:
   const symbol_tablet &symbol_table;
   const goto_functionst &goto_functions;

src/goto-programs/lazy_goto_model.h

@@ -243,6 +243,15 @@ class lazy_goto_modelt : public abstract_goto_modelt
     return goto_functions.at(id);
   }
 
+  /// 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 validation_modet vm) const override
+  {
+    goto_model->validate(vm);
+  }
+
 private:
   std::unique_ptr<goto_modelt> goto_model;