C++ front-end: support explicit type conversion with braced-init-list

Now follows the grammar described in the C++ standard: Explicit type
conversions are postfix expressions.

Author: tautschnig

regression/cbmc-cpp/Constructor7/main.cpp

@@ -0,0 +1,16 @@
+#include <cassert>
+
+int main(int argc, char * argv[])
+{
+  struct S {
+    S() : x(42)
+                 {
+                 }
+
+    int x;
+  };
+  S s = S{};
+
+  __CPROVER_assert(s.x == 42, "");
+  assert(s.x == 42);
+}

regression/cbmc-cpp/Constructor7/test.desc

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

regression/cpp/brace_initializer1/main.cpp

@@ -0,0 +1,24 @@
+struct __invoke_memfun_ref {};
+    constexpr bool __call_is_nt(__invoke_memfun_ref)
+    {
+      return false;
+    }
+
+  template<typename _Result>
+    struct __call_is_nothrow
+    {
+      constexpr static bool is_nt =
+__call_is_nt(typename _Result::__invoke_type{});
+    };
+
+int main(int argc, char * argv[])
+{
+  struct S {
+    S() : x(42)
+                 {
+                 }
+
+    int x;
+  };
+  S s = S{};
+}

regression/cpp/brace_initializer1/test.desc

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

src/cpp/cpp_typecheck_expr.cpp

@@ -966,13 +966,8 @@ void cpp_typecheckt::typecheck_expr_explicit_constructor_call(exprt &expr)
   }
   else
   {
-    CHECK_RETURN(expr.type().id() == ID_struct);
-
-    struct_tag_typet tag(expr.type().get(ID_name));
-    tag.add_source_location() = expr.source_location();
-
     exprt e=expr;
-    new_temporary(e.source_location(), tag, e.operands(), expr);
+    new_temporary(e.source_location(), e.type(), e.operands(), expr);
   }
 }
 

src/cpp/parse.cpp

@@ -6363,7 +6363,10 @@ bool Parser::rAllocateInitializer(exprt &init)
   postfix.exp
   : primary.exp
   | postfix.expr '[' comma.expression ']'
+  | postfix.expr '[' initializer ']'
   | postfix.expr '(' function.arguments ')'
+  | integral.or.class.spec '(' function.arguments ')'
+  | integral.or.class.spec initializer
   | postfix.expr '.' var.name
   | postfix.expr ArrowOp var.name
   | postfix.expr IncOp
@@ -6372,8 +6375,6 @@ bool Parser::rAllocateInitializer(exprt &init)
   openc++.postfix.expr
   : postfix.expr '.' userdef.statement
   | postfix.expr ArrowOp userdef.statement
