Merge pull request #2288 from peterschrammel/code-type-const

peterschrammel · web-flow · commit 260156f8130c · 2018-06-06T21:19:50.000+01:00
Make code_typet declarations const
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -765,7 +765,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     this_param.set_base_name("this");
     this_param.set_this();
     this_param.type()=java_reference_type(symbol_type);
-    code_typet clone_type({this_param}, java_lang_object_type());
+    const code_typet clone_type({this_param}, java_lang_object_type());
 
     parameter_symbolt this_symbol;
     this_symbol.name=this_param.get_identifier();
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -31,8 +31,7 @@ static void create_initialize(symbol_table_baset &symbol_table)
   initialize.base_name=INITIALIZE_FUNCTION;
   initialize.mode=ID_java;
 
-  code_typet type({}, empty_typet());
-  initialize.type=type;
+  initialize.type = code_typet({}, empty_typet());
 
   code_blockt init_code;
 
@@ -687,10 +686,8 @@ bool generate_java_start_function(
   // we just built and register it in the symbol table
   symbolt new_symbol;
 
-  code_typet main_type({}, empty_typet());
-
   new_symbol.name=goto_functionst::entry_point();
-  new_symbol.type.swap(main_type);
+  new_symbol.type = code_typet({}, empty_typet());
   new_symbol.value.swap(init_code);
   new_symbol.mode=ID_java;
 
diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -293,7 +293,7 @@ static void create_clinit_wrapper_symbols(
 
   // Create symbol for the "clinit_wrapper"
   symbolt wrapper_method_symbol;
-  code_typet wrapper_method_type({}, void_typet());
+  const code_typet wrapper_method_type({}, void_typet());
   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";
@@ -713,7 +713,7 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
       "a class cannot be both incomplete, and so have stub static fields, and "
       "also define a static initializer");
 
-    code_typet thunk_type({}, void_typet());
+    const code_typet thunk_type({}, void_typet());
 
     symbolt static_init_symbol;
     static_init_symbol.name = static_init_name;
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -1611,7 +1611,7 @@ codet java_string_library_preprocesst::make_object_get_class_code(
     "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;");
   fun_call.lhs()=class1;
   fun_call.arguments().push_back(string1);
-  code_typet fun_type({code_typet::parametert(string_ptr_type)}, class_type);
+  const code_typet fun_type({code_typet::parametert(string_ptr_type)}, class_type);
   fun_call.function().type()=fun_type;
   code.add(fun_call, loc);
 
diff --git a/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp b/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp
@@ -58,7 +58,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
     const symbol_exprt lhs("lhs", unsignedbv_typet(32));
     const symbol_exprt lhs2("lhs2", unsignedbv_typet(32));
     const symbol_exprt lhs3("lhs3", unsignedbv_typet(32));
-    code_typet fun_type(
+    const code_typet fun_type(
       {code_typet::parametert(length_type()),
        code_typet::parametert(pointer_type(java_char_type())),
        code_typet::parametert(string_type),
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
@@ -445,10 +445,8 @@ bool generate_ansi_c_start_function(
   // add the entry point symbol
   symbolt new_symbol;
 
-  code_typet main_type({}, empty_typet());
-
   new_symbol.name=goto_functionst::entry_point();
-  new_symbol.type.swap(main_type);
+  new_symbol.type = code_typet({}, empty_typet());
   new_symbol.value.swap(init_code);
   new_symbol.mode=symbol.mode;
 
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -450,7 +450,7 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
   typet arg_type=expr.type();
   typecheck_type(arg_type);
 
-  code_typet new_type(
+  const code_typet new_type(
     {code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type));
 
   assert(expr.operands().size()==1);
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
@@ -1479,7 +1479,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t(
+      const code_typet t(
         {code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(signed_int_type())},
         ptr_arg.type().subtype());
@@ -1513,7 +1513,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t(
+      const code_typet t(
         {code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(ptr_arg.type().subtype()),
          code_typet::parametert(signed_int_type())},
@@ -1548,7 +1548,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t(
+      const code_typet t(
         {code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(ptr_arg.type().subtype()),
          code_typet::parametert(signed_int_type())},
@@ -1591,7 +1591,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t(
+      const code_typet t(
         {code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(signed_int_type())},
@@ -1640,7 +1640,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t(
+      const code_typet t(
         {code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(ptr_arg.type()),
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
@@ -611,22 +611,22 @@ void cpp_typecheck_resolvet::make_constructors(
 
       // 1. no arguments, default initialization
       {
-        code_typet t1({}, it->type());
+        const code_typet t1({}, it->type());
         exprt pod_constructor1("pod_constructor", t1);
         new_identifiers.push_back(pod_constructor1);
       }
 
       // 2. one argument, copy/conversion
       {
-        code_typet t2({code_typet::parametert(it->type())}, it->type());
+        const code_typet t2({code_typet::parametert(it->type())}, it->type());
         exprt pod_constructor2("pod_constructor", t2);
         new_identifiers.push_back(pod_constructor2);
       }
 
       // enums, in addition, can also be constructed from int
       if(symbol_type.id()==ID_c_enum_tag)
       {
-        code_typet t3({code_typet::parametert(signed_int_type())}, it->type());
+        const code_typet t3({code_typet::parametert(signed_int_type())}, it->type());
         exprt pod_constructor3("pod_constructor", t3);
         new_identifiers.push_back(pod_constructor3);
       }
diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
@@ -593,7 +593,7 @@ int linker_script_merget::ls_data2instructions(
   for(const auto &d : data["regions"].array)
   {
     code_function_callt f;
-    code_typet void_t({}, empty_typet());
+    const code_typet void_t({}, empty_typet());
     f.function()=symbol_exprt(CPROVER_PREFIX "allocated_memory", void_t);
     unsigned start=safe_string2unsigned(d["start"].value);
     unsigned size=safe_string2unsigned(d["size"].value);
@@ -619,7 +619,7 @@ int linker_script_merget::ls_data2instructions(
     sym.name=CPROVER_PREFIX "allocated_memory";
     sym.pretty_name=CPROVER_PREFIX "allocated_memory";
     sym.is_lvalue=sym.is_static_lifetime=true;
-    code_typet void_t({}, empty_typet());
+    const code_typet void_t({}, empty_typet());
     sym.type=void_t;
     symbol_table.add(sym);
   }
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
@@ -228,7 +228,7 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
     case ATOMIC_END:
       {
         code_function_callt f;
-        code_typet void_t({}, empty_typet());
+        const code_typet void_t({}, empty_typet());
         f.function()=symbol_exprt(
             target->is_atomic_begin() ?
             "__CPROVER_atomic_begin" :
@@ -1948,12 +1948,10 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
           base_name="nondet_"+std::to_string(count);
         }
 
-        code_typet code_type({}, expr.type());
-
         symbolt symbol;
         symbol.base_name=base_name;
         symbol.name=base_name;
-        symbol.type=code_type;
+        symbol.type = code_typet({}, expr.type());
         id=symbol.name;
 
         symbol_table.insert(std::move(symbol));
diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp
@@ -26,8 +26,7 @@ static void create_initialize(symbol_tablet &symbol_table)
   initialize.base_name = INITIALIZE_FUNCTION;
   initialize.mode="jsil";
 
-  code_typet type({}, empty_typet());
-  initialize.type=type;
+  initialize.type = code_typet({}, empty_typet());
 
   code_blockt init_code;
 
@@ -151,10 +150,8 @@ bool jsil_entry_point(
   // add "main"
   symbolt new_symbol;
 
-  code_typet main_type({}, empty_typet());
-
   new_symbol.name=goto_functionst::entry_point();
-  new_symbol.type.swap(main_type);
+  new_symbol.type = code_typet({}, empty_typet());
   new_symbol.value.swap(init_code);
 
   if(!symbol_table.insert(std::move(new_symbol)).second)
diff --git a/unit/analyses/call_graph.cpp b/unit/analyses/call_graph.cpp
@@ -22,7 +22,7 @@ static symbolt create_void_function_symbol(
   const irep_idt &name,
   const codet &code)
 {
-  code_typet void_function_type({}, empty_typet());
+  const code_typet void_function_type({}, empty_typet());
   symbolt function;
   function.name=name;
   function.type=void_function_type;
diff --git a/unit/analyses/dependence_graph.cpp b/unit/analyses/dependence_graph.cpp
@@ -22,7 +22,7 @@ static symbolt create_void_function_symbol(
   const irep_idt &name,
   const codet &code)
 {
-  code_typet void_function_type({}, empty_typet());
+  const code_typet void_function_type({}, empty_typet());
   symbolt function;
   function.name = name;
   function.type = void_function_type;
@@ -74,7 +74,7 @@ SCENARIO("dependence_graph", "[core][analyses][dependence_graph]")
     x_symbol.is_file_local = true;
     goto_model.symbol_table.add(x_symbol);
 
-    code_typet void_function_type({}, empty_typet());
+    const code_typet void_function_type({}, empty_typet());
 
     code_blockt a_body;
     code_declt declare_x(x_symbol.symbol_expr());

Original file line number	Diff line number	Diff line change
`@@ -611,22 +611,22 @@ void cpp_typecheck_resolvet::make_constructors(`
`611`	`611`
`612`	`612`	`// 1. no arguments, default initialization`
`613`	`613`	`{`
`614`		`- code_typet t1({}, it->type());`
	`614`	`+ const code_typet t1({}, it->type());`
`615`	`615`	`exprt pod_constructor1("pod_constructor", t1);`
`616`	`616`	`new_identifiers.push_back(pod_constructor1);`
`617`	`617`	`}`
`618`	`618`
`619`	`619`	`// 2. one argument, copy/conversion`
`620`	`620`	`{`
`621`		`- code_typet t2({code_typet::parametert(it->type())}, it->type());`
	`621`	`+ const code_typet t2({code_typet::parametert(it->type())}, it->type());`
`622`	`622`	`exprt pod_constructor2("pod_constructor", t2);`
`623`	`623`	`new_identifiers.push_back(pod_constructor2);`
`624`	`624`	`}`
`625`	`625`
`626`	`626`	`// enums, in addition, can also be constructed from int`
`627`	`627`	`if(symbol_type.id()==ID_c_enum_tag)`
`628`	`628`	`{`
`629`		`- code_typet t3({code_typet::parametert(signed_int_type())}, it->type());`
	`629`	`+ const code_typet t3({code_typet::parametert(signed_int_type())}, it->type());`
`630`	`630`	`exprt pod_constructor3("pod_constructor", t3);`
`631`	`631`	`new_identifiers.push_back(pod_constructor3);`
`632`	`632`	`}`