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

regression/cbmc-cpp/Constructor7/main.cpp

@@ -0,0 +1,17 @@
+#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,26 @@
+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/ansi-c/parser.y

@@ -279,6 +279,10 @@ int yyansi_cerror(const std::string &error);
 %token TOK_MSC_IF_EXISTS "__if_exists"
 %token TOK_MSC_IF_NOT_EXISTS "__if_not_exists"
 %token TOK_UNDERLYING_TYPE "__underlying_type"
+%token TOK_DYNAMIC_CAST "dynamic_cast"
+%token TOK_STATIC_CAST "static_cast"
+%token TOK_REINTERPRET_CAST "reinterpret_cast"
+%token TOK_CONST_CAST "const_cast"
 
 /*** priority, associativity, etc. definitions **************************/
 

src/ansi-c/scanner.l

@@ -1316,6 +1316,11 @@
                          return make_identifier();
                      }
 
+"dynamic_cast"  { return cpp98_keyword(TOK_DYNAMIC_CAST); }
+"static_cast"   { return cpp98_keyword(TOK_STATIC_CAST); }
+"reinterpret_cast"   { return cpp98_keyword(TOK_REINTERPRET_CAST); }
+"const_cast"    { return cpp98_keyword(TOK_CONST_CAST); }
+
 {CPROVER_PREFIX}"atomic"       { loc(); return TOK_CPROVER_ATOMIC; }
 {CPROVER_PREFIX}"forall"       { loc(); return TOK_FORALL; }
 {CPROVER_PREFIX}"exists"       { loc(); return TOK_EXISTS; }

src/cpp/cpp_is_pod.cpp

@@ -73,6 +73,10 @@ bool cpp_typecheckt::cpp_is_pod(const typet &type) const
   {
     return cpp_is_pod(to_array_type(type).element_type());
   }
+  else if(type.id() == ID_vector)
+  {
+    return cpp_is_pod(to_vector_type(type).element_type());
+  }
   else if(type.id()==ID_pointer)
   {
     if(is_reference(type)) // references are not PODs

src/cpp/cpp_typecheck_expr.cpp

@@ -126,6 +126,12 @@
   {
     expr.type().id(ID_initializer_list);
   }
+  else if(
+    expr.id() == ID_const_cast || expr.id() == ID_dynamic_cast ||
+    expr.id() == ID_reinterpret_cast || expr.id() == ID_static_cast)
+  {
+    typecheck_cast_expr(expr);
+  }
   else
     c_typecheck_baset::typecheck_expr_main(expr);
 }
@@ -966,13 +972,8 @@
   }
   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);
   }
 }
 
@@ -1274,53 +1275,20 @@
 
 void cpp_typecheckt::typecheck_cast_expr(exprt &expr)
 {
-  side_effect_expr_function_callt e =
-    to_side_effect_expr_function_call(expr);
-
-  if(e.arguments().size() != 1)
+  if(expr.operands().size() != 1)
   {
     error().source_location=expr.find_source_location();
     error() << "cast expressions expect one operand" << eom;
     throw 0;
   }
 
-  exprt &f_op=e.function();
-  exprt &cast_op=e.arguments().front();
+  exprt &cast_op = to_unary_expr(expr).op();
 
   add_implicit_dereference(cast_op);
 
-  const irep_idt &id=
-  f_op.get_sub().front().get(ID_identifier);
-
-  if(f_op.get_sub().size()!=2 ||
-     f_op.get_sub()[1].id()!=ID_template_args)
-  {
-    error().source_location=expr.find_source_location();
-    error() << id << " expects template argument" << eom;
-    throw 0;
-  }
-
-  irept &template_arguments=f_op.get_sub()[1].add(ID_arguments);
-
-  if(template_arguments.get_sub().size()!=1)
-  {
-    error().source_location=expr.find_source_location();
-    error() << id << " expects one template argument" << eom;
-    throw 0;
-  }
-
-  irept &template_arg=template_arguments.get_sub().front();
-
-  if(template_arg.id() != ID_type && template_arg.id() != ID_ambiguous)
-  {
-    error().source_location=expr.find_source_location();
-    error() << id << " expects a type as template argument" << eom;
-    throw 0;
-  }
-
-  typet &type=static_cast<typet &>(
-    template_arguments.get_sub().front().add(ID_type));
+  const irep_idt &id = expr.id();
 
+  typet &type = expr.type();
   typecheck_type(type);
 
   source_locationt source_location=expr.source_location();
@@ -1414,21 +1382,6 @@
     }
   }
 
-  if(expr.get_sub().size()>=1 &&
-     expr.get_sub().front().id()==ID_name)
-  {
-    const irep_idt &id=expr.get_sub().front().get(ID_identifier);
-
-    if(id==ID_const_cast ||
-       id==ID_dynamic_cast ||
-       id==ID_reinterpret_cast ||
-       id==ID_static_cast)
-    {
-      expr.id(ID_cast_expression);
-      return;
-    }
-  }
-
   exprt symbol_expr=
     resolve(
       to_cpp_name(expr),
@@ -1555,14 +1508,6 @@
 
     return;
   }
-  else if(expr.function().id() == ID_cast_expression)
-  {
-    // These are not really function calls,
-    // but usually just type adjustments.
-    typecheck_cast_expr(expr);
-    add_implicit_dereference(expr);
-    return;
-  }
   else if(expr.function().id() == ID_cpp_dummy_destructor)
   {
     // these don't do anything, e.g., (char*)->~char()