Merge pull request #2343 from tautschnig/c++-auto

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/auto2/main.cpp

@@ -0,0 +1,7 @@
+int main()
+{
+#ifndef _MSC_VER
+  // Visual Studio uses C++14 by default, thus the below would not be valid
+  auto int x = 42;
+#endif
+}

regression/cpp/auto2/test.desc

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

regression/cpp/auto3/main.cpp

@@ -0,0 +1,11 @@
+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/auto3/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.cpp
+
+^EXIT=(64|1)$
+^SIGNAL=0$
+parse error
+--
+^warning: ignoring
+^CONVERSION ERROR$

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, kroening@cs.cmu.edu
 
 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);