Make sure code_typet always has parameters property

The existence of the parameters property may depend on
whether parameters() has been called or not, which can
lead to unexpectedly unequal instructions in goto programs.

Author: peterschrammel

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -295,9 +295,6 @@ static void create_clinit_wrapper_symbols(
   symbolt wrapper_method_symbol;
   code_typet wrapper_method_type;
   wrapper_method_type.return_type() = void_typet();
-  // Ensure the parameters property is there
-  // to avoid trouble in irept comparisons
-  wrapper_method_type.parameters();
   wrapper_method_symbol.name = clinit_wrapper_name(class_name);
   wrapper_method_symbol.pretty_name = wrapper_method_symbol.name;
   wrapper_method_symbol.base_name = "clinit_wrapper";

src/util/std_types.h

@@ -760,6 +760,9 @@ class code_typet:public typet
 public:
   code_typet():typet(ID_code)
   {
+    // make sure this property is always there to avoid problems
+    // with irept comparisons
+    add(ID_parameters);
   }
 
   // used to be argumentt -- now uses standard terminology