Add validation methods to codet

Author: danpoe

src/util/std_code.h

@@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "expr.h"
 #include "expr_cast.h"
 #include "invariant.h"
+#include "validate.h"
+#include "validate_code.h"
 
 /// Data structure for representing an arbitrary statement in a program. Every
 /// specific type of statement (e.g. block of statements, assignment,
@@ -59,6 +61,49 @@ class codet:public exprt
   codet &last_statement();
   const codet &last_statement() const;
   class code_blockt &make_block();
+
+  /// Check that the code statement is well-formed (shallow checks only, i.e.,
+  /// enclosed statements, subexpressions, etc. are not checked)
+  ///
+  /// Subclasses may override this method to provide specific well-formedness
+  /// checks for the corresponding types.
+  ///
+  /// The validation mode indicates whether well-formedness check failures are
+  /// reported via DATA_INVARIANT violations or exceptions.
+  void check(const validation_modet vm = validation_modet::INVARIANT) const
+  {
+  }
+
+  /// Check that the code statement is well-formed, assuming that all its
+  /// enclosed statements, subexpressions, etc. have all ready been checked for
+  /// well-formedness.
+  ///
+  /// Subclasses may override this method to provide specific well-formedness
+  /// checks for the corresponding types.
+  ///
+  /// 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 = validation_modet::INVARIANT) const
+  {
+    check_code_pick(*this, vm);
+  }
+
+  /// Check that the code statement is well-formed (full check, including checks
+  /// of all subexpressions)
+  ///
+  /// Subclasses may override this method to provide specific well-formedness
+  /// checks for the corresponding types.
+  ///
+  /// The validation mode indicates whether well-formedness check failures are
+  /// reported via DATA_INVARIANT violations or exceptions.
+  void validate_full(
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    check_code_pick(*this, vm);
+  }
 };
 
 namespace detail // NOLINT