C++11 auto type specifier

Author: tautschnig

regression/cpp/auto1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 -std=c++11
 ^EXIT=0$

regression/cpp/auto3/main.cpp

@@ -3,6 +3,8 @@ int main()
 #ifndef _MSC_VER
   // should yield a parse error unless in C++11 (or later) mode
   auto x = 42;
+  const auto y = 42;
+  const auto &z = y;
 #else
   intentionally invalid
 #endif

regression/cpp/auto4/main.cpp

@@ -0,0 +1,6 @@
+int main()
+{
+  auto x = 42;
+  const auto y = 42;
+  const auto &z = y;
+}

regression/cpp/auto4/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.cpp
+-std=c++11
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/cpp/cpp_convert_type.cpp

@@ -591,3 +591,19 @@ void cpp_convert_plain_type(typet &type)
     cpp_convert_type.write(type);
   }
 }
+
+void cpp_convert_auto(typet &dest, const typet &src)
+{
+  if(dest.id() != ID_merged_type && dest.has_subtype())
+  {
+    cpp_convert_auto(dest.subtype(), src);
+    return;
+  }
+
+  cpp_convert_typet cpp_convert_type(dest);
+  for(auto &t : cpp_convert_type.other)
+    if(t.id() == ID_auto)
+      t = src;
+
+  cpp_convert_type.write(dest);
+}

src/cpp/cpp_convert_type.h

@@ -16,4 +16,6 @@ Author: Daniel Kroening, [email protected]
 
 void cpp_convert_plain_type(typet &);
 
+void cpp_convert_auto(typet &dest, const typet &src);
+
 #endif // CPROVER_CPP_CPP_CONVERT_TYPE_H

src/cpp/cpp_declarator_converter.cpp

@@ -68,7 +68,8 @@ symbolt &cpp_declarator_convertert::convert(
     scope=&cpp_typecheck.cpp_scopes.current_scope();
 
     // check the declarator-part of the type, in that scope
-    cpp_typecheck.typecheck_type(final_type);
+    if(declarator.value().is_nil() || !cpp_typecheck.has_auto(final_type))
+      cpp_typecheck.typecheck_type(final_type);
   }
 
   is_code=is_code_type(final_type);

src/cpp/cpp_typecheck.h

@@ -395,6 +395,7 @@ class cpp_typecheckt:public c_typecheck_baset
 
   static bool has_const(const typet &type);
   static bool has_volatile(const typet &type);
+  static bool has_auto(const typet &type);
 
   void typecheck_member_function(
     const irep_idt &compound_identifier,

src/cpp/cpp_typecheck_code.cpp

@@ -366,7 +366,9 @@ void cpp_typecheckt::typecheck_decl(codet &code)
 
   bool is_typedef=declaration.is_typedef();
 
-  typecheck_type(type);
+  if(declaration.declarators().empty() || !has_auto(type))
+    typecheck_type(type);
+
   assert(type.is_not_nil());
 
   if(declaration.declarators().empty() &&
@@ -407,7 +409,10 @@ void cpp_typecheckt::typecheck_decl(codet &code)
        symbol.value.id()!=ID_code)
     {
       decl_statement.copy_to_operands(symbol.value);
-      assert(follow(decl_statement.op1().type())==follow(symbol.type));
+      DATA_INVARIANT(
+        has_auto(symbol.type) ||
+          follow(decl_statement.op1().type()) == follow(symbol.type),
+        "declarator type should match symbol type");
     }
 
     new_code.move_to_operands(decl_statement);

src/cpp/cpp_typecheck_compound_type.cpp

@@ -57,6 +57,22 @@ bool cpp_typecheckt::has_volatile(const typet &type)
     return false;
 }
 
+bool cpp_typecheckt::has_auto(const typet &type)
+{
+  if(type.id() == ID_auto)
+    return true;
+  else if(type.id() == ID_merged_type || type.id() == ID_frontend_pointer)
+  {
+    forall_subtypes(it, type)
+      if(has_auto(*it))
+        return true;
+
+    return false;
+  }
+  else
+    return false;
+}
+
 cpp_scopet &cpp_typecheckt::tag_scope(
   const irep_idt &base_name,
   bool has_body,