-
-  Note: function-style casts are accepted as function calls.
 */
 bool Parser::rPostfixExpr(exprt &exp)
 {
@@ -6382,8 +6383,89 @@ bool Parser::rPostfixExpr(exprt &exp)
   std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0\n";
 #endif
 
-  if(!rPrimaryExpr(exp))
-    return false;
+  typet type;
+
+  cpp_token_buffert::post pos=lex.Save();
+  // try to see whether this is explicit type conversion, else it has to be
+  // a primary-expression
+  if(optIntegralTypeOrClassSpec(type) &&
+     type.is_not_nil() &&
+     (lex.LookAhead(0) == '(' || lex.LookAhead(0) == '{'))
+  {
+#ifdef DEBUG
+    std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0.1\n";
+#endif
+
+    cpp_tokent tk;
+    lex.LookAhead(0, tk);
+    exprt exp2;
+    if(lex.LookAhead(0)=='{')
+    {
+      if(!rInitializeExpr(exp2))
+        return false;
+    }
+    else
+    {
+      // lex.LookAhead(0)=='('
+      lex.get_token(tk);
+
+      if(!rFunctionArguments(exp2))
+        return false;
+
+      cpp_tokent tk2;
+      if(lex.get_token(tk2)!=')')
+        return false;
+    }
+
+    exp=exprt("explicit-constructor-call");
+    exp.type().swap(type);
+    exp.operands().swap(exp2.operands());
+    set_location(exp, tk);
+  }
+  else
+    lex.Restore(pos);
+
+  exprt type_or_function_name;
+  if(rName(type_or_function_name) &&
+     (lex.LookAhead(0) == '(' || lex.LookAhead(0) == '{'))
+  {
+#ifdef DEBUG
+    std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0.2\n";
+#endif
+
+    cpp_tokent tk;
+    lex.LookAhead(0, tk);
+    exprt exp2;
+    if(lex.LookAhead(0)=='{')
+    {
+      if(!rInitializeExpr(exp2))
+        return false;
+    }
+    else
+    {
+      // lex.LookAhead(0)=='('
+      lex.get_token(tk);
+
+      if(!rFunctionArguments(exp2))
+        return false;
+
+      cpp_tokent tk2;
+      if(lex.get_token(tk2)!=')')
+        return false;
+    }
+
+    side_effect_expr_function_callt fc(
+      std::move(type_or_function_name), exp2.operands(), typet{}, source_locationt{});
+    set_location(fc, tk);
+
+    exp.swap(fc);
+  }
+  else
+  {
+    lex.Restore(pos);
+    if(!rPrimaryExpr(exp))
+      return false;
+  }
 
 #ifdef DEBUG
   std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 1\n";
@@ -6399,7 +6481,14 @@ bool Parser::rPostfixExpr(exprt &exp)
     {
     case '[':
       lex.get_token(op);
-      if(!rCommaExpression(e))
+
+      if(lex.LookAhead(0) == '{')
+      {
+        // C++11 initialisation expression
+        if(!rInitializeExpr(e))
+          return false;
+      }
+      else if(!rCommaExpression(e))
         return false;
 
 #ifdef DEBUG
@@ -6424,7 +6513,6 @@ bool Parser::rPostfixExpr(exprt &exp)
       std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 3\n";
 #endif
 
-      lex.get_token(op);
       if(!rFunctionArguments(e))
         return false;
 
@@ -6718,8 +6806,6 @@ bool Parser::rTypePredicate(exprt &expr)
   | THIS
   | var.name
   | '(' comma.expression ')'
-  | integral.or.class.spec '(' function.arguments ')'
-  | integral.or.class.spec initializer
   | typeid.expr
   | true
   | false
@@ -6837,12 +6923,6 @@ bool Parser::rPrimaryExpr(exprt &exp)
 #endif
     return true;
 
-  case '{': // C++11 initialisation expression
-#ifdef DEBUG
-    std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 10\n";
-#endif
-    return rInitializeExpr(exp);
-
   case TOK_TYPEID:
     return rTypeidExpr(exp);
 
@@ -6873,60 +6953,6 @@ bool Parser::rPrimaryExpr(exprt &exp)
     std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 14\n";
 #endif
     {
-      typet type;
-
-      if(!optIntegralTypeOrClassSpec(type))
-        return false;
-
-#ifdef DEBUG
-      std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 15\n";
-#endif
-
-      if(type.is_not_nil() && lex.LookAhead(0)==TOK_SCOPE)
-      {
-        lex.get_token(tk);
-        lex.get_token(tk);
-
-        // TODO
-      }
-      else if(type.is_not_nil())
-      {
-#ifdef DEBUG
-        std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 16\n";
-#endif
-        if(lex.LookAhead(0)=='{')
-        {
-          lex.LookAhead(0, tk);
-
-          exprt exp2;
-          if(!rInitializeExpr(exp2))
-            return false;
-
-          exp=exprt("explicit-constructor-call");
-          exp.type().swap(type);
-          exp.add_to_operands(std::move(exp2));
-          set_location(exp, tk);
-        }
-        else if(lex.LookAhead(0)=='(')
-        {
-          lex.get_token(tk);
-
-          exprt exp2;
-          if(!rFunctionArguments(exp2))
-            return false;
-
-          if(lex.get_token(tk2)!=')')
-            return false;
-
-          exp=exprt("explicit-constructor-call");
-          exp.type().swap(type);
-          exp.operands().swap(exp2.operands());
-          set_location(exp, tk);
-        }
-        else
-          return false;
-      }
-      else
       {
         if(!rVarName(exp))
           return false;