Add check for well-formedness of assign instructions

Author: danpoe

src/goto-programs/goto_program.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <iomanip>
 
 #include <util/std_expr.h>
+#include <util/validate.h>
 
 #include <langapi/language_util.h>
 
@@ -668,6 +669,62 @@ bool goto_programt::instructiont::equals(const instructiont &other) const
   // clang-format on
 }
 
+void goto_programt::instructiont::validate(
+  const namespacet &ns,
+  const validation_modet vm) const
+{
+  validate_code_full_pick(code, ns, vm);
+  validate_expr_full_pick(guard, ns, vm);
+
+  switch(type)
+  {
+  case NO_INSTRUCTION_TYPE:
+    break;
+  case GOTO:
+    break;
+  case ASSUME:
+    break;
+  case ASSERT:
+    break;
+  case OTHER:
+    break;
+  case SKIP:
+    break;
+  case START_THREAD:
+    break;
+  case END_THREAD:
+    break;
+  case LOCATION:
+    break;
+  case END_FUNCTION:
+    break;
+  case ATOMIC_BEGIN:
+    break;
+  case ATOMIC_END:
+    break;
+  case RETURN:
+    break;
+  case ASSIGN:
+    DATA_CHECK(
+      code.get_statement() == ID_assign,
+      "assign instruction should contain an assign statement");
+    DATA_CHECK(targets.empty(), "assign instruction should not have a target");
+    break;
+  case DECL:
+    break;
+  case DEAD:
+    break;
+  case FUNCTION_CALL:
+    break;
+  case THROW:
+    break;
+  case CATCH:
+    break;
+  case INCOMPLETE_GOTO:
+    break;
+  }
+}
+
 bool goto_programt::equals(const goto_programt &other) const
 {
   if(instructions.size() != other.instructions.size())

src/goto-programs/goto_program.h

@@ -20,10 +20,12 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/invariant.h>
 #include <util/namespace.h>
-#include <util/symbol_table.h>
 #include <util/source_location.h>
-#include <util/std_expr.h>
 #include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+enum class validation_modet;
 
 /// The type of an instruction in a GOTO program.
 enum goto_program_instruction_typet
@@ -403,11 +405,7 @@ class goto_programt
     ///
     /// 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);
-    }
+    void validate(const namespacet &ns, const validation_modet vm) const;
   };
 
   // Never try to change this to vector-we mutate the list while iterating