diff --git a/regression/cbmc-cpp/Constructor7/main.cpp b/regression/cbmc-cpp/Constructor7/main.cpp
new file mode 100644
index 00000000000..e01ab3ffd00
--- /dev/null
+++ b/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);
+}
diff --git a/regression/cbmc-cpp/Constructor7/test.desc b/regression/cbmc-cpp/Constructor7/test.desc
new file mode 100644
index 00000000000..91d9cf8b52e
--- /dev/null
+++ b/regression/cbmc-cpp/Constructor7/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cpp/brace_initializer1/main.cpp b/regression/cpp/brace_initializer1/main.cpp
new file mode 100644
index 00000000000..0910fc42dd8
--- /dev/null
+++ b/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{};
+}
diff --git a/regression/cpp/brace_initializer1/test.desc b/regression/cpp/brace_initializer1/test.desc
new file mode 100644
index 00000000000..3862862ffd3
--- /dev/null
+++ b/regression/cpp/brace_initializer1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.cpp
+-std=c++11
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/cpp/constexpr1/main.cpp b/regression/cpp/constexpr1/main.cpp
index 4c54dd28cec..55724408fa7 100644
--- a/regression/cpp/constexpr1/main.cpp
+++ b/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()
 {
 }
diff --git a/regression/cpp/constexpr1/test.desc b/regression/cpp/constexpr1/test.desc
index 0daa9695017..3862862ffd3 100644
--- a/regression/cpp/constexpr1/test.desc
+++ b/regression/cpp/constexpr1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 -std=c++11
 ^EXIT=0$
diff --git a/regression/cpp/type_traits_essentials1/test.desc b/regression/cpp/type_traits_essentials1/test.desc
index 0daa9695017..3862862ffd3 100644
--- a/regression/cpp/type_traits_essentials1/test.desc
+++ b/regression/cpp/type_traits_essentials1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 -std=c++11
 ^EXIT=0$
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index 59e320f7112..bb8a8057688 100644
--- a/src/ansi-c/parser.y
+++ b/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 **************************/
 
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index ad408dbeb31..10a3bde914c 100644
--- a/src/ansi-c/scanner.l
+++ b/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; }
@@ -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))
diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp
index d55fd811898..f77bd262eab 100644
--- a/src/cpp/cpp_convert_type.cpp
+++ b/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);
diff --git a/src/cpp/cpp_declarator.h b/src/cpp/cpp_declarator.h
index 2f62817383a..a459e73eb3f 100644
--- a/src/cpp/cpp_declarator.h
+++ b/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()
   {
diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp
index cfeeaf929d5..a1ad94f9679 100644
--- a/src/cpp/cpp_declarator_converter.cpp
+++ b/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);
   }
 
diff --git a/src/cpp/cpp_is_pod.cpp b/src/cpp/cpp_is_pod.cpp
index d1acd9b71b8..c11ffb54b6a 100644
--- a/src/cpp/cpp_is_pod.cpp
+++ b/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
diff --git a/src/cpp/cpp_storage_spec.cpp b/src/cpp/cpp_storage_spec.cpp
index 170abe0d6f5..df8c7587c01 100644
--- a/src/cpp/cpp_storage_spec.cpp
+++ b/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();
 }
diff --git a/src/cpp/cpp_storage_spec.h b/src/cpp/cpp_storage_spec.h
index db9d0e52833..d7118a848ef 100644
--- a/src/cpp/cpp_storage_spec.h
+++ b/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;
   }
diff --git a/src/cpp/cpp_token_buffer.h b/src/cpp/cpp_token_buffer.h
index 0721c85878d..6e0ddc5ff4c 100644
--- a/src/cpp/cpp_token_buffer.h
+++ b/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()
   {
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 2685771889c..8cee6b3f829 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/mathematical_types.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
+#include <util/replace_symbol.h>
 #include <util/symbol_table_base.h>
 
 #include <ansi-c/c_qualifiers.h>
@@ -126,6 +127,13 @@ void cpp_typecheckt::typecheck_expr_main(exprt &expr)
   {
     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 +974,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);
   }
 }
 
@@ -1274,53 +1277,20 @@ void cpp_typecheckt::typecheck_expr_ptrmember(
 
 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 +1384,6 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
     }
   }
 
-  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 +1510,6 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
 
     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()
@@ -1825,6 +1772,71 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
 
   add_implicit_dereference(expr);
 
