Merge pull request #2201 from diffblue/remove-incomplete-type-constructors

kroening · web-flow · commit 72e99a0d162a · 2018-05-30T12:51:56.000+01:00
Remove incomplete type constructors
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1185,7 +1185,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       if(cur_pc==it->handler_pc)
       {
-        if(catch_type!=typet() || it->catch_type==symbol_typet())
+        if(catch_type != typet() || it->catch_type == symbol_typet(irep_idt()))
         {
           catch_type=symbol_typet("java::java.lang.Throwable");
           break;
diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
@@ -105,6 +105,11 @@ class java_bytecode_parse_treet
     struct exceptiont
     {
     public:
+      exceptiont()
+        : start_pc(0), end_pc(0), handler_pc(0), catch_type(irep_idt())
+      {
+      }
+
       std::size_t start_pc;
       std::size_t end_pc;
       std::size_t handler_pc;
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -1249,7 +1249,8 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
-  symbol_typet object_type;
+  optionalt<symbol_typet> object_type;
+
   typet value_type;
   if(type_name==ID_boolean)
   {
@@ -1296,6 +1297,8 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
   else
     UNREACHABLE;
 
+  DATA_INVARIANT(object_type.has_value(), "must have symbol for primitive");
+
   // declare tmp_type_name to hold the value
   std::string aux_name="tmp_"+id2string(type_name);
   symbolt symbol=get_fresh_aux_symbol(
@@ -1304,7 +1307,9 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
 
   // Check that the type of the object is in the symbol table,
   // otherwise there is no safe way of finding its value.
-  if(const auto maybe_symbol=symbol_table.lookup(object_type.get_identifier()))
+  if(
+    const auto maybe_symbol =
+      symbol_table.lookup(object_type->get_identifier()))
   {
     struct_typet struct_type=to_struct_type(maybe_symbol->type);
     // Check that the type has a value field
@@ -1321,7 +1326,7 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
     }
   }
 
-  warning() << object_type.get_identifier()
+  warning() << object_type->get_identifier()
             << " not available to format function" << eom;
   code.add(code_declt(value), loc);
   return value;
diff --git a/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp b/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp
@@ -17,9 +17,12 @@ SCENARIO("generic_type_index", "[core][java_types]")
     const auto symbol_type = symbol_typet("java::GenericClass");
     const auto generic_symbol_type = java_generic_symbol_typet(
       symbol_type, "LGenericClass<TX;Tvalue;>;", "PrefixClassName");
-    java_generic_parametert paramX("PrefixClassName::X", symbol_typet());
-    java_generic_parametert value("PrefixClassName::value", symbol_typet());
-    java_generic_parametert paramZ("PrefixClassName::Z", symbol_typet());
+    java_generic_parametert paramX(
+      "PrefixClassName::X", symbol_typet(irep_idt()));
+    java_generic_parametert value(
+      "PrefixClassName::value", symbol_typet(irep_idt()));
+    java_generic_parametert paramZ(
+      "PrefixClassName::Z", symbol_typet(irep_idt()));
 
     WHEN("Looking for parameter indexes")
     {
@@ -43,9 +46,12 @@ SCENARIO("generic_type_index", "[core][java_types]")
     const auto symbol_type = symbol_typet("java::java.util.Map");
     const auto generic_symbol_type = java_generic_symbol_typet(
       symbol_type, "Ljava/util/Map<TK;TV;>;", "java.util.HashMap");
-    java_generic_parametert param0("java.util.HashMap::K", symbol_typet());
-    java_generic_parametert param1("java.util.HashMap::V", symbol_typet());
-    java_generic_parametert param2("java.util.HashMap::T", symbol_typet());
+    java_generic_parametert param0(
+      "java.util.HashMap::K", symbol_typet(irep_idt()));
+    java_generic_parametert param1(
+      "java.util.HashMap::V", symbol_typet(irep_idt()));
+    java_generic_parametert param2(
+      "java.util.HashMap::T", symbol_typet(irep_idt()));
 
     WHEN("Looking for parameter indexes")
     {
diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
@@ -601,10 +601,8 @@ void ansi_c_convert_typet::write(typet &type)
 
   if(vector_size.is_not_nil())
   {
-    vector_typet new_type;
-    new_type.size()=vector_size;
+    vector_typet new_type(type, vector_size);
     new_type.add_source_location()=vector_size.source_location();
-    new_type.subtype().swap(type);
     type=new_type;
   }
 
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
@@ -792,9 +792,8 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
     }
   }
 
-  symbol_typet symbol_type;
+  symbol_typet symbol_type(identifier);
   symbol_type.add_source_location()=type.source_location();
-  symbol_type.set_identifier(identifier);
 
   c_qualifierst original_qualifiers(type);
   type.swap(symbol_type);
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
@@ -5987,9 +5987,7 @@ bool Parser::rNewDeclarator(typet &decl)
     if(lex.get_token(cb)!=']')
       return false;
 
-    array_typet array_type;
-    array_type.size().swap(expr);
-    array_type.subtype().swap(decl);
+    array_typet array_type(decl, expr);
     set_location(array_type, ob);
 
     decl.swap(array_type);
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
@@ -177,7 +177,7 @@ void remove_virtual_functionst::remove_virtual_function(
   // So long as `this` is already not `void*` typed, the second parameter
   // is ignored:
   exprt this_class_identifier =
-    get_class_identifier_field(this_expr, symbol_typet(), ns);
+    get_class_identifier_field(this_expr, symbol_typet(irep_idt()), ns);
 
   // If instructed, add an ASSUME(FALSE) to handle the case where we don't
   // match any expected type:
diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp
@@ -791,9 +791,7 @@ void string_instrumentationt::do_strerror(
     new_symbol_size.is_lvalue=true;
     new_symbol_size.is_static_lifetime=true;
 
-    array_typet type;
-    type.subtype()=char_type();
-    type.size()=new_symbol_size.symbol_expr();
+    array_typet type(char_type(), new_symbol_size.symbol_expr());
     symbolt new_symbol_buf;
     new_symbol_buf.mode=ID_C;
     new_symbol_buf.type=type;
diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
@@ -1028,26 +1028,27 @@ typet smt2_parsert::function_signature_definition()
     return sort();
   }
 
-  mathematical_function_typet result;
+  mathematical_function_typet::domaint domain;
 
   while(peek()!=CLOSE)
   {
     if(next_token()!=OPEN)
     {
       error() << "expected '(' at beginning of parameter" << eom;
-      return result;
+      return nil_typet();
     }
 
     if(next_token()!=SYMBOL)
     {
       error() << "expected symbol in parameter" << eom;
-      return result;
+      return nil_typet();
     }
 
-    auto &var=result.add_variable();
+    mathematical_function_typet::variablet var;
     std::string id=buffer;
     var.set_identifier(id);
     var.type()=sort();
+    domain.push_back(var);
 
     auto &entry=id_map[id];
     entry.type=var.type();
@@ -1056,15 +1057,15 @@ typet smt2_parsert::function_signature_definition()
     if(next_token()!=CLOSE)
     {
       error() << "expected ')' at end of parameter" << eom;
-      return result;
+      return nil_typet();
     }
   }
 
   next_token(); // eat the ')'
 
-  result.codomain()=sort();
+  typet codomain = sort();
 
-  return result;
+  return mathematical_function_typet(domain, codomain);
 }
 
 typet smt2_parsert::function_signature_declaration()
@@ -1081,37 +1082,38 @@ typet smt2_parsert::function_signature_declaration()
     return sort();
   }
 
-  mathematical_function_typet result;
+  mathematical_function_typet::domaint domain;
 
   while(peek()!=CLOSE)
   {
     if(next_token()!=OPEN)
     {
       error() << "expected '(' at beginning of parameter" << eom;
-      return result;
+      return nil_typet();
     }
 
     if(next_token()!=SYMBOL)
     {
       error() << "expected symbol in parameter" << eom;
-      return result;
+      return nil_typet();
     }
 
-    auto &var=result.add_variable();
+    mathematical_function_typet::variablet var;
     var.type()=sort();
+    domain.push_back(var);
 
     if(next_token()!=CLOSE)
     {
       error() << "expected ')' at end of parameter" << eom;
-      return result;
+      return nil_typet();
     }
   }
 
   next_token(); // eat the ')'
 
-  result.codomain()=sort();
+  typet codomain = sort();
 
-  return result;
+  return mathematical_function_typet(domain, codomain);
 }
 
 void smt2_parsert::command(const std::string &c)
diff --git a/src/util/std_types.h b/src/util/std_types.h
@@ -110,10 +110,6 @@ class real_typet:public typet
 class symbol_typet:public typet
 {
 public:
-  symbol_typet():typet(ID_symbol)
-  {
-  }
-
   explicit symbol_typet(const irep_idt &identifier):typet(ID_symbol)
   {
     set_identifier(identifier);
@@ -492,10 +488,6 @@ inline union_typet &to_union_type(typet &type)
 class tag_typet:public typet
 {
 public:
-  explicit tag_typet(const irep_idt &_id):typet(_id)
-  {
-  }
-
   explicit tag_typet(
     const irep_idt &_id,
     const irep_idt &identifier):typet(_id)
@@ -980,10 +972,6 @@ inline code_typet &to_code_type(typet &type)
 class array_typet:public type_with_subtypet
 {
 public:
-  array_typet():type_with_subtypet(ID_array)
-  {
-  }
-
   array_typet(
     const typet &_subtype,
     const exprt &_size):type_with_subtypet(ID_array, _subtype)
@@ -1575,10 +1563,6 @@ inline const string_typet &to_string_type(const typet &type)
 class range_typet:public typet
 {
 public:
-  range_typet():typet(ID_range)
-  {
-  }
-
   range_typet(const mp_integer &_from, const mp_integer &_to)
   {
     set_from(_from);
@@ -1613,10 +1597,6 @@ inline const range_typet &to_range_type(const typet &type)
 class vector_typet:public type_with_subtypet
 {
 public:
-  vector_typet():type_with_subtypet(ID_vector)
-  {
-  }
-
   vector_typet(
     const typet &_subtype,
     const exprt &_size):type_with_subtypet(ID_vector, _subtype)
@@ -1706,11 +1686,6 @@ inline complex_typet &to_complex_type(typet &type)
 class mathematical_function_typet:public typet
 {
 public:
-  mathematical_function_typet():typet(ID_mathematical_function)
-  {
-    subtypes().resize(2);
-  }
-
   // the domain of the function is composed of zero, one, or
   // many variables
   class variablet:public irept
@@ -1740,6 +1715,14 @@ class mathematical_function_typet:public typet
 
   using domaint=std::vector<variablet>;
 
+  mathematical_function_typet(const domaint &_domain, const typet &_codomain)
+    : typet(ID_mathematical_function)
+  {
+    subtypes().resize(2);
+    domain() = _domain;
+    codomain() = _codomain;
+  }
+
   domaint &domain()
   {
     return (domaint &)subtypes()[0].subtypes();

Original file line number	Diff line number	Diff line change
`@@ -1185,7 +1185,7 @@ codet java_bytecode_convert_methodt::convert_instructions(`
`1185`	`1185`	`{`
`1186`	`1186`	`if(cur_pc==it->handler_pc)`
`1187`	`1187`	`{`
`1188`		`- if(catch_type!=typet() \|\| it->catch_type==symbol_typet())`
	`1188`	`+ if(catch_type != typet() \|\| it->catch_type == symbol_typet(irep_idt()))`
`1189`	`1189`	`{`
`1190`	`1190`	`catch_type=symbol_typet("java::java.lang.Throwable");`
`1191`	`1191`	`break;`
Original file line number	Diff line number	Diff line change
`@@ -601,10 +601,8 @@ void ansi_c_convert_typet::write(typet &type)`
`601`	`601`
`602`	`602`	`if(vector_size.is_not_nil())`
`603`	`603`	`{`
`604`		`- vector_typet new_type;`
`605`		`- new_type.size()=vector_size;`
	`604`	`+ vector_typet new_type(type, vector_size);`
`606`	`605`	`new_type.add_source_location()=vector_size.source_location();`
`607`		`- new_type.subtype().swap(type);`
`608`	`606`	`type=new_type;`
`609`	`607`	`}`
`610`	`608`
Original file line number	Diff line number	Diff line change
`@@ -792,9 +792,8 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)`
`792`	`792`	`}`
`793`	`793`	`}`
`794`	`794`
`795`		`- symbol_typet symbol_type;`
	`795`	`+ symbol_typet symbol_type(identifier);`
`796`	`796`	`symbol_type.add_source_location()=type.source_location();`
`797`		`- symbol_type.set_identifier(identifier);`
`798`	`797`
`799`	`798`	`c_qualifierst original_qualifiers(type);`
`800`	`799`	`type.swap(symbol_type);`
Original file line number	Diff line number	Diff line change
`@@ -1028,26 +1028,27 @@ typet smt2_parsert::function_signature_definition()`
`1028`	`1028`	`return sort();`
`1029`	`1029`	`}`
`1030`	`1030`
`1031`		`- mathematical_function_typet result;`
	`1031`	`+ mathematical_function_typet::domaint domain;`
`1032`	`1032`
`1033`	`1033`	`while(peek()!=CLOSE)`
`1034`	`1034`	`{`
`1035`	`1035`	`if(next_token()!=OPEN)`
`1036`	`1036`	`{`
`1037`	`1037`	`error() << "expected '(' at beginning of parameter" << eom;`
`1038`		`- return result;`
	`1038`	`+ return nil_typet();`
`1039`	`1039`	`}`
`1040`	`1040`
`1041`	`1041`	`if(next_token()!=SYMBOL)`
`1042`	`1042`	`{`
`1043`	`1043`	`error() << "expected symbol in parameter" << eom;`
`1044`		`- return result;`
	`1044`	`+ return nil_typet();`
`1045`	`1045`	`}`
`1046`	`1046`
`1047`		`- auto &var=result.add_variable();`
	`1047`	`+ mathematical_function_typet::variablet var;`
`1048`	`1048`	`std::string id=buffer;`
`1049`	`1049`	`var.set_identifier(id);`
`1050`	`1050`	`var.type()=sort();`
	`1051`	`+ domain.push_back(var);`
`1051`	`1052`
`1052`	`1053`	`auto &entry=id_map[id];`
`1053`	`1054`	`entry.type=var.type();`
`@@ -1056,15 +1057,15 @@ typet smt2_parsert::function_signature_definition()`
`1056`	`1057`	`if(next_token()!=CLOSE)`
`1057`	`1058`	`{`
`1058`	`1059`	`error() << "expected ')' at end of parameter" << eom;`
`1059`		`- return result;`
	`1060`	`+ return nil_typet();`
`1060`	`1061`	`}`
`1061`	`1062`	`}`
`1062`	`1063`
`1063`	`1064`	`next_token(); // eat the ')'`
`1064`	`1065`
`1065`		`- result.codomain()=sort();`
	`1066`	`+ typet codomain = sort();`
`1066`	`1067`
`1067`		`- return result;`
	`1068`	`+ return mathematical_function_typet(domain, codomain);`
`1068`	`1069`	`}`
`1069`	`1070`
`1070`	`1071`	`typet smt2_parsert::function_signature_declaration()`
`@@ -1081,37 +1082,38 @@ typet smt2_parsert::function_signature_declaration()`
`1081`	`1082`	`return sort();`
`1082`	`1083`	`}`
`1083`	`1084`
`1084`		`- mathematical_function_typet result;`
	`1085`	`+ mathematical_function_typet::domaint domain;`
`1085`	`1086`
`1086`	`1087`	`while(peek()!=CLOSE)`
`1087`	`1088`	`{`
`1088`	`1089`	`if(next_token()!=OPEN)`
`1089`	`1090`	`{`
`1090`	`1091`	`error() << "expected '(' at beginning of parameter" << eom;`
`1091`		`- return result;`
	`1092`	`+ return nil_typet();`
`1092`	`1093`	`}`
`1093`	`1094`
`1094`	`1095`	`if(next_token()!=SYMBOL)`
`1095`	`1096`	`{`
`1096`	`1097`	`error() << "expected symbol in parameter" << eom;`
`1097`		`- return result;`
	`1098`	`+ return nil_typet();`
`1098`	`1099`	`}`
`1099`	`1100`
`1100`		`- auto &var=result.add_variable();`
	`1101`	`+ mathematical_function_typet::variablet var;`
`1101`	`1102`	`var.type()=sort();`
	`1103`	`+ domain.push_back(var);`
`1102`	`1104`
`1103`	`1105`	`if(next_token()!=CLOSE)`
`1104`	`1106`	`{`
`1105`	`1107`	`error() << "expected ')' at end of parameter" << eom;`
`1106`		`- return result;`
	`1108`	`+ return nil_typet();`
`1107`	`1109`	`}`
`1108`	`1110`	`}`
`1109`	`1111`
`1110`	`1112`	`next_token(); // eat the ')'`
`1111`	`1113`
`1112`		`- result.codomain()=sort();`
	`1114`	`+ typet codomain = sort();`
`1113`	`1115`
`1114`		`- return result;`
	`1116`	`+ return mathematical_function_typet(domain, codomain);`
`1115`	`1117`	`}`
`1116`	`1118`
`1117`	`1119`	`void smt2_parsert::command(const std::string &c)`