Add INVARIANTs that goto declarations may not initialize

Initializations must be sepearated out of `code_declt` into a separate
assignment before adding to goto program. This is the case already.
These new INVARIANTs check that this continues to be true.

Author: thomasspriggs

src/goto-programs/goto_program.h

@@ -199,13 +199,21 @@ class goto_programt
     const code_declt &get_decl() const
     {
       PRECONDITION(is_decl());
-      return to_code_decl(code);
+      const auto &decl = expr_checked_cast<code_declt>(code);
+      INVARIANT(
+        !decl.initial_value(),
+        "code_declt in goto program may not contain initialization.");
+      return decl;
     }
 
     /// Set the declaration for DECL
     void set_decl(code_declt c)
     {
       PRECONDITION(is_decl());
+      INVARIANT(
+        !c.initial_value(),
+        "Initialization must be separated from code_declt before adding to "
+        "goto_instructiont.");
       code = std::move(c);
     }
 

src/util/std_code.h

@@ -422,6 +422,8 @@ class code_declt:public codet
 
   /// Returns the initial value to which the declared variable is initialized,
   /// or empty in the case where no initialisation is included.
+  /// \note: Initial values may be present in the front end but they must be
+  ///   separated into a separate assignment when used in a `goto_instructiont`.
   optionalt<exprt> initial_value() const
   {
     if(operands().size() < 2)
@@ -431,6 +433,8 @@ class code_declt:public codet
 
   /// Sets the value to which this declaration initializes the declared
   /// variable. Empty optional maybe passed to remove existing initialisation.
+  /// \note: Initial values may be present in the front end but they must be
+  ///   separated into a separate assignment when used in a `goto_instructiont`.
   void set_initial_value(optionalt<exprt> initial_value)
   {
     if(!initial_value)