+  if(auto sym_expr = expr_try_dynamic_cast<symbol_exprt>(expr.function()))
+  {
+    const auto &symbol = lookup(sym_expr->get_identifier());
+    if(symbol.is_macro)
+    {
+      // constexpr functions evaluated using a mini interpreter
+      const auto &code_type = to_code_type(symbol.type);
+      // PRECONDITION(code_type.return_type().id() != ID_empty);
+      PRECONDITION(expr.arguments().size() == code_type.parameters().size());
+      replace_symbolt value_map;
+      auto param_it = code_type.parameters().begin();
+      for(const auto &arg : expr.arguments())
+      {
+        value_map.insert(
+          symbol_exprt{param_it->get_identifier(), param_it->type()},
+          typecast_exprt::conditional_cast(arg, param_it->type()));
+        ++param_it;
+      }
+      const auto &block = to_code_block(to_code(symbol.value));
+      for(const auto &stmt : block.statements())
+      {
+        if(
+          auto return_stmt = expr_try_dynamic_cast<code_frontend_returnt>(stmt))
+        {
+          PRECONDITION(return_stmt->has_return_value());
+          exprt tmp = return_stmt->return_value();
+          value_map.replace(tmp);
+          expr.swap(tmp);
+          return;
+        }
+        else if(auto expr_stmt = expr_try_dynamic_cast<code_expressiont>(stmt))
+        {
+          // C++14 and later only
+          if(
+            auto assign = expr_try_dynamic_cast<side_effect_expr_assignt>(
+              expr_stmt->expression()))
+          {
+            PRECONDITION(assign->lhs().id() == ID_symbol);
+            exprt rhs = assign->rhs();
+            value_map.replace(rhs);
+            value_map.set(to_symbol_expr(assign->lhs()), rhs);
+          }
+          else
+            UNIMPLEMENTED_FEATURE(
+              "constexpr with " + expr_stmt->expression().pretty());
+        }
+        else if(stmt.get_statement() == ID_decl_block)
+        {
+          // C++14 and later only
+          for(const auto &expect_decl : stmt.operands())
+          {
+            PRECONDITION(to_code(expect_decl).get_statement() == ID_decl);
+            PRECONDITION(!to_code_frontend_decl(to_code(expect_decl))
+                            .initial_value()
+                            .has_value());
+          }
+        }
+        else
+        {
+          UNIMPLEMENTED_FEATURE("constexpr with " + stmt.pretty());
+        }
+      }
+    }
+  }
+
   // we will deal with some 'special' functions here
   exprt tmp=do_special_functions(expr);
   if(tmp.is_not_nil())
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
index e555353ed55..b855f095fa1 100644
--- a/src/cpp/cpp_typecheck_resolve.cpp
+++ b/src/cpp/cpp_typecheck_resolve.cpp
@@ -359,8 +359,16 @@ exprt cpp_typecheck_resolvet::convert_identifier(
     }
     else if(symbol.is_macro)
     {
-      e=symbol.value;
-      PRECONDITION(e.is_not_nil());
+      if(symbol.type.id() == ID_code)
+      {
+        // constexpr function
+        e = cpp_symbol_expr(symbol);
+      }
+      else
+      {
+        e = symbol.value;
+        PRECONDITION(e.is_not_nil());
+      }
     }
     else
     {
diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp
index 6dfcd4a05e2..4e9b276685a 100644
--- a/src/cpp/cpp_typecheck_template.cpp
+++ b/src/cpp/cpp_typecheck_template.cpp
@@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include "cpp_type2name.h"
 #include "cpp_typecheck.h"
 
+#include <iostream>
+
 void cpp_typecheckt::salvage_default_arguments(
   const template_typet &old_type,
   template_typet &new_type)
@@ -714,6 +716,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
   // put template parameters into this scope
   template_typet::template_parameterst &parameters=
     type.template_parameters();
+  std::cerr << type.pretty() << std::endl;
 
   unsigned anon_count=0;
 
@@ -730,6 +733,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
     cpp_declarator_convertert cpp_declarator_converter(*this);
 
     // there must be _one_ declarator
+    std::cerr << declaration.pretty() << std::endl;
     PRECONDITION(declaration.declarators().size() == 1);
 
     cpp_declaratort &declarator=declaration.declarators().front();
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index 777f4b2f0bd..c60d83537bd 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include "cpp_member_spec.h"
 #include "cpp_enum_type.h"
 
+// #define DEBUG
 #ifdef DEBUG
 #include <iostream>
 
@@ -341,6 +342,7 @@ class Parser // NOLINT(readability/identifiers)
   bool rAllocateType(exprt &, typet &, exprt &);
   bool rNewDeclarator(typet &);
   bool rAllocateInitializer(exprt &);
+  bool rCppCastExpr(exprt &);
   bool rPostfixExpr(exprt &);
   bool rPrimaryExpr(exprt &);
   bool rVarName(exprt &);
@@ -764,11 +766,10 @@ bool Parser::isTypeSpecifier()
 {
   int t=lex.LookAhead(0);
 
-  return is_identifier(t) || t == TOK_SCOPE || t == TOK_CONSTEXPR ||
-         t == TOK_CONST || t == TOK_VOLATILE || t == TOK_RESTRICT ||
-         t == TOK_CHAR || t == TOK_INT || t == TOK_SHORT || t == TOK_LONG ||
-         t == TOK_CHAR16_T || t == TOK_CHAR32_T || t == TOK_WCHAR_T ||
-         t == TOK_COMPLEX // new !!!
+  return is_identifier(t) || t == TOK_SCOPE || t == TOK_CONST ||
+         t == TOK_VOLATILE || t == TOK_RESTRICT || t == TOK_CHAR ||
+         t == TOK_INT || t == TOK_SHORT || t == TOK_LONG || t == TOK_CHAR16_T ||
+         t == TOK_CHAR32_T || t == TOK_WCHAR_T || t == TOK_COMPLEX // new !!!
          || t == TOK_SIGNED || t == TOK_UNSIGNED || t == TOK_FLOAT ||
          t == TOK_DOUBLE || t == TOK_INT8 || t == TOK_INT16 || t == TOK_INT32 ||
          t == TOK_INT64 || t == TOK_GCC_INT128 || t == TOK_PTR32 ||
@@ -777,7 +778,7 @@ bool Parser::isTypeSpecifier()
          t == TOK_CPROVER_BOOL || t == TOK_CLASS || t == TOK_STRUCT ||
          t == TOK_UNION || t == TOK_ENUM || t == TOK_INTERFACE ||
          t == TOK_TYPENAME || t == TOK_TYPEOF || t == TOK_DECLTYPE ||
-         t == TOK_UNDERLYING_TYPE;
+         t == TOK_UNDERLYING_TYPE || t == TOK_ATOMIC_TYPE_SPECIFIER;
 }
 
 /*
@@ -1031,6 +1032,11 @@ bool Parser::rLinkageBody(cpp_linkage_spect::itemst &items)
 */
 bool Parser::rTemplateDecl(cpp_declarationt &decl)
 {
+#ifdef DEBUG
+  indenter _i;
+  std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl 1\n";
+#endif
+
   TemplateDeclKind kind=tdk_unknown;
 
   make_sub_scope("#template", new_scopet::kindt::TEMPLATE);
@@ -1040,6 +1046,10 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl)
   if(!rTemplateDecl2(template_type, kind))
     return false;
 
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl 2\n";
+#endif
+
   cpp_declarationt body;
   if(lex.LookAhead(0)==TOK_USING)
   {
@@ -1087,11 +1097,20 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl)
 
 bool Parser::rTemplateDecl2(typet &decl, TemplateDeclKind &kind)
 {
+#ifdef DEBUG
+  indenter _i;
+  std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 1\n";
+#endif
+
   cpp_tokent tk;
 
   if(lex.get_token(tk)!=TOK_TEMPLATE)
     return false;
 
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 2\n";
+#endif
+
   decl=typet(ID_template);
   set_location(decl, tk);
 
@@ -1102,17 +1121,33 @@ bool Parser::rTemplateDecl2(typet &decl, TemplateDeclKind &kind)
     return true;        // ignore TEMPLATE
   }
 
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 3\n";
+#endif
+
   if(lex.get_token(tk)!='<')
     return false;
 
   irept &template_parameters=decl.add(ID_template_parameters);
 
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 4\n";
+#endif
+
   if(!rTempArgList(template_parameters))
     return false;
 
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 5\n";
+#endif
+
   if(lex.get_token(tk)!='>')
     return false;
 
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 6\n";
+#endif
+
   // ignore nested TEMPLATE
   while(lex.LookAhead(0)==TOK_TEMPLATE)
   {
@@ -1129,6 +1164,10 @@ bool Parser::rTemplateDecl2(typet &decl, TemplateDeclKind &kind)
       return false;
   }
 
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 7\n";
+#endif
+
   if(template_parameters.get_sub().empty())
     // template < > declaration
     kind=tdk_specialization;
@@ -1176,7 +1215,7 @@ bool Parser::rTempArgList(irept &args)
   : CLASS [Identifier] {'=' type.name}
   | CLASS Ellipsis [Identifier]
   | type.specifier arg.declarator {'=' conditional.expr}
-  | template.decl2 CLASS Identifier {'=' type.name}
+  | template.decl2 CLASS {Identifier {'=' type.name}}
 */
 bool Parser::rTempArgDeclaration(cpp_declarationt &declaration)
 {
@@ -1189,6 +1228,10 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration)
 
   if((t0==TOK_CLASS || t0==TOK_TYPENAME))
   {
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.1\n";
+#endif
+
     cpp_token_buffert::post pos=lex.Save();
 
     cpp_tokent tk1;
@@ -1208,14 +1251,11 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration)
     declarator.type().make_nil();
     set_location(declarator, tk1);
 
-    bool has_ellipsis=false;
-
     if(lex.LookAhead(0)==TOK_ELLIPSIS)
     {
       cpp_tokent tk2;
       lex.get_token(tk2);
-
-      has_ellipsis=true;
+      declarator.set_has_ellipsis();
     }
 
     if(is_identifier(lex.LookAhead(0)))
@@ -1227,16 +1267,15 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration)
       set_location(declarator.name(), tk2);
 
       add_id(declarator.name(), new_scopet::kindt::TYPE_TEMPLATE_PARAMETER);
-
-      if(has_ellipsis)
-      {
-        // TODO
-      }
     }
 
     if(lex.LookAhead(0)=='=')
     {
-      if(has_ellipsis)
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.2\n";
+#endif
+
+      if(declarator.get_has_ellipsis())
         return false;
 
       typet default_type;
@@ -1248,10 +1287,38 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration)
       declarator.value()=exprt(ID_type);
       declarator.value().type().swap(default_type);
     }
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.3\n";
+#endif
 
     if(lex.LookAhead(0)==',' ||
        lex.LookAhead(0)=='>')
       return true;
+#if 0
+    else if(lex.LookAhead(0) == TOK_SHIFTRIGHT)
+    {
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.4\n";
+#endif
+
+      // turn >> into > >
+      cpp_token_buffert::post pos=lex.Save();
+      cpp_tokent tk;
+      lex.get_token(tk);
+      lex.Restore(pos);
+      tk.kind='>';
+      tk.text='>';
+      lex.Replace(tk);
+      lex.Insert(tk);
+      DATA_INVARIANT(lex.LookAhead(0) == '>', "should be >");
+      DATA_INVARIANT(lex.LookAhead(1) == '>', "should be >");
+      return true;
+    }
+#endif
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.5\n";
+#endif
+
 
     lex.Restore(pos);
   }
@@ -1273,9 +1340,14 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration)
 
     cpp_tokent tk1, tk2;
 
-    if(lex.get_token(tk1) != TOK_CLASS || !is_identifier(lex.get_token(tk2)))
+    if(lex.get_token(tk1) != TOK_CLASS)
       return false;
 
+    if(lex.LookAhead(0) == ',' || lex.LookAhead(0) == '>')
+      return true;
+
+    if(!is_identifier(lex.get_token(tk2)))
+      return false;
     // Ptree cspec=new PtreeClassSpec(new LeafReserved(tk1),
     //                                  Ptree::Cons(new Leaf(tk2),nil),
     //                                  nil);
@@ -1309,19 +1381,16 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration)
               << "Parser::rTempArgDeclaration 3\n";
 #endif
 
-    bool has_ellipsis=false;
+    declaration.declarators().resize(1);
+    cpp_declaratort &declarator = declaration.declarators().front();
 
     if(lex.LookAhead(0)==TOK_ELLIPSIS)
     {
       cpp_tokent tk2;
       lex.get_token(tk2);
-
-      has_ellipsis=true;
+      declarator.set_has_ellipsis();
     }
 
-    declaration.declarators().resize(1);
-    cpp_declaratort &declarator=declaration.declarators().front();
-
     if(!rDeclarator(declarator, kArgDeclarator, true, false))
       return false;
 
@@ -1332,16 +1401,11 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration)
 
     add_id(declarator.name(), new_scopet::kindt::NON_TYPE_TEMPLATE_PARAMETER);
 
-    if(has_ellipsis)
-    {
-      // TODO
-    }
-
     exprt &value=declarator.value();
 
     if(lex.LookAhead(0)=='=')
     {
-      if(has_ellipsis)
+      if(declarator.get_has_ellipsis())
         return false;
 
       cpp_tokent tk;
@@ -2018,7 +2082,7 @@ bool Parser::optMemberSpec(cpp_member_spect &member_spec)
 
 /*
   storage.spec : STATIC | EXTERN | AUTO | REGISTER | MUTABLE | ASM |
-                 THREAD_LOCAL
+                 THREAD_LOCAL | CONSTEXPR
 */
 bool Parser::optStorageSpec(cpp_storage_spect &storage_spec)
 {
@@ -2027,7 +2091,7 @@ bool Parser::optStorageSpec(cpp_storage_spect &storage_spec)
   if(
     t == TOK_STATIC || t == TOK_EXTERN || (t == TOK_AUTO && !cpp11) ||
     t == TOK_REGISTER || t == TOK_MUTABLE || t == TOK_GCC_ASM ||
-    t == TOK_THREAD_LOCAL)
+    t == TOK_THREAD_LOCAL || t == TOK_CONSTEXPR)
   {
     cpp_tokent tk;
     lex.get_token(tk);
@@ -2041,6 +2105,9 @@ bool Parser::optStorageSpec(cpp_storage_spect &storage_spec)
     case TOK_MUTABLE: storage_spec.set_mutable(); break;
     case TOK_GCC_ASM: storage_spec.set_asm(); break;
     case TOK_THREAD_LOCAL: storage_spec.set_thread_local(); break;
+    case TOK_CONSTEXPR:
+      storage_spec.set_constexpr();
+      break;
     default: UNREACHABLE;
     }
 
@@ -2051,17 +2118,17 @@ bool Parser::optStorageSpec(cpp_storage_spect &storage_spec)
 }
 
 /*
-  cv.qualify : (CONSTEXPR | CONST | VOLATILE | RESTRICT)+
+  cv.qualify : (CONST | VOLATILE | RESTRICT)+
 */
 bool Parser::optCvQualify(typet &cv)
 {
   for(;;)
   {
     int t=lex.LookAhead(0);
-    if(t==TOK_CONSTEXPR ||
-       t==TOK_CONST || t==TOK_VOLATILE || t==TOK_RESTRICT ||
-       t==TOK_PTR32 || t==TOK_PTR64 ||
-       t==TOK_GCC_ATTRIBUTE || t==TOK_GCC_ASM)
+    if(
+      t == TOK_CONST || t == TOK_VOLATILE || t == TOK_RESTRICT ||
+      t == TOK_PTR32 || t == TOK_PTR64 || t == TOK_GCC_ATTRIBUTE ||
+      t == TOK_GCC_ASM)
     {
       cpp_tokent tk;
       lex.get_token(tk);
@@ -2069,12 +2136,6 @@ bool Parser::optCvQualify(typet &cv)
 
       switch(t)
       {
-      case TOK_CONSTEXPR:
-        p=typet(ID_constexpr);
-        set_location(p, tk);
-        merge_types(p, cv);
-        break;
-
       case TOK_CONST:
         p=typet(ID_const);
         set_location(p, tk);
@@ -2397,7 +2458,7 @@ bool Parser::rGCCAttribute(typet &t)
 
 bool Parser::optAttribute(typet &t)
 {
-  if(lex.LookAhead(0) == TOK_GCC_ATTRIBUTE)
+  while(lex.LookAhead(0) == TOK_GCC_ATTRIBUTE)
   {
     lex.get_token();
 
@@ -2441,6 +2502,17 @@ bool Parser::optAttribute(typet &t)
         break;
       }
 
+      case TOK_GCC_IDENTIFIER:
+        if(tk.text == "clang" && lex.LookAhead(0) == TOK_SCOPE)
+        {
+          exprt discarded;
+          if(!rExpression(discarded, false))
+            return false;
+        }
+        else
+          return false;
+        break;
+
     default:
       // TODO: way may wish to change this: GCC, Clang, Visual Studio merely
       // warn when they see an attribute that they don't recognize
@@ -2676,8 +2748,34 @@ bool Parser::optIntegralTypeOrClassSpec(typet &p)
 
     return true;
   }
+  else if(t == TOK_ATOMIC_TYPE_SPECIFIER)
+  {
+#ifdef DEBUG
+    std::cout << std::string(__indent, ' ')
+              << "Parser::optIntegralTypeOrClassSpec 9\n";
+#endif // DEBUG
+    cpp_tokent atomic_tk;
+    lex.get_token(atomic_tk);
+
+    cpp_tokent tk;
+    if(lex.get_token(tk)!='(')
+      return false;
+
+    // the argument is always a type
+    if(!rTypeSpecifier(p, false))
+      return false;
+
+    if(lex.get_token(tk)!=')')
+      return false;
+
+    return true;
+  }
   else
   {
+#ifdef DEBUG
+    std::cout << std::string(__indent, ' ')
+              << "Parser::optIntegralTypeOrClassSpec 10\n";
+#endif // DEBUG
     p.make_nil();
     return true;
   }
@@ -3088,8 +3186,18 @@ bool Parser::rDeclarator(
   if(!rDeclaratorQualifier())
     return false;
 
+  if(lex.LookAhead(0)==TOK_ELLIPSIS && lex.LookAhead(1)!=')')
+  {
+    cpp_tokent tk;
+    lex.get_token(tk);
+    d_outer.set(ID_ellipsis, true);
+  }
+
 #ifdef DEBUG
-  std::cout << std::string(__indent, ' ') << "Parser::rDeclarator2 2\n";
+  std::cout << std::string(__indent, ' ') << "Parser::rDeclarator2 2 "
+              << lex.LookAhead(0)
+              << ' ' << lex.peek().text
+              << '\n';
 #endif
 
   t=lex.LookAhead(0);
@@ -3553,7 +3661,11 @@ bool Parser::rName(irept &name)
 {
 #ifdef DEBUG
   indenter _i;
-  std::cout << std::string(__indent, ' ') << "Parser::rName 0\n";
+  std::cout << std::string(__indent, ' ') << "Parser::rName 0 "
+              << lex.LookAhead(0)
+              << ' ' << lex.peek().text
+              << ' ' << lex.Save()
+              << '\n';
 #endif
 
   name=cpp_namet();
@@ -3675,6 +3787,34 @@ bool Parser::rName(irept &name)
         return true;
       break;
 
+    case TOK_DECLTYPE:
+#ifdef DEBUG
+      std::cout << std::string(__indent, ' ') << "Parser::rName 9\n";
+#endif
+      lex.get_token(tk);
+      {
+        components.push_back(typet{ID_decltype});
+        set_location(components.back(), tk);
+
+        if(lex.get_token(tk)!='(')
+          return false;
+
+        // the argument is always an expression
+
+        exprt expr;
+        if(!rCommaExpression(expr))
+          return false;
+
+        if(lex.get_token(tk)!=')')
+          return false;
+
+        components.back().add(ID_expr_arg).swap(expr);
+
+        if(lex.LookAhead(0) != TOK_SCOPE)
+          return false;
+      }
+      break;
+
     default:
       return false;
     }
@@ -3988,7 +4128,8 @@ bool Parser::rTemplateArgs(irept &template_args)
         )
     {
 #ifdef DEBUG
-      std::cout << std::string(__indent, ' ') <<  "Parser::rTemplateArgs 4\n";
+      std::cout << std::string(__indent, ' ') <<  "Parser::rTemplateArgs 4 " <<
+        lex.LookAhead(0) << "\n";
 #endif
 
       // ok
@@ -4000,21 +4141,30 @@ bool Parser::rTemplateArgs(irept &template_args)
       lex.Restore(pos);
       exprt tmp;
       if(rConditionalExpr(tmp, true))
+      {
+#ifdef DEBUG
+      std::cout << std::string(__indent, ' ') <<  "Parser::rTemplateArgs 4.0\n";
+#endif
         exp.id(ID_ambiguous);
+      }
 #ifdef DEBUG
       std::cout << std::string(__indent, ' ') <<  "Parser::rTemplateArgs 4.1\n";
 #endif
       lex.Restore(pos);
       rTypeNameOrFunctionType(a);
 
+#ifdef DEBUG
+      std::cout << std::string(__indent, ' ') <<  "Parser::rTemplateArgs 4.1a " <<
+        lex.LookAhead(0) << "\n";
+#endif
       if(lex.LookAhead(0)==TOK_ELLIPSIS)
       {
         lex.get_token(tk1);
-
-        // TODO
+        exp.set(ID_ellipsis, true);
       }
 #ifdef DEBUG
-      std::cout << std::string(__indent, ' ') <<  "Parser::rTemplateArgs 4.2\n";
+      std::cout << std::string(__indent, ' ') <<  "Parser::rTemplateArgs 4.2 " <<
+        lex.LookAhead(0) << "\n";
 #endif
     }
     else
@@ -4033,8 +4183,7 @@ bool Parser::rTemplateArgs(irept &template_args)
       if(lex.LookAhead(0)==TOK_ELLIPSIS)
       {
         lex.get_token(tk1);
-
-        // TODO
+        exp.set(ID_ellipsis, true);
       }
     }
 
@@ -4090,9 +4239,20 @@ bool Parser::rArgDeclListOrInit(
   bool &is_args,
   bool maybe_init)
 {
+#ifdef DEBUG
+  indenter _i;
+  std::cout << std::string(__indent, ' ') << "Parser::rArgDeclListOrInit 0 "
+              << lex.LookAhead(0)
+              << ' ' << lex.peek().text
+              << '\n';
+#endif
+
   cpp_token_buffert::post pos=lex.Save();
   if(maybe_init)
   {
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rArgDeclListOrInit 1" << std::endl;
+#endif
     if(rFunctionArguments(arglist))
       if(lex.LookAhead(0)==')')
       {
@@ -4106,12 +4266,18 @@ bool Parser::rArgDeclListOrInit(
   }
   else
   {
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rArgDeclListOrInit 2" << std::endl;
+#endif
     is_args = rArgDeclList(arglist);
 
     if(is_args)
       return true;
     else
     {
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rArgDeclListOrInit 3" << std::endl;
+#endif
       lex.Restore(pos);
       // encode.Clear();
       return rFunctionArguments(arglist);
@@ -4126,11 +4292,22 @@ bool Parser::rArgDeclListOrInit(
 */
 bool Parser::rArgDeclList(irept &arglist)
 {
+#ifdef DEBUG
+  indenter _i;
+  std::cout << std::string(__indent, ' ') << "Parser::rArgDeclList 0 "
+              << lex.LookAhead(0)
+              << ' ' << lex.peek().text
+              << '\n';
+#endif
+
   irept list;
 
   list.clear();
   for(;;)
   {
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rArgDeclList 1" << std::endl;
+#endif
     cpp_declarationt declaration;
 
     int t=lex.LookAhead(0);
@@ -4138,6 +4315,9 @@ bool Parser::rArgDeclList(irept &arglist)
       break;
     else if(t==TOK_ELLIPSIS)
     {
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rArgDeclList 2" << std::endl;
+#endif
       cpp_tokent tk;
       lex.get_token(tk);
       list.get_sub().push_back(irept(ID_ellipsis));
@@ -4145,18 +4325,25 @@ bool Parser::rArgDeclList(irept &arglist)
     }
     else if(rArgDeclaration(declaration))
     {
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rArgDeclList 3 "
+              << lex.LookAhead(0)
+              << ' ' << lex.peek().text
+              << '\n';
+#endif
       cpp_tokent tk;
 
       list.get_sub().push_back(irept(irep_idt()));
       list.get_sub().back().swap(declaration);
-      t=lex.LookAhead(0);
-      if(t==',')
-        lex.get_token(tk);
-      else if(t==TOK_ELLIPSIS)
+      if(lex.LookAhead(0)==TOK_ELLIPSIS)
       {
         lex.get_token(tk);
         list.get_sub().push_back(irept(ID_ellipsis));
       }
+
+      t=lex.LookAhead(0);
+      if(t==',')
+        lex.get_token(tk);
       else if(t!=')' && t!=TOK_ELLIPSIS)
         return false;
     }
@@ -4224,11 +4411,23 @@ bool Parser::rArgDeclaration(cpp_declarationt &declaration)
 */
 bool Parser::rInitializeExpr(exprt &expr)
 {
+#ifdef DEBUG
+  indenter _i;
+  std::cout << std::string(__indent, ' ') << "Parser::rInitializeExpr 0 "
+              << lex.LookAhead(0)
+              << ' ' << lex.peek().text
+              << '\n';
+#endif
+
   if(lex.LookAhead(0)!='{')
     return rExpression(expr, false);
 
   // we want { initialize_expr, ... }
 
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rInitializeExpr 1\n";
+#endif
+
   cpp_tokent tk;
   lex.get_token(tk);
 
@@ -4306,12 +4505,17 @@ bool Parser::rInitializeExpr(exprt &expr)
 /*
   function.arguments
   : empty
-  | expression (',' expression)*
+  | initializer.expr (',' initializer.expr)*
 
   This assumes that the next token following function.arguments is ')'.
 */
 bool Parser::rFunctionArguments(exprt &args)
 {
+#ifdef DEBUG
+  indenter _i;
+  std::cout << std::string(__indent, ' ') << "Parser::rFunctionArguments 1\n";
+#endif
+
   exprt exp;
   cpp_tokent tk;
 
@@ -4321,11 +4525,19 @@ bool Parser::rFunctionArguments(exprt &args)
 
   for(;;)
   {
-    if(!rExpression(exp, false))
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rFunctionArguments 2\n";
+#endif
+
+    if(!rInitializeExpr(exp))
       return false;
 
     args.add_to_operands(std::move(exp));
 
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rFunctionArguments 3\n";
+#endif
+
     if(lex.LookAhead(0)==TOK_ELLIPSIS &&
        (lex.LookAhead(1)==')' || lex.LookAhead(1)==','))
     {
@@ -4374,6 +4586,9 @@ bool Parser::rEnumSpec(typet &spec)
     spec.set(ID_C_class, true);
   }
 
+  if(!optAttribute(spec))
+    return false;
+
   if(lex.LookAhead(0)!='{' &&
      lex.LookAhead(0)!=':')
   {
@@ -4452,6 +4667,10 @@ bool Parser::rEnumBody(irept &body)
     set_location(n, tk);
     n.set(ID_name, tk.data.get(ID_C_base_name));
 
+    typet discarded_attribute;
+    if(!optAttribute(discarded_attribute))
+      return false;
+
     if(lex.LookAhead(0, tk2)=='=') // set the constant
     {
       lex.get_token(tk2); // read the '='
@@ -4860,7 +5079,9 @@ bool Parser::rCommaExpression(exprt &exp)
 
 /*
   expression
-  : conditional.expr {(AssignOp | '=') expression}        right-to-left
+  : conditional.expr
+  | logical.or.expr (AssignOp | '=') initialize.expr
+  | throw.expression
 */
 bool Parser::rExpression(exprt &exp, bool template_args)
 {
@@ -4871,7 +5092,30 @@ bool Parser::rExpression(exprt &exp, bool template_args)
   std::cout << std::string(__indent, ' ') << "Parser::rExpression 0\n";
 #endif
 
-  if(!rConditionalExpr(exp, template_args))
+  if(lex.LookAhead(0) == TOK_THROW)
+    return rThrowExpr(exp);
+
+  cpp_token_buffert::post pos=lex.Save();
+
+  // see whether we have logical.or.expr followed by '?'; the parsed expression
+  // will be discarded and be parsed again, below
+  exprt tmp;
+  if(!rLogicalOrExpr(tmp, template_args))
+    return false;
+
+  if(lex.LookAhead(0) == '?')
+  {
+    lex.Restore(pos);
+    return rConditionalExpr(exp, template_args);
+  }
+
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rExpression 0.1\n";
+#endif
+
+  lex.Restore(pos);
+
+  if(!rLogicalOrExpr(exp, template_args))
     return false;
 
 #ifdef DEBUG
@@ -4893,7 +5137,7 @@ bool Parser::rExpression(exprt &exp, bool template_args)
 #endif
 
     exprt right;
-    if(!rExpression(right, template_args))
+    if(!rInitializeExpr(right))
       return false;
 
 #ifdef DEBUG
@@ -4941,7 +5185,7 @@ bool Parser::rExpression(exprt &exp, bool template_args)
 
 /*
   conditional.expr
-  : logical.or.expr {'?' comma.expression ':' conditional.expr}  right-to-left
+  : logical.or.expr {'?' comma.expression ':' expression}  right-to-left
 */
 bool Parser::rConditionalExpr(exprt &exp, bool template_args)
 {
@@ -4996,7 +5240,10 @@ bool Parser::rLogicalOrExpr(exprt &exp, bool template_args)
 {
 #ifdef DEBUG
   indenter _i;
-  std::cout << std::string(__indent, ' ') << "Parser::rLogicalOrExpr 0\n";
+  std::cout << std::string(__indent, ' ') << "Parser::rLogicalOrExpr 0 "
+              << lex.LookAhead(0)
+              << ' ' << lex.peek().text
+              << '\n';
 #endif
 
   if(!rLogicalAndExpr(exp, template_args))
@@ -5462,6 +5709,7 @@ bool Parser::rPmExpr(exprt &exp)
   cast.expr
   : unary.expr
   | '(' type.name ')' cast.expr
+  | '(' type.name ')' initializer.expr  -- GCC/Clang extension
 */
 bool Parser::rCastExpr(exprt &exp)
 {
@@ -5499,6 +5747,20 @@ bool Parser::rCastExpr(exprt &exp)
           // we have (x) & 123
           // This is likely a binary bit-wise 'and'
         }
+        else if(lex.LookAhead(0)=='{')
+        {
+          // this is a GCC/Clang extension
+          exprt exp2;
+          if(!rInitializeExpr(exp2))
+            return false;
+
+          exp=exprt("explicit-typecast");
+          exp.type().swap(tname);
+          exp.add_to_operands(std::move(exp2));
+          set_location(exp, tk1);
+
+          return true;
+        }
         else if(rCastExpr(exp))
         {
           exprt op;
@@ -5688,18 +5950,21 @@ bool Parser::rTypeNameOrFunctionType(typet &tname)
       type.parameters().push_back(parameter);
 
       t=lex.LookAhead(0);
-      if(t==',')
+      if(t == TOK_ELLIPSIS)
       {
         cpp_tokent tk;
         lex.get_token(tk);
+        to_cpp_declaration(type.parameters().back())
+          .declarators()
+          .back()
+          .set_has_ellipsis();
+        t = lex.LookAhead(0);
       }
-      else if(t==TOK_ELLIPSIS)
+
+      if(t == ',')
       {
-        // TODO -- this is actually ambiguous as it could refer to a
-        // template parameter pack or declare a variadic function
         cpp_tokent tk;
         lex.get_token(tk);
-        type.make_ellipsis();
       }
       else if(t==')')
         break;
@@ -5742,9 +6007,9 @@ bool Parser::rTypeNameOrFunctionType(typet &tname)
   : postfix.expr
   | ('*' | '&' | '+' | '-' | '!' | '~' | IncOp) cast.expr
   | sizeof.expr
-  | allocate.expr
-  | throw.expression
+  | alignof.expr
   | noexcept.expr
+  | allocate.expr
 */
 
 bool Parser::rUnaryExpr(exprt &exp)
@@ -5824,8 +6089,6 @@ bool Parser::rUnaryExpr(exprt &exp)
     return rSizeofExpr(exp);
   else if(t==TOK_ALIGNOF)
     return rAlignofExpr(exp);
-  else if(t==TOK_THROW)
-    return rThrowExpr(exp);
   else if(t==TOK_NOEXCEPT)
     return rNoexceptExpr(exp);
   else if(t==TOK_REAL || t==TOK_IMAG)
@@ -6057,7 +6320,7 @@ bool Parser::rAlignofExpr(exprt &exp)
 
 /*
   noexcept.expr
-  : NOEXCEPT '(' expression ')'
+  : NOEXCEPT '(' comma.expression ')'
 */
 bool Parser::rNoexceptExpr(exprt &exp)
 {
@@ -6071,29 +6334,24 @@ bool Parser::rNoexceptExpr(exprt &exp)
   if(lex.get_token(tk)!=TOK_NOEXCEPT)
     return false;
 
-  if(lex.LookAhead(0)=='(')
-  {
-    exprt subexp;
-    cpp_tokent op, cp;
+  if(lex.LookAhead(0)!='(')
+    return false;
 
-    lex.get_token(op);
+  exprt subexp;
+  cpp_tokent op, cp;
 
-    if(rExpression(subexp, false))
-    {
-      if(lex.get_token(cp)==')')
-      {
-        // TODO
-        exp=exprt(ID_noexcept);
-        exp.add_to_operands(std::move(subexp));
-        set_location(exp, tk);
-        return true;
-      }
-    }
-  }
-  else
-    return true;
+  lex.get_token(op);
 
-  return false;
+  if(!rCommaExpression(subexp))
+    return false;
+
+  if(lex.get_token(cp)!=')')
+    return false;
+
+  exp=exprt(ID_noexcept);
+  exp.add_to_operands(std::move(subexp));
+  set_location(exp, tk);
+  return true;
 }
 
 bool Parser::isAllocateExpr(int t)
@@ -6106,7 +6364,7 @@ bool Parser::isAllocateExpr(int t)
 
 /*
   allocate.expr
-  : {Scope | userdef.keyword} NEW allocate.type
+  : {Scope} NEW allocate.type
   | {Scope} DELETE {'[' ']'} cast.expr
 */
 bool Parser::rAllocateExpr(exprt &exp)
@@ -6367,31 +6625,140 @@ bool Parser::rAllocateInitializer(exprt &init)
   return true;
 }
 
+static bool isCppCastExpr(int t)
+{
+  return t == TOK_DYNAMIC_CAST || t == TOK_STATIC_CAST || t == TOK_REINTERPRET_CAST || t == TOK_CONST_CAST;
+}
+
 /*
-  postfix.exp
-  : primary.exp
+  postfix.expr
+  : primary.expr
   | postfix.expr '[' comma.expression ']'
+  | postfix.expr '[' initializer.expr ']'
   | postfix.expr '(' function.arguments ')'
+  | integral.or.class.spec '(' function.arguments ')'
+  | integral.or.class.spec initializer.expr
+  | postfix.expr '.' userdef.statement
+  | postfix.expr ArrowOp userdef.statement
   | postfix.expr '.' var.name
   | postfix.expr ArrowOp var.name
   | postfix.expr IncOp
-  | openc++.postfix.expr
-
-  openc++.postfix.expr
-  : postfix.expr '.' userdef.statement
-  | postfix.expr ArrowOp userdef.statement
-
-  Note: function-style casts are accepted as function calls.
+  | c++cast.expr
+  | typeid.expr
 */
 bool Parser::rPostfixExpr(exprt &exp)
 {
 #ifdef DEBUG
   indenter _i;
-  std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0\n";
+  std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0 "
+              << lex.LookAhead(0)
+              << ' ' << lex.peek().text
+              << ' ' << lex.Save()
+              << '\n';
 #endif
 
-  if(!rPrimaryExpr(exp))
-    return false;
+  typet type;
+
+  cpp_token_buffert::post pos=lex.Save();
+
+  if(isCppCastExpr(lex.LookAhead(0)))
+  {
+    if(!rCppCastExpr(exp))
+      return false;
+  }
+  else if(lex.LookAhead(0) == TOK_TYPEID)
+  {
+    if(!rTypeidExpr(exp))
+      return false;
+  }
+  // try to see whether this is explicit type conversion, else it has to be
+  // a primary-expression
+  else 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(tk.kind == '{')
+    {
+      if(!rInitializeExpr(exp2))
+        return false;
+    }
+    else
+    {
+      // tk.kind == '('
+      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);
+#ifdef DEBUG
+  std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0.2\n";
+#endif
+
+    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.3\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
+    {
+#ifdef DEBUG
+      std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0.4\n";
+#endif
+      lex.Restore(pos);
+      if(!rPrimaryExpr(exp))
+        return false;
+    }
+  }
 
 #ifdef DEBUG
   std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 1\n";
@@ -6407,7 +6774,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
@@ -6428,11 +6802,11 @@ bool Parser::rPostfixExpr(exprt &exp)
       break;
 
     case '(':
+      lex.get_token(op);
 #ifdef DEBUG
       std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 3\n";
 #endif
 
-      lex.get_token(op);
       if(!rFunctionArguments(e))
         return false;
 
@@ -6516,6 +6890,48 @@ bool Parser::rPostfixExpr(exprt &exp)
   }
 }
 
+/*
+  c++cast.expr
+  : castOp '<' type.name '>' '(' comma.expression ')'
+*/
+bool Parser::rCppCastExpr(exprt &expr)
+{
+  cpp_tokent tk;
+
+  lex.get_token(tk);
+
+  expr.id(irep_idt(tk.text));
+  set_location(expr, tk);
+
+  if(!isCppCastExpr(tk.kind))
+    return false;
+
+  if(lex.get_token(tk) != '<')
+    return false;
+
+  typet tname;
+  if(!rTypeName(tname))
+    return false;
+
+  if(lex.get_token(tk) != '>')
+    return false;
+
+  if(lex.get_token(tk) != '(')
+    return false;
+
+  exprt op;
+  if(!rCommaExpression(op))
+    return false;
+
+  if(lex.get_token(tk) != ')')
+    return false;
+
+  expr.type().swap(tname);
+  expr.add_to_operands(std::move(op));
+
+  return true;
+}
+
 /*
   __uuidof( expression )
   __uuidof( type )
@@ -6726,9 +7142,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
   | nullptr
@@ -6740,7 +7153,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
 #ifdef DEBUG
   indenter _i;
   std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 0 "
-            << lex.LookAhead(0) << ' ' << lex.current_token().text << '\n';
+            << lex.LookAhead(0) << ' ' << lex.peek().text << '\n';
 #endif
 
   switch(lex.LookAhead(0))
@@ -6845,15 +7258,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);
-
   case TOK_UNARY_TYPE_PREDICATE:
   case TOK_BINARY_TYPE_PREDICATE:
 #ifdef DEBUG
@@ -6880,75 +7284,9 @@ bool Parser::rPrimaryExpr(exprt &exp)
 #ifdef DEBUG
     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;
-
-        if(lex.LookAhead(0)==TOK_SCOPE)
-        {
-          lex.get_token(tk);
+    if(!rVarName(exp))
+      return false;
 
-          // exp=new PtreeStaticUserStatementExpr(exp,
-          //                        Ptree::Cons(new Leaf(tk), exp2));
-          // TODO
-        }
-      }
-    }
 #ifdef DEBUG
     std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 17\n";
 #endif
@@ -6971,7 +7309,11 @@ bool Parser::rVarName(exprt &name)
 {
 #ifdef DEBUG
   indenter _i;
-  std::cout << std::string(__indent, ' ') << "Parser::rVarName 0\n";
+  std::cout << std::string(__indent, ' ') << "Parser::rVarName 0 "
+              << lex.LookAhead(0)
+              << ' ' << lex.peek().text
+              << ' ' << lex.Save()
+              << '\n';
 #endif
 
   if(rVarNameCore(name))
@@ -7107,6 +7449,34 @@ bool Parser::rVarNameCore(exprt &name)
       }
       return true;
 
+    case TOK_DECLTYPE:
+#ifdef DEBUG
+      std::cout << std::string(__indent, ' ') << "Parser::rVarNameCore 8\n";
+#endif
+      lex.get_token(tk);
+      {
+        components.push_back(typet{ID_decltype});
+        set_location(components.back(), tk);
+
+        if(lex.get_token(tk)!='(')
+          return false;
+
+        // the argument is always an expression
+
+        exprt expr;
+        if(!rCommaExpression(expr))
+          return false;
+
+        if(lex.get_token(tk)!=')')
+          return false;
+
+        components.back().add(ID_expr_arg).swap(expr);
+
+        if(lex.LookAhead(0) != TOK_SCOPE)
+          return false;
+      }
+      break;
+
     default:
       return false;
     }
@@ -7414,6 +7784,14 @@ std::optional<codet> Parser::rStatement()
 #endif
       lex.get_token(tk2);
     }
+    else if(lex.LookAhead(0) == '{')
+    {
+      if(!rInitializeExpr(statement.return_value()))
+        return {};
+
+      if(lex.get_token(tk2)!=';')
+        return {};
+    }
     else
     {
 #ifdef DEBUG
@@ -7565,7 +7943,9 @@ std::optional<codet> Parser::rStatement()
       if(!rUsing(cpp_using))
         return {};
 
-      UNIMPLEMENTED;
+      codet statement(ID_cpp_using);
+      // UNIMPLEMENTED;
+      return std::move(statement);
     }
 
   case TOK_STATIC_ASSERT:
@@ -7582,6 +7962,14 @@ std::optional<codet> Parser::rStatement()
       return std::move(statement);
     }
 
+  case '[':
+    {
+      typet discard;
+      if(!optAttribute(discard))
+        return {};
+      return code_blockt{};
+    }
+
   default:
     return rExprStatement();
   }