C++ front-end fixes

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$

regression/cpp/constexpr1/main.cpp

@@ -14,6 +14,18 @@ constexpr int some_other_value =
 
 static_assert(some_other_value == 2, "some_other_value == 2");
 
+constexpr int some_function2(int a)
+{
+  int b;
+  a = a + 1;
+  b = a;
+  return b + 1;
+}
+
+constexpr int some_other_value2 = some_function2(1);
+
+static_assert(some_other_value2 == 3, "some_other_value == 2");
+
 int main()
 {
 }

regression/cpp/constexpr1/test.desc

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

regression/cpp/type_traits_essentials1/test.desc

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

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 @@ __decltype          { if(PARSER.cpp98 &&
                          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; }
@@ -1431,7 +1436,7 @@ __decltype          { if(PARSER.cpp98 &&
 
   /* This is a C11 keyword */
 
-"_Alignof"      { if(!PARSER.cpp98 &&
+"_Alignof"      { if((!PARSER.cpp98 || PARSER.cpp11) &&
                      (PARSER.mode==configt::ansi_ct::flavourt::GCC ||
                       PARSER.mode==configt::ansi_ct::flavourt::CLANG ||
                       PARSER.mode==configt::ansi_ct::flavourt::ARM ||
@@ -1453,7 +1458,7 @@ __decltype          { if(PARSER.cpp98 &&
 "_Atomic"{ws}"(" { // put back all but _Atomic
                    yyless(7);
 
-                   if(!PARSER.cpp98 &&
+                   if((!PARSER.cpp98 || PARSER.cpp11) &&
                       (PARSER.mode==configt::ansi_ct::flavourt::GCC ||
                        PARSER.mode==configt::ansi_ct::flavourt::CLANG ||
                        PARSER.mode==configt::ansi_ct::flavourt::ARM))

src/cbmc/cbmc_parse_options.cpp

@@ -542,11 +542,14 @@ int cbmc_parse_optionst::doit()
   register_languages();
 
   // configure gcc, if required
-  if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
+  if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC ||
+    config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::CLANG)
   {
     gcc_versiont gcc_version;
     gcc_version.get("gcc");
     configure_gcc(gcc_version);
+    config.ansi_c.c_standard = gcc_version.default_c_standard;
+    config.cpp.cpp_standard = gcc_version.default_cxx_standard;
   }
 
   if(cmdline.isset("test-preprocessor"))

src/cpp/cpp_convert_type.cpp

@@ -63,8 +63,6 @@ void cpp_convert_typet::read_rec(const typet &type)
     ++char16_t_count;
   else if(type.id()==ID_char32_t)
     ++char32_t_count;
-  else if(type.id()==ID_constexpr)
-    c_qualifiers.is_constant = true;
   else if(type.id()==ID_function_type)
   {
     read_function_type(type);

src/cpp/cpp_declaration.h

@@ -54,8 +54,11 @@ class cpp_declarationt:public exprt
 
   bool is_class_template() const
   {
+    const typet * t = &type();
+    while(t->id() == ID_merged_type)
+      t = &to_type_with_subtypes(*t).subtypes().back();
     return is_template() &&
-           type().id()==ID_struct &&
+           t->id()==ID_struct &&
            declarators().empty();
   }
 

src/cpp/cpp_declarator.h

@@ -55,6 +55,16 @@ class cpp_declaratort:public exprt
     set(ID_is_parameter, is_parameter);
   }
 
+  bool get_has_ellipsis() const
+  {
+    return get_bool(ID_ellipsis);
+  }
+
+  void set_has_ellipsis()
+  {
+    set(ID_ellipsis, true);
+  }
+
   // initializers for function arguments
   exprt &init_args()
   {

src/cpp/cpp_declarator_converter.cpp

@@ -456,7 +456,8 @@ symbolt &cpp_declarator_convertert::convert_new_symbol(
   symbol.is_weak = storage_spec.is_weak();
   symbol.module=cpp_typecheck.module;
   symbol.is_type=is_typedef;
-  symbol.is_macro=is_typedef && !is_template_parameter;
+  symbol.is_macro =
+    (is_typedef && !is_template_parameter) || storage_spec.is_constexpr();
   symbol.pretty_name=pretty_name;
 
   if(is_code && !symbol.is_type)
@@ -493,7 +494,7 @@ symbolt &cpp_declarator_convertert::convert_new_symbol(
       storage_spec.is_thread_local();
 
     symbol.is_file_local =
-      symbol.is_macro ||
+      (symbol.is_macro && !storage_spec.is_constexpr()) ||
       (!cpp_typecheck.cpp_scopes.current_scope().is_global_scope() &&
        !storage_spec.is_extern()) ||
       (cpp_typecheck.cpp_scopes.current_scope().is_global_scope() &&
@@ -553,10 +554,14 @@ symbolt &cpp_declarator_convertert::convert_new_symbol(
   // do the value
   if(!new_symbol->is_type)
   {
-    if(is_code && declarator.type().id()!=ID_template)
-      cpp_typecheck.add_method_body(new_symbol);
-
-    if(!is_code)
+    if(is_code)
+    {
+      if(new_symbol->is_macro)
+        cpp_typecheck.convert_function(*new_symbol);
+      else if(declarator.type().id() != ID_template)
+        cpp_typecheck.add_method_body(new_symbol);
+    }
+    else
       cpp_typecheck.convert_initializer(*new_symbol);
   }
 

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_storage_spec.cpp

@@ -33,4 +33,6 @@ void cpp_storage_spect::read(const typet &type)
     set_asm();
   else if(type.id() == ID_weak)
     set_weak();
+  else if(type.id() == ID_constexpr)
+    set_constexpr();
 }

src/cpp/cpp_storage_spec.h

@@ -47,6 +47,10 @@ class cpp_storage_spect:public irept
   {
     return get_bool(ID_weak);
   }
+  bool is_constexpr() const
+  {
+    return get_bool(ID_constexpr);
+  }
 
   void set_static()       { set(ID_static, true); }
   void set_extern()       { set(ID_extern, true); }
@@ -59,11 +63,16 @@ class cpp_storage_spect:public irept
   {
     set(ID_weak, true);
   }
+  void set_constexpr()
+  {
+    set(ID_constexpr, true);
+  }
 
   bool is_empty() const
   {
     return !is_static() && !is_extern() && !is_auto() && !is_register() &&
-           !is_mutable() && !is_thread_local() && !is_asm() && !is_weak();
+           !is_mutable() && !is_thread_local() && !is_asm() && !is_weak() &&
+           !is_constexpr();
   }
 
   cpp_storage_spect &operator|=(const cpp_storage_spect &other)
@@ -84,6 +93,8 @@ class cpp_storage_spect:public irept
       set_asm();
     if(other.is_weak())
       set_weak();
+    if(other.is_constexpr())
+      set_constexpr();
 
     return *this;
   }

src/cpp/cpp_token_buffer.h

@@ -49,6 +49,11 @@ class cpp_token_buffert
   void Restore(post pos);
   void Replace(const cpp_tokent &token);
   void Insert(const cpp_tokent &token);
+  const cpp_tokent &peek()
+  {
+    PRECONDITION(current_pos <= token_vector.size());
+    return *token_vector[current_pos];
+  }
 
   void clear()
   {