Merge pull request #3941 from tautschnig/deprecation-nil_typet-typechecking

Use typet instead of nil_typet during type checking [blocks: #3800, #3907]

Author: tautschnig

jbmc/unit/java_bytecode/load_method_by_regex.cpp

@@ -92,7 +92,7 @@ static symbolt create_method_symbol(const std::string &method_name)
 {
   symbolt new_symbol;
   new_symbol.name = method_name;
-  new_symbol.type = java_method_typet{{}, nil_typet{}};
+  new_symbol.type = java_method_typet{{}, typet{}};
   return new_symbol;
 }
 

src/cpp/cpp_parse_tree.h

@@ -28,4 +28,12 @@ class cpp_parse_treet
   void clear();
 };
 
+class uninitialized_typet : public typet
+{
+public:
+  uninitialized_typet() : typet(static_cast<const typet &>(get_nil_irep()))
+  {
+  }
+};
+
 #endif // CPROVER_CPP_CPP_PARSE_TREE_H

src/cpp/cpp_typecheck.h

@@ -216,7 +216,7 @@ class cpp_typecheckt:public c_typecheck_baset
     const symbolt &symbol,
     const cpp_template_args_tct &specialization_template_args,
     const cpp_template_args_tct &full_template_args,
-    const typet &specialization=typet(ID_nil));
+    const typet &specialization = uninitialized_typet{});
 
   void elaborate_class_template(
     const source_locationt &source_location,

src/cpp/cpp_typecheck_constructor.cpp

@@ -166,7 +166,7 @@ void cpp_typecheckt::default_cpctor(
   cpp_declaratort parameter_tor;
   parameter_tor.add(ID_value).make_nil();
   parameter_tor.set(ID_name, cpp_parameter);
-  parameter_tor.type()=reference_type(nil_typet());
+  parameter_tor.type() = reference_type(uninitialized_typet{});
   parameter_tor.add_source_location()=source_location;
 
   // Parameter declaration
@@ -308,7 +308,7 @@ void cpp_typecheckt::default_assignop(
   declarator_name.get_sub().push_back(irept("="));
 
   declarator_type.id(ID_function_type);
-  declarator_type.subtype()=reference_type(nil_typet());
+  declarator_type.subtype() = reference_type(uninitialized_typet{});
   declarator_type.subtype().add(ID_C_qualifier).make_nil();
 
   exprt &args=static_cast<exprt&>(declarator.type().add(ID_parameters));
@@ -335,7 +335,7 @@ void cpp_typecheckt::default_assignop(
   args_decl_declor.name() = cpp_namet(arg_name, source_location);
   args_decl_declor.add_source_location()=source_location;
 
-  args_decl_declor.type()=pointer_type(typet(ID_nil));
+  args_decl_declor.type() = pointer_type(uninitialized_typet{});
   args_decl_declor.type().set(ID_C_reference, true);
   args_decl_declor.value().make_nil();
 }

src/cpp/parse.cpp

@@ -2206,7 +2206,7 @@ bool Parser::rAttribute(typet &t)
       if(lex.get_token(tk3)!=')')
         return false;
 
-      vector_typet attr(nil_typet(), exp);
+      vector_typet attr(uninitialized_typet{}, exp);
       attr.add_source_location()=exp.source_location();
       merge_types(attr, t);
       break;

src/goto-programs/string_abstraction.cpp

@@ -682,9 +682,8 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
   if(known_entry!=known.end())
     return known_entry->second;
 
-  ::std::pair< abstraction_types_mapt::iterator, bool > map_entry(
-      abstraction_types_map.insert(::std::make_pair(
-          eff_type, nil_typet())));
+  ::std::pair<abstraction_types_mapt::iterator, bool> map_entry(
+    abstraction_types_map.insert(::std::make_pair(eff_type, typet())));
   if(!map_entry.second)
     return map_entry.first->second;
 

src/jsil/jsil_parse_tree.cpp

@@ -70,9 +70,7 @@ void jsil_declarationt::to_symbol(symbolt &symbol) const
 
   irept throws(find(ID_throw));
   side_effect_expr_throwt t(
-    symbol_exprt::typeless(throws.get(ID_value)),
-    nil_typet(),
-    s.source_location());
+    symbol_exprt::typeless(throws.get(ID_value)), typet(), s.source_location());
   code_expressiont ct(t);
 
   if(insert_at_label(r, returns.get(ID_label), code))