diff --git a/build.sc b/build.sc
index 9968329aa5..c22e10d9ee 100644
--- a/build.sc
+++ b/build.sc
@@ -41,19 +41,20 @@ object col extends VercorsModule {
 
 
 object parsers extends VercorsModule {
-  def key = "parsers"
-  def generatedSources = T.sources {
-    Seq(
-      antlr.c.generate(),
-      antlr.java.generate(),
-      antlr.pvl.generate(),
-			antlr.llvm.generate(),
-    )
-  }
-  def deps = Agg(
-    ivy"org.antlr:antlr4-runtime:4.8"
-  )
-  def moduleDeps = Seq(hre, col)
+	def key = "parsers"
+	def generatedSources = T.sources {
+		Seq(
+			antlr.c.generate(),
+			antlr.cpp.generate(),
+			antlr.java.generate(),
+			antlr.pvl.generate(),
+      antlr.llvm.generate(),
+		)
+	}
+	def deps = Agg(
+		ivy"org.antlr:antlr4-runtime:4.8"
+	)
+	def moduleDeps = Seq(hre, col)
 }
 
 object rewrite extends VercorsModule {
diff --git a/examples/concepts/cpp/Arrays.cpp b/examples/concepts/cpp/Arrays.cpp
new file mode 100644
index 0000000000..efd21c6a74
--- /dev/null
+++ b/examples/concepts/cpp/Arrays.cpp
@@ -0,0 +1,21 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Loops
+//:: tools silicon
+//:: verdict Pass
+
+//@ requires size > 0;
+//@ context \pointer(a, size, read);
+//@ requires (\forall int i = 0 .. size; {: a[i] :} == 0);
+//@ ensures \result == b;
+int sumWithLast(int a[], int size, int b) {
+	int sum = a[size-1] + b;
+	//@ assert a[size-1] == 0;
+	return sum;
+}
+
+//@ requires size > 2;
+//@ context \pointer(a, size, write);
+//@ ensures a[2] == 5;
+void writeToArray(int a[], int size) {
+	a[2] = 5;
+}
\ No newline at end of file
diff --git a/examples/concepts/cpp/Conditionals.cpp b/examples/concepts/cpp/Conditionals.cpp
new file mode 100644
index 0000000000..3ed2e6bc18
--- /dev/null
+++ b/examples/concepts/cpp/Conditionals.cpp
@@ -0,0 +1,33 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Conditionals
+//:: tools silicon
+//:: verdict Pass
+
+void onlyAssignInIf() {
+	int num = 5;
+	int result;
+	if (num < 10) {
+		result = 10;
+	}
+	//@ assert result == 10;
+}
+
+void matchIf() {
+	int num = 5;
+	int result = 0;
+	if (num < 10) {
+		result = 10;
+	}
+	//@ assert result == 10;
+}
+
+void matchElse() {
+	int num = 5;
+	int result = 0;
+	if (num < 5) {
+		result = 10;
+	} else {
+		result = 20;
+	}
+	//@ assert result == 20;
+}
\ No newline at end of file
diff --git a/examples/concepts/cpp/Loops.cpp b/examples/concepts/cpp/Loops.cpp
new file mode 100644
index 0000000000..f8de6bae5b
--- /dev/null
+++ b/examples/concepts/cpp/Loops.cpp
@@ -0,0 +1,26 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Loops
+//:: tools silicon
+//:: verdict Pass
+
+
+void whileLoop() {
+	int numLoops = 10;
+	//@ decreases numLoops;
+	//@ loop_invariant numLoops >= 0;
+	while(numLoops > 0) {
+		numLoops--;
+	}
+}
+
+//@ context_everywhere size >= 0;
+//@ context_everywhere \pointer(arr, size, read);
+void forArrayLoop(bool arr[], int size) {
+	bool sum = true;
+
+	//@ loop_invariant i >= 0 && i <= size;
+	//@ loop_invariant sum == (\forall int j; j >= 0 && j < i; arr[j]);
+	for(int i = 0; i < size; i++) {
+		sum = sum && arr[i];
+	}
+}
diff --git a/examples/concepts/cpp/Namespaces.cpp b/examples/concepts/cpp/Namespaces.cpp
new file mode 100644
index 0000000000..f732fd0107
--- /dev/null
+++ b/examples/concepts/cpp/Namespaces.cpp
@@ -0,0 +1,48 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Namespaces
+//:: tools silicon
+//:: verdict Pass
+
+int x;
+
+namespace spaceA {
+	int x;
+
+	//@ context Perm(x, write);
+	//@ ensures x == 90;
+	//@ ensures \result == \old(x) + 1;
+	int incr() {
+		int newX = x + 1;
+		x = 90;
+		return newX;
+	}
+
+	namespace spaceB {
+		//@ context Perm(x, 0.5);
+		//@ ensures \result == x + 2;
+		int incr() {
+  		return x + 2;
+  	}
+
+  	void doNothing() {};
+	}
+}
+
+//@ context Perm(spaceA::x, write);
+//@ context Perm(x, write);
+int main() {
+	x = 99;
+	spaceA::x = 5;
+	//@ assert spaceA::x == 5;
+  int varA = spaceA::incr();
+  //@ assert varA == 6;
+  //@ assert spaceA::x == 90;
+  int varB = spaceA::spaceB::incr();
+  //@ assert varB == 92;
+  spaceA::spaceB::doNothing();
+  int varX = spaceA::x;
+  //@ assert varX == 90;
+
+  //@ assert x == 99;
+  return 0;
+}
\ No newline at end of file
diff --git a/examples/concepts/cpp/NamespacesDoNotFindWithoutNamespacePrefix.cpp b/examples/concepts/cpp/NamespacesDoNotFindWithoutNamespacePrefix.cpp
new file mode 100644
index 0000000000..d9e7ff8f04
--- /dev/null
+++ b/examples/concepts/cpp/NamespacesDoNotFindWithoutNamespacePrefix.cpp
@@ -0,0 +1,15 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases NamespacesDoNotFindWithoutNamespacePrefix
+//:: tools silicon
+//:: verdict Fail
+
+namespace spaceA {
+
+	namespace spaceB {
+	  int b = 10;
+	}
+
+	int getB() {
+	   return b;
+	}
+}
\ No newline at end of file
diff --git a/examples/concepts/cpp/Operators.cpp b/examples/concepts/cpp/Operators.cpp
new file mode 100644
index 0000000000..37e4da2ff6
--- /dev/null
+++ b/examples/concepts/cpp/Operators.cpp
@@ -0,0 +1,88 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Operators
+//:: tools silicon
+//:: verdict Pass
+
+void test() {
+
+    int num = 5;
+
+    int numPlus = num + 5;
+    //@ assert numPlus == 10;
+
+    int numMinus = num - 5;
+    //@ assert numMinus == 0;
+
+    int numMult = num * 5;
+    //@ assert numMult == 25;
+
+    int numDiv = num / 5;
+    //@ assert numDiv == 1;
+
+    int numMod = num % 5;
+    //@ assert numMod == 0;
+
+    num++;
+    //@ assert num == 6;
+
+    num--;
+    //@ assert num == 5;
+
+    num += 5;
+    //@ assert num == 10;
+
+    num -= 5;
+    //@ assert num == 5;
+
+    num *= 5;
+    //@ assert num == 25;
+
+    num /= 5;
+    //@ assert num == 5;
+
+    num %= 5;
+    //@ assert num == 0;
+
+    int numMinus2 = -5;
+    //@ assert numMinus2 == -5;
+
+    int numPlus2 = +5;
+    //@ assert numPlus2 == 5;
+
+    bool boolean = true;
+
+    bool booleanNot = !boolean;
+    //@ assert booleanNot == false;
+
+    bool booleanNot2 = not boolean;
+    //@ assert booleanNot2 == false;
+
+    bool booleanAnd = boolean && false;
+    //@ assert booleanAnd == false;
+
+    bool booleanOr = boolean || false;
+    //@ assert booleanOr == true;
+
+    bool booleanEquals = boolean == true;
+    //@ assert booleanEquals == true;
+
+    bool booleanNotEquals = boolean != true;
+    //@ assert booleanNotEquals == false;
+
+    num = 5;
+
+    bool booleanLess = num < 6;
+    //@ assert booleanLess == true;
+
+    bool booleanLessEq = num <= 5;
+    //@ assert booleanLessEq == true;
+
+    bool booleanGreater = num > 4;
+    //@ assert booleanGreater == true;
+
+    bool booleanGreaterEq = num >= 5;
+    //@ assert booleanGreaterEq == true;
+
+    //@ assert 4 - 3 - 2 - 1 == (((4 - 3) - 2) - 1);
+
+}
\ No newline at end of file
diff --git a/examples/concepts/cpp/Pointers.cpp b/examples/concepts/cpp/Pointers.cpp
new file mode 100644
index 0000000000..61b926c08e
--- /dev/null
+++ b/examples/concepts/cpp/Pointers.cpp
@@ -0,0 +1,12 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Pointers
+//:: tools silicon
+//:: verdict Pass
+
+//@ context \pointer(ints, size, write);
+void test(int ints[], int size, int* p) {
+	int* intsPtr = ints;
+	//@ assert intsPtr == ints;
+
+	void* voidPtr = nullptr;
+}
\ No newline at end of file
diff --git a/examples/concepts/cpp/Scoping.cpp b/examples/concepts/cpp/Scoping.cpp
new file mode 100644
index 0000000000..00afe14a01
--- /dev/null
+++ b/examples/concepts/cpp/Scoping.cpp
@@ -0,0 +1,17 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Scoping
+//:: tools silicon
+//:: verdict Pass
+void test() {
+	int a = 10;
+	int b = 10;
+
+	{
+		a = 20;
+		int b = 20;
+		//@ assert a == 20;
+		//@ assert b == 20;
+	}
+	//@ assert a == 20;
+	//@ assert b == 10;
+}
\ No newline at end of file
diff --git a/examples/concepts/cpp/Types.cpp b/examples/concepts/cpp/Types.cpp
new file mode 100644
index 0000000000..1e40272177
--- /dev/null
+++ b/examples/concepts/cpp/Types.cpp
@@ -0,0 +1,17 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Types
+//:: tools silicon
+//:: verdict Pass
+
+void test() {
+	bool aBool = true;
+
+	int anInt = 5;
+	long aLong = 5;
+	double aDouble = 5.1;
+	float aFloat = 5.1;
+
+	char aChar = 'a';
+
+	void* voidPtr = nullptr;
+}
\ No newline at end of file
diff --git a/examples/concepts/cpp/methods/AbstractMethod.cpp b/examples/concepts/cpp/methods/AbstractMethod.cpp
new file mode 100644
index 0000000000..c47b09298a
--- /dev/null
+++ b/examples/concepts/cpp/methods/AbstractMethod.cpp
@@ -0,0 +1,13 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases AbstractMethod
+//:: tools silicon
+//:: verdict Pass
+
+/*@ ghost
+	ensures \result == a >= 0;
+	bool isPositive(int a);
+*/
+
+//@ requires b != 0;
+//@ ensures \result == a / b;
+int div(int a, int b);
\ No newline at end of file
diff --git a/examples/concepts/cpp/methods/ContextAndContextEverywhere.cpp b/examples/concepts/cpp/methods/ContextAndContextEverywhere.cpp
new file mode 100644
index 0000000000..1624f1dce1
--- /dev/null
+++ b/examples/concepts/cpp/methods/ContextAndContextEverywhere.cpp
@@ -0,0 +1,23 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases ContextAndContextEverywhere
+//:: tools silicon
+//:: verdict Pass
+
+//@ context b != 0;
+// requires b != 0;
+// ensures b != 0;
+int div(int a, int b) {
+	return a / b;
+}
+
+//@ context_everywhere number > 0;
+// requires number > 0;
+// ensures number > 0;
+int factorial(int number) {
+	int result = 1;
+	// loop_invariant number > 0;
+	for(int i = 2; i <= number; i++) {
+		result *= i;
+	}
+	return result;
+}
\ No newline at end of file
diff --git a/examples/concepts/cpp/methods/Decreases.cpp b/examples/concepts/cpp/methods/Decreases.cpp
new file mode 100644
index 0000000000..f5dfdeee49
--- /dev/null
+++ b/examples/concepts/cpp/methods/Decreases.cpp
@@ -0,0 +1,12 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Decreases
+//:: tools silicon
+//:: verdict Pass
+
+//@ decreases number;
+int factorial(int number) {
+	if (number <= 1) {
+		return 1;
+	}
+	return number * factorial(number - 1);
+}
\ No newline at end of file
diff --git a/examples/concepts/cpp/methods/GhostMethodsAndVariables.cpp b/examples/concepts/cpp/methods/GhostMethodsAndVariables.cpp
new file mode 100644
index 0000000000..8bf939a6e8
--- /dev/null
+++ b/examples/concepts/cpp/methods/GhostMethodsAndVariables.cpp
@@ -0,0 +1,27 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases GhostMethodsAndVariables
+//:: tools silicon
+//:: verdict Pass
+
+/*@ ghost
+	ensures \result == (current && a >= 0);
+	bool isPositive(bool current, int a) {
+		return current && a >= 0;
+	}
+*/
+
+//@ context_everywhere size >= 0;
+//@ context_everywhere \pointer(a, size, read);
+int sum(int a[], int size) {
+	//@ ghost bool positive = true;
+	int result = 0;
+	//@ loop_invariant i >= 0 && i <= size;
+	//@ loop_invariant positive ==> (\forall int j = 0 .. i; a[j] >= 0);
+	//@ loop_invariant (\forall int j = 0 .. i; a[j] >= 0) ==> result >= 0;
+	for(int i = 0; i < size; i++) {
+		//@ ghost positive = isPositive(positive, a[i]);
+		result += a[i];
+	}
+	//@ assert positive ==> result >= 0;
+	return result;
+}
diff --git a/examples/concepts/cpp/methods/GhostParamsAndResults.cpp b/examples/concepts/cpp/methods/GhostParamsAndResults.cpp
new file mode 100644
index 0000000000..b68ef70b7a
--- /dev/null
+++ b/examples/concepts/cpp/methods/GhostParamsAndResults.cpp
@@ -0,0 +1,22 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases GhostParamsAndResults
+//:: tools silicon
+//:: verdict Pass
+	
+/*@
+	given int min;
+	yields bool all_ge_min;
+	requires min >= 0;
+	ensures all_ge_min == (a >= min && b >= min);
+*/
+int add(int a, int b) {
+	//@ ghost all_ge_min = a >= min && b >= min;
+	return a + b;
+}
+
+int caller() {
+	//@ ghost bool items_ge_5;
+	int result = add(10, 12) /*@ given { min = 5 } */ /*@ yields { items_ge_5 = all_ge_min } */ ;
+	//@ assert items_ge_5;
+	return result;
+}
diff --git a/examples/concepts/cpp/methods/InlineFunction.cpp b/examples/concepts/cpp/methods/InlineFunction.cpp
new file mode 100644
index 0000000000..04b5ed9576
--- /dev/null
+++ b/examples/concepts/cpp/methods/InlineFunction.cpp
@@ -0,0 +1,9 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases InlineFunction
+//:: tools silicon
+//:: verdict Pass
+
+//@ inline pure bool isPositive(int a) = (a >= 0);
+
+//@ requires isPositive(number);
+bool incr(int number);
\ No newline at end of file
diff --git a/examples/concepts/cpp/methods/Permissions.cpp b/examples/concepts/cpp/methods/Permissions.cpp
new file mode 100644
index 0000000000..3f06a001bd
--- /dev/null
+++ b/examples/concepts/cpp/methods/Permissions.cpp
@@ -0,0 +1,15 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Permissions
+//:: tools silicon
+//:: verdict Pass
+
+
+int amount = 0;
+
+//@ requires Perm(amount, 1);
+//@ ensures Perm(amount, 1) ** amount == x;
+void set(int x) {
+	amount = x;
+}
+
+
diff --git a/examples/concepts/cpp/methods/Predicates.cpp b/examples/concepts/cpp/methods/Predicates.cpp
new file mode 100644
index 0000000000..b3c65d7d94
--- /dev/null
+++ b/examples/concepts/cpp/methods/Predicates.cpp
@@ -0,0 +1,27 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Predicates
+//:: tools silicon
+//:: verdict Pass
+
+int amount = 0;
+
+//@ resource pre_state() = Perm(amount, write);
+//@ resource state(int value) = Perm(amount, write) ** amount == value;
+
+//@ requires pre_state();
+//@ ensures state(x);
+void set(int x) {
+	// pre_state();
+	//@ unfold pre_state();
+	// Perm(amount, write);
+	amount = x;
+	// Perm(amount, write) ** amount == x;
+	//@ fold state(x);
+	// state(x);
+}
+
+//@ requires pre_state();
+//@ ensures state(50);
+void manageAccount() {
+	set(50);
+}
diff --git a/examples/concepts/cpp/methods/PureGhostMethod.cpp b/examples/concepts/cpp/methods/PureGhostMethod.cpp
new file mode 100644
index 0000000000..55231fd64a
--- /dev/null
+++ b/examples/concepts/cpp/methods/PureGhostMethod.cpp
@@ -0,0 +1,10 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases PureGhostMethod
+//:: tools silicon
+//:: verdict Pass
+
+/*@
+	ensures \result == a >= 0;
+	pure bool isPositive(int a) = a >= 0;
+*/
+
diff --git a/examples/concepts/sycl/MethodResolving.cpp b/examples/concepts/sycl/MethodResolving.cpp
new file mode 100644
index 0000000000..7d50f3c942
--- /dev/null
+++ b/examples/concepts/sycl/MethodResolving.cpp
@@ -0,0 +1,8 @@
+#include <sycl/sycl.hpp>
+
+void test2() {
+	sycl::queue queue;
+	queue.submit(5);
+	queue.submit(33);
+	int x = queue.test2();
+}
\ No newline at end of file
diff --git a/project/antlr.sc b/project/antlr.sc
index 9b0556126a..ab271c26ff 100644
--- a/project/antlr.sc
+++ b/project/antlr.sc
@@ -58,6 +58,15 @@ object c extends GenModule {
   )
 }
 
+object cpp extends GenModule {
+  def lexer = "LangCPPLexer.g4"
+  def parser = "CPPParser.g4"
+  def deps = Seq(
+    "SpecParser.g4", "SpecLexer.g4",
+    "LangCPPParser.g4", "LangCPPLexer.g4"
+  )
+}
+
 object java extends GenModule {
   def lexer = "LangJavaLexer.g4"
   def parser = "JavaParser.g4"
diff --git a/res/universal/res/cpp/stdbool.h b/res/universal/res/cpp/stdbool.h
new file mode 100644
index 0000000000..930ddeb7c6
--- /dev/null
+++ b/res/universal/res/cpp/stdbool.h
@@ -0,0 +1,3 @@
+#define bool	_Bool
+#define true	1
+#define false	0
\ No newline at end of file
diff --git a/res/universal/res/cpp/sycl/sycl.hpp b/res/universal/res/cpp/sycl/sycl.hpp
new file mode 100644
index 0000000000..68365606b3
--- /dev/null
+++ b/res/universal/res/cpp/sycl/sycl.hpp
@@ -0,0 +1,8 @@
+namespace VERCORS {
+	namespace sycl {
+		namespace queue {
+			int VERCORS__submit(int kernel);
+			int VERCORS__test2();
+		}
+	}
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala
index 1c66c94088..65e41d8450 100644
--- a/src/col/vct/col/ast/Node.scala
+++ b/src/col/vct/col/ast/Node.scala
@@ -17,7 +17,6 @@ import vct.col.ast.expr.ambiguous._
 import vct.col.ast.expr.apply._
 import vct.col.ast.expr.binder._
 import vct.col.ast.expr.bip._
-import vct.col.ast.family.coercion._
 import vct.col.ast.expr.context._
 import vct.col.ast.expr.heap.alloc._
 import vct.col.ast.expr.heap.read._
@@ -42,9 +41,12 @@ import vct.col.ast.expr.resource._
 import vct.col.ast.expr.sideeffect._
 import vct.col.ast.family.accountedpredicate._
 import vct.col.ast.family.bipdata._
+import vct.col.ast.family.bipglueelement._
+import vct.col.ast.family.bipporttype._
 import vct.col.ast.family.catchclause._
 import vct.col.ast.family.coercion._
 import vct.col.ast.family.contract._
+import vct.col.ast.family.data._
 import vct.col.ast.family.decreases._
 import vct.col.ast.family.fieldflag._
 import vct.col.ast.family.invoking._
@@ -54,9 +56,6 @@ import vct.col.ast.family.location._
 import vct.col.ast.family.loopcontract._
 import vct.col.ast.family.parregion._
 import vct.col.ast.family.signals._
-import vct.col.ast.family.bipglueelement._
-import vct.col.ast.family.bipporttype._
-import vct.col.ast.family.data._
 import vct.col.ast.lang._
 import vct.col.ast.lang.smt._
 import vct.col.ast.node._
@@ -67,15 +66,10 @@ import vct.col.ast.statement.nonexecutable._
 import vct.col.ast.statement.terminal._
 import vct.col.ast.statement.veymont._
 import vct.col.ast.util.Declarator
-import vct.col.debug._
 import vct.col.origin._
-import vct.col.ref.{DirectRef, Ref}
-import vct.col.resolve._
+import vct.col.ref.Ref
 import vct.col.resolve.ctx._
 import vct.col.resolve.lang.JavaAnnotationData
-import vct.col.resolve.lang.Java
-import vct.col.typerules.{CoercionUtils, Types}
-import vct.result.VerificationError.Unreachable
 
 /** @inheritdoc */ sealed trait Node[G] extends NodeImpl[G]
 
@@ -356,6 +350,7 @@ final case class CoerceNullPointer[G](pointerElementType: Type[G])(implicit val
 final case class CoerceNullEnum[G](targetEnum: Ref[G, Enum[G]])(implicit val o: Origin) extends Coercion[G] with CoerceNullEnumImpl[G]
 
 final case class CoerceCArrayPointer[G](elementType: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceCArrayPointerImpl[G]
+final case class CoerceCPPArrayPointer[G](elementType: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceCPPArrayPointerImpl[G]
 
 final case class CoerceFracZFrac[G]()(implicit val o: Origin) extends Coercion[G] with CoerceFracZFracImpl[G]
 final case class CoerceZFracRat[G]()(implicit val o: Origin) extends Coercion[G] with CoerceZFracRatImpl[G]
@@ -379,6 +374,9 @@ final case class CoerceJavaClassAnyClass[G](sourceClass: Ref[G, JavaClassOrInter
 final case class CoerceCPrimitiveToCol[G](source: Type[G], target: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceCPrimitiveToColImpl[G]
 final case class CoerceColToCPrimitive[G](source: Type[G], target: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceColToCPrimitiveImpl[G]
 
+final case class CoerceCPPPrimitiveToCol[G](source: Type[G], target: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceCPPPrimitiveToColImpl[G]
+final case class CoerceColToCPPPrimitive[G](source: Type[G], target: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceColToCPPPrimitiveImpl[G]
+
 final case class CoerceMapOption[G](inner: Coercion[G], sourceOptionElement: Type[G], targetOptionElement: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceMapOptionImpl[G]
 final case class CoerceMapTuple[G](inner: Seq[Coercion[G]], sourceTypes: Seq[Type[G]], targetTypes: Seq[Type[G]])(implicit val o: Origin) extends Coercion[G] with CoerceMapTupleImpl[G]
 final case class CoerceMapEither[G](inner: (Coercion[G], Coercion[G]), sourceTypes: (Type[G], Type[G]), targetTypes: (Type[G], Type[G]))(implicit val o: Origin) extends Coercion[G] with CoerceMapEitherImpl[G]
@@ -957,6 +955,71 @@ final case class CTPointer[G](innerType: Type[G])(implicit val o: Origin = Diagn
 final case class CTArray[G](size: Option[Expr[G]], innerType: Type[G])(val blame: Blame[ArraySizeError])(implicit val o: Origin = DiagnosticOrigin) extends CType[G] with CTArrayImpl[G]
 final case class CTCudaVec[G]()(implicit val o: Origin = DiagnosticOrigin) extends CType[G] with CTCudaVecImpl[G]
 
+sealed trait CPPDeclarationSpecifier[G] extends NodeFamily[G] with CPPDeclarationSpecifierImpl[G]
+
+sealed trait CPPSpecificationModifier[G] extends CPPDeclarationSpecifier[G] with CPPSpecificationModifierImpl[G]
+final case class CPPPure[G]()(implicit val o: Origin) extends CPPSpecificationModifier[G] with CPPPureImpl[G]
+final case class CPPInline[G]()(implicit val o: Origin) extends CPPSpecificationModifier[G] with CPPInlineImpl[G]
+
+sealed trait CPPTypeSpecifier[G] extends CPPDeclarationSpecifier[G] with CPPTypeSpecifierImpl[G]
+final case class CPPVoid[G]()(implicit val o: Origin) extends CPPTypeSpecifier[G] with CPPVoidImpl[G]
+final case class CPPChar[G]()(implicit val o: Origin) extends CPPTypeSpecifier[G] with CPPCharImpl[G]
+final case class CPPShort[G]()(implicit val o: Origin) extends CPPTypeSpecifier[G] with CPPShortImpl[G]
+final case class CPPInt[G]()(implicit val o: Origin) extends CPPTypeSpecifier[G] with CPPIntImpl[G]
+final case class CPPLong[G]()(implicit val o: Origin) extends CPPTypeSpecifier[G] with CPPLongImpl[G]
+final case class CPPSigned[G]()(implicit val o: Origin) extends CPPTypeSpecifier[G] with CPPSignedImpl[G]
+final case class CPPUnsigned[G]()(implicit val o: Origin) extends CPPTypeSpecifier[G] with CPPUnsignedImpl[G]
+final case class CPPBool[G]()(implicit val o: Origin) extends CPPTypeSpecifier[G] with CPPBoolImpl[G]
+final case class CPPTypedefName[G](var nestedName: String)(implicit val o: Origin) extends CPPTypeSpecifier[G] with CPPTypedefNameImpl[G] {
+  var ref: Option[CPPTypeNameTarget[G]] = None
+}
+final case class SYCLQueue[G]()(implicit val o: Origin) extends CPPTypeSpecifier[G] with SYCLQueueImpl[G]
+final case class TSYCLQueue[G]()(implicit val o: Origin) extends Type[G] with TSYCLQueueImpl[G]
+
+final case class CPPSpecificationType[G](t: Type[G])(implicit val o: Origin) extends CPPTypeSpecifier[G] with CPPSpecificationTypeImpl[G]
+
+final case class CPPPointer[G]()(implicit val o: Origin) extends NodeFamily[G] with CPPPointerImpl[G]
+
+final class CPPParam[G](val specifiers: Seq[CPPDeclarationSpecifier[G]], val declarator: CPPDeclarator[G])(implicit val o: Origin) extends Declaration[G] with CPPParamImpl[G]
+
+sealed trait CPPDeclarator[G] extends NodeFamily[G] with CPPDeclaratorImpl[G]
+final case class CPPPointerDeclarator[G](pointers: Seq[CPPPointer[G]], inner: CPPDeclarator[G])(implicit val o: Origin) extends CPPDeclarator[G] with CPPPointerDeclaratorImpl[G]
+final case class CPPArrayDeclarator[G](inner: CPPDeclarator[G], size: Option[Expr[G]])(val blame: Blame[ArraySizeError])(implicit val o: Origin) extends CPPDeclarator[G] with CPPArrayDeclaratorImpl[G]
+final case class CPPTypedFunctionDeclarator[G](params: Seq[CPPParam[G]], varargs: Boolean, inner: CPPDeclarator[G])(implicit val o: Origin) extends CPPDeclarator[G] with CPPTypedFunctionDeclaratorImpl[G]
+final case class CPPName[G](name: String)(implicit val o: Origin) extends CPPDeclarator[G] with CPPNameImpl[G]
+
+final case class CPPInit[G](decl: CPPDeclarator[G], init: Option[Expr[G]])(implicit val o: Origin) extends NodeFamily[G] with CPPInitImpl[G] {
+  var ref: Option[RefCPPFunctionDefinition[G]] = None
+}
+
+final case class CPPDeclaration[G](val contract: ApplicableContract[G], val specs: Seq[CPPDeclarationSpecifier[G]], val inits: Seq[CPPInit[G]])(implicit val o: Origin) extends NodeFamily[G] with CPPDeclarationImpl[G]
+
+final class CPPTranslationUnit[G](val declarations: Seq[GlobalDeclaration[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with Declarator[G] with CPPTranslationUnitImpl[G]
+
+sealed trait CPPAbstractDeclaration[G] extends GlobalDeclaration[G] with CPPAbstractDeclarationImpl[G]
+
+final class CPPGlobalDeclaration[G](val decl: CPPDeclaration[G])(implicit val o: Origin) extends CPPAbstractDeclaration[G] with CPPGlobalDeclarationImpl[G]
+final class CPPLocalDeclaration[G](val decl: CPPDeclaration[G])(implicit val o: Origin) extends Declaration[G] with CPPLocalDeclarationImpl[G]
+final class CPPFunctionDefinition[G](val contract: ApplicableContract[G], val specs: Seq[CPPDeclarationSpecifier[G]], val declarator: CPPDeclarator[G], val body: Statement[G])(val blame: Blame[CallableFailure])(implicit val o: Origin) extends GlobalDeclaration[G] with CPPFunctionDefinitionImpl[G] {
+  var ref: Option[RefCPPGlobalDeclaration[G]] = None
+}
+final class CPPNamespaceDefinition[G](val name: String, val declarations: Seq[GlobalDeclaration[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with CPPNamespaceDefinitionImpl[G]
+
+sealed trait CPPStatement[G] extends Statement[G] with CPPStatementImpl[G]
+final case class CPPDeclarationStatement[G](decl: CPPLocalDeclaration[G])(implicit val o: Origin) extends CPPStatement[G] with CPPDeclarationStatementImpl[G]
+
+sealed trait CPPExpr[G] extends Expr[G] with CPPExprImpl[G]
+final case class CPPLocal[G](name: String)(val blame: Blame[DerefInsufficientPermission])(implicit val o: Origin) extends CPPExpr[G] with CPPLocalImpl[G] {
+  var ref: Option[CPPNameTarget[G]] = None
+}
+final case class CPPInvocation[G](applicable: Expr[G], args: Seq[Expr[G]], givenArgs: Seq[(Ref[G, Variable[G]], Expr[G])], yields: Seq[(Expr[G], Ref[G, Variable[G]])])(val blame: Blame[FrontendInvocationError])(implicit val o: Origin) extends CPPExpr[G] with CPPInvocationImpl[G] {
+  var ref: Option[CPPInvocationTarget[G]] = None
+}
+
+sealed trait CPPType[G] extends Type[G] with CPPTypeImpl[G]
+final case class CPPPrimitiveType[G](specifiers: Seq[CPPDeclarationSpecifier[G]])(implicit val o: Origin = DiagnosticOrigin) extends CPPType[G] with CPPPrimitiveTypeImpl[G]
+final case class CPPTArray[G](size: Option[Expr[G]], innerType: Type[G])(val blame: Blame[ArraySizeError])(implicit val o: Origin = DiagnosticOrigin) extends CPPType[G] with CPPTArrayImpl[G]
+
 final case class JavaName[G](names: Seq[String])(implicit val o: Origin) extends NodeFamily[G] with JavaNameImpl[G] {
   var ref: Option[JavaTypeNameTarget[G]] = None
 }
diff --git a/src/col/vct/col/ast/declaration/global/HeapVariableImpl.scala b/src/col/vct/col/ast/declaration/global/HeapVariableImpl.scala
index f0170e5b7a..d203665195 100644
--- a/src/col/vct/col/ast/declaration/global/HeapVariableImpl.scala
+++ b/src/col/vct/col/ast/declaration/global/HeapVariableImpl.scala
@@ -5,7 +5,7 @@ import vct.col.print._
 
 trait HeapVariableImpl[G] { this: HeapVariable[G] =>
   override def layout(implicit ctx: Ctx): Doc = ctx.syntax match {
-    case Ctx.C | Ctx.Cuda | Ctx.OpenCL =>
+    case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP =>
       val (spec, decl) = t.layoutSplitDeclarator
       spec <+> decl <> ctx.name(this) <> ";"
     case _ =>
diff --git a/src/col/vct/col/ast/declaration/global/ProcedureImpl.scala b/src/col/vct/col/ast/declaration/global/ProcedureImpl.scala
index 4e45e31aeb..f6cc4e3f51 100644
--- a/src/col/vct/col/ast/declaration/global/ProcedureImpl.scala
+++ b/src/col/vct/col/ast/declaration/global/ProcedureImpl.scala
@@ -35,7 +35,7 @@ trait ProcedureImpl[G] { this: Procedure[G] =>
 
   override def layout(implicit ctx: Ctx): Doc = ctx.syntax match {
     case Ctx.Silver => layoutSilver
-    case Ctx.C | Ctx.Cuda | Ctx.OpenCL => layoutC
+    case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP => layoutC
     case Ctx.PVL | Ctx.Java => Doc.spec(Show.lazily(layoutSpec(_)))
   }
 }
\ No newline at end of file
diff --git a/src/col/vct/col/ast/declaration/singular/VariableImpl.scala b/src/col/vct/col/ast/declaration/singular/VariableImpl.scala
index a4b634273b..78f8c2d855 100644
--- a/src/col/vct/col/ast/declaration/singular/VariableImpl.scala
+++ b/src/col/vct/col/ast/declaration/singular/VariableImpl.scala
@@ -5,7 +5,7 @@ import vct.col.print._
 
 trait VariableImpl[G] { this: Variable[G] =>
   override def layout(implicit ctx: Ctx): Doc = ctx.syntax match {
-    case Ctx.C | Ctx.Cuda | Ctx.OpenCL =>
+    case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP =>
       val (spec, decl) = t.layoutSplitDeclarator
       spec <+> decl <> ctx.name(this)
     case Ctx.PVL | Ctx.Java => t.show <+> ctx.name(this)
diff --git a/src/col/vct/col/ast/expr/ambiguous/AmbiguousSubscriptImpl.scala b/src/col/vct/col/ast/expr/ambiguous/AmbiguousSubscriptImpl.scala
index f61023d4eb..92e0362557 100644
--- a/src/col/vct/col/ast/expr/ambiguous/AmbiguousSubscriptImpl.scala
+++ b/src/col/vct/col/ast/expr/ambiguous/AmbiguousSubscriptImpl.scala
@@ -9,6 +9,7 @@ trait AmbiguousSubscriptImpl[G] { this: AmbiguousSubscript[G] =>
   def isSeqOp: Boolean = CoercionUtils.getAnySeqCoercion(collection.t).isDefined
   def isArrayOp: Boolean = CoercionUtils.getAnyArrayCoercion(collection.t).isDefined
   def isCArrayOp: Boolean = CoercionUtils.getAnyCArrayCoercion(collection.t).isDefined
+  def isCPPArrayOp: Boolean = CoercionUtils.getAnyCPPArrayCoercion(collection.t).isDefined
   def isPointerOp: Boolean = CoercionUtils.getAnyPointerCoercion(collection.t).isDefined
   def isMapOp: Boolean = CoercionUtils.getAnyMapCoercion(collection.t).isDefined
 
@@ -16,6 +17,7 @@ trait AmbiguousSubscriptImpl[G] { this: AmbiguousSubscript[G] =>
     if (isSeqOp) collection.t.asSeq.get.element
     else if (isArrayOp) collection.t.asArray.get.element
     else if (isCArrayOp) collection.t.asCArray.get.innerType
+    else if (isCPPArrayOp) collection.t.asCPPArray.get.innerType
     else if (isPointerOp) collection.t.asPointer.get.element
     else if (isMapOp) collection.t.asMap.get.value
     else throw Unreachable(s"Trying to subscript ($this) a non subscriptable variable with type ${collection.t}")
diff --git a/src/col/vct/col/ast/expr/context/AmbiguousResultImpl.scala b/src/col/vct/col/ast/expr/context/AmbiguousResultImpl.scala
index e6d8994a14..8f3467d1e2 100644
--- a/src/col/vct/col/ast/expr/context/AmbiguousResultImpl.scala
+++ b/src/col/vct/col/ast/expr/context/AmbiguousResultImpl.scala
@@ -6,7 +6,7 @@ import vct.col.check.{CheckContext, CheckError, ResultOutsidePostcondition}
 import vct.col.err
 import vct.col.print._
 import vct.col.resolve.ctx._
-import vct.col.resolve.lang.C
+import vct.col.resolve.lang.{C, CPP}
 
 trait AmbiguousResultImpl[G] extends NodeFamilyImpl[G] { this: AmbiguousResult[G] =>
   override lazy val t: Type[G] = ref.getOrElse(
@@ -15,6 +15,10 @@ trait AmbiguousResultImpl[G] extends NodeFamilyImpl[G] { this: AmbiguousResult[G
       C.typeOrReturnTypeFromDeclaration(decl.specs, decl.declarator)
     case RefCGlobalDeclaration(decls, initIdx) =>
       C.typeOrReturnTypeFromDeclaration(decls.decl.specs, decls.decl.inits(initIdx).decl)
+    case RefCPPFunctionDefinition(decl) =>
+      CPP.typeOrReturnTypeFromDeclaration(decl.specs, decl.declarator)
+    case RefCPPGlobalDeclaration(decls, initIdx) =>
+      CPP.typeOrReturnTypeFromDeclaration(decls.decl.specs, decls.decl.inits(initIdx).decl)
     case RefFunction(decl) => decl.returnType
     case RefProcedure(decl) => decl.returnType
     case RefJavaMethod(decl) => decl.returnType
diff --git a/src/col/vct/col/ast/family/coercion/CoerceCPPArrayPointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceCPPArrayPointerImpl.scala
new file mode 100644
index 0000000000..f424079e17
--- /dev/null
+++ b/src/col/vct/col/ast/family/coercion/CoerceCPPArrayPointerImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceCPPArrayPointer, TPointer}
+
+trait CoerceCPPArrayPointerImpl[G] { this: CoerceCPPArrayPointer[G] =>
+  override def target: TPointer[G] = TPointer(elementType)
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/family/coercion/CoerceCPPPrimitiveToColImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceCPPPrimitiveToColImpl.scala
new file mode 100644
index 0000000000..69a4f1ecf9
--- /dev/null
+++ b/src/col/vct/col/ast/family/coercion/CoerceCPPPrimitiveToColImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.CoerceCPPPrimitiveToCol
+
+trait CoerceCPPPrimitiveToColImpl[G] { this: CoerceCPPPrimitiveToCol[G] =>
+    
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/family/coercion/CoerceColToCPPPrimitiveImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceColToCPPPrimitiveImpl.scala
new file mode 100644
index 0000000000..263a5fb505
--- /dev/null
+++ b/src/col/vct/col/ast/family/coercion/CoerceColToCPPPrimitiveImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.CoerceColToCPPPrimitive
+
+trait CoerceColToCPPPrimitiveImpl[G] { this: CoerceColToCPPPrimitive[G] =>
+    
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala
index c811820f2c..a12fa7ec67 100644
--- a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala
+++ b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala
@@ -1,6 +1,6 @@
 package vct.col.ast.family.coercion
 
-import vct.col.ast.{CoerceBoolResource, CoerceBoundIntFrac, CoerceBoundIntZFrac, CoerceCPrimitiveToCol, CoerceClassAnyClass, CoerceColToCPrimitive, CoerceFloatRat, CoerceFracZFrac, CoerceIdentity, CoerceIncreasePrecision, CoerceIntRat, CoerceJavaClassAnyClass, CoerceJavaSupports, CoerceJoinUnion, CoerceMapBag, CoerceMapEither, CoerceMapMap, CoerceMapMatrix, CoerceMapOption, CoerceMapSeq, CoerceMapSet, CoerceMapTuple, CoerceMapType, CoerceNothingSomething, CoerceNullAnyClass, CoerceNullArray, CoerceNullClass, CoerceNullJavaClass, CoerceNullPointer, CoerceNullRef, CoerceRatZFrac, CoerceSelectUnion, CoerceSomethingAny, CoerceSupports, CoerceUnboundInt, CoerceWidenBound, CoerceZFracFrac, CoerceZFracRat, Coercion, CoercionSequence, Type}
+import vct.col.ast.{CoerceBoolResource, CoerceBoundIntFrac, CoerceBoundIntZFrac, CoerceCPrimitiveToCol, CoerceCPPPrimitiveToCol, CoerceClassAnyClass, CoerceColToCPrimitive, CoerceColToCPPPrimitive, CoerceFloatRat, CoerceFracZFrac, CoerceIdentity, CoerceIncreasePrecision, CoerceIntRat, CoerceJavaClassAnyClass, CoerceJavaSupports, CoerceJoinUnion, CoerceMapBag, CoerceMapEither, CoerceMapMap, CoerceMapMatrix, CoerceMapOption, CoerceMapSeq, CoerceMapSet, CoerceMapTuple, CoerceMapType, CoerceNothingSomething, CoerceNullAnyClass, CoerceNullArray, CoerceNullClass, CoerceNullJavaClass, CoerceNullPointer, CoerceNullRef, CoerceRatZFrac, CoerceSelectUnion, CoerceSomethingAny, CoerceSupports, CoerceUnboundInt, CoerceWidenBound, CoerceZFracFrac, CoerceZFracRat, Coercion, CoercionSequence, Type}
 
 trait CoercionImpl[G] { this: Coercion[G] =>
   def target: Type[G]
@@ -34,6 +34,8 @@ trait CoercionImpl[G] { this: Coercion[G] =>
     case CoerceJavaClassAnyClass(_) => true
     case CoerceCPrimitiveToCol(_, _) => true
     case CoerceColToCPrimitive(_, _) => true
+    case CoerceCPPPrimitiveToCol(_, _) => true
+    case CoerceColToCPPPrimitive(_, _) => true
     case CoerceMapOption(inner, _, _) => inner.isPromoting
     case CoerceMapTuple(inner, _, _) => inner.forall(_.isPromoting)
     case CoerceMapEither(inner, _, _) => inner._1.isPromoting && inner._2.isPromoting
diff --git a/src/col/vct/col/ast/lang/CPPAbstractDeclarationImpl.scala b/src/col/vct/col/ast/lang/CPPAbstractDeclarationImpl.scala
new file mode 100644
index 0000000000..0998d2988d
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPAbstractDeclarationImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPAbstractDeclaration
+
+trait CPPAbstractDeclarationImpl[G] { this: CPPAbstractDeclaration[G] =>
+
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPArrayDeclaratorImpl.scala b/src/col/vct/col/ast/lang/CPPArrayDeclaratorImpl.scala
new file mode 100644
index 0000000000..4fcad5e33b
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPArrayDeclaratorImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPArrayDeclarator
+import vct.col.print.{Ctx, Doc, Group}
+
+trait CPPArrayDeclaratorImpl[G] { this: CPPArrayDeclarator[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Group(inner.show <> "[" <> Doc.arg(Doc.stack(size.toSeq)) <> "]")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPBoolImpl.scala b/src/col/vct/col/ast/lang/CPPBoolImpl.scala
new file mode 100644
index 0000000000..4ee8f9efb6
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPBoolImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPBool
+import vct.col.print.{Ctx, Doc, Text}
+
+trait CPPBoolImpl[G] { this: CPPBool[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text("_Bool")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPCharImpl.scala b/src/col/vct/col/ast/lang/CPPCharImpl.scala
new file mode 100644
index 0000000000..acc57512be
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPCharImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPChar
+import vct.col.print.{Ctx, Doc, Text}
+
+trait CPPCharImpl[G] { this: CPPChar[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text("char")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPDeclarationImpl.scala b/src/col/vct/col/ast/lang/CPPDeclarationImpl.scala
new file mode 100644
index 0000000000..f901e91714
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPDeclarationImpl.scala
@@ -0,0 +1,26 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPDeclaration
+import vct.col.print._
+
+trait CPPDeclarationImpl[G] { this: CPPDeclaration[G] =>
+  // PB: Please keep in sync with ApplicableContractImpl
+  def layoutContract(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      Doc.stack(contract.givenArgs.map(Text("given") <+> _.show <> ";")),
+      Doc.stack(contract.yieldsArgs.map(Text("yields") <+> _.show <> ";")),
+      DocUtil.clauses("context_everywhere", contract.contextEverywhere),
+      DocUtil.clauses("requires", contract.requires),
+      Doc.stack(contract.decreases.toSeq),
+      DocUtil.clauses("ensures", contract.ensures),
+      Doc.stack(contract.signals),
+    ))
+
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      layoutContract,
+      Group(
+        Doc.spread(specs) <>> Doc.args(inits)
+      ),
+    ))
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPDeclarationSpecifierImpl.scala b/src/col/vct/col/ast/lang/CPPDeclarationSpecifierImpl.scala
new file mode 100644
index 0000000000..938805162d
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPDeclarationSpecifierImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPDeclarationSpecifier
+
+trait CPPDeclarationSpecifierImpl[G] { this: CPPDeclarationSpecifier[G] =>
+
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPDeclarationStatementImpl.scala b/src/col/vct/col/ast/lang/CPPDeclarationStatementImpl.scala
new file mode 100644
index 0000000000..a22698c559
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPDeclarationStatementImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPDeclarationStatement
+import vct.col.print.{Ctx, Doc}
+
+trait CPPDeclarationStatementImpl[G] { this: CPPDeclarationStatement[G] =>
+  override def layout(implicit ctx: Ctx): Doc = decl.show <> ";"
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPDeclaratorImpl.scala b/src/col/vct/col/ast/lang/CPPDeclaratorImpl.scala
new file mode 100644
index 0000000000..0bbabca1d4
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPDeclaratorImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPDeclarator
+
+trait CPPDeclaratorImpl[G] { this: CPPDeclarator[G] =>
+
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPExprImpl.scala b/src/col/vct/col/ast/lang/CPPExprImpl.scala
new file mode 100644
index 0000000000..de4c24348b
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPExprImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPExpr
+
+trait CPPExprImpl[G] { this: CPPExpr[G] =>
+
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPFunctionDefinitionImpl.scala b/src/col/vct/col/ast/lang/CPPFunctionDefinitionImpl.scala
new file mode 100644
index 0000000000..645cc52967
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPFunctionDefinitionImpl.scala
@@ -0,0 +1,14 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPFunctionDefinition
+import vct.col.print.{Ctx, Doc, Group}
+
+trait CPPFunctionDefinitionImpl[G] { this: CPPFunctionDefinition[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      contract,
+      Group(
+        Doc.spread(specs) <>> declarator
+      ) <+> body.layoutAsBlock,
+    ))
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPGlobalDeclarationImpl.scala b/src/col/vct/col/ast/lang/CPPGlobalDeclarationImpl.scala
new file mode 100644
index 0000000000..c178df89fa
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPGlobalDeclarationImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPGlobalDeclaration
+import vct.col.print._
+
+trait CPPGlobalDeclarationImpl[G] { this: CPPGlobalDeclaration[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    decl.show <> ";"
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPInitImpl.scala b/src/col/vct/col/ast/lang/CPPInitImpl.scala
new file mode 100644
index 0000000000..901bc2e3b6
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPInitImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPInit
+import vct.col.print.{Ctx, Doc, Group}
+
+trait CPPInitImpl[G] { this: CPPInit[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    if(init.isEmpty) decl.show else Group(decl.show <+> "=" <>> init.get)
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPInlineImpl.scala b/src/col/vct/col/ast/lang/CPPInlineImpl.scala
new file mode 100644
index 0000000000..5894e5bed8
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPInlineImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPInline
+import vct.col.print.{Ctx, Doc, Text}
+
+trait CPPInlineImpl[G] { this: CPPInline[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text("inline")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPIntImpl.scala b/src/col/vct/col/ast/lang/CPPIntImpl.scala
new file mode 100644
index 0000000000..5a72d5ae25
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPIntImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPInt
+import vct.col.print.{Ctx, Doc, Text}
+
+trait CPPIntImpl[G] { this: CPPInt[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text("int")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPInvocationImpl.scala b/src/col/vct/col/ast/lang/CPPInvocationImpl.scala
new file mode 100644
index 0000000000..28938ba191
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPInvocationImpl.scala
@@ -0,0 +1,31 @@
+package vct.col.ast.lang
+
+import vct.col.ast.{CPPInvocation, Type}
+import vct.col.print._
+import vct.col.resolve.ctx._
+import vct.col.resolve.lang.CPP
+import vct.result.VerificationError.Unreachable
+
+trait CPPInvocationImpl[G] { this: CPPInvocation[G] =>
+  override lazy val t: Type[G] = ref.get match {
+    case RefFunction(decl) =>  decl.returnType
+    case RefProcedure(decl) => decl.returnType
+    case RefPredicate(decl) => decl.returnType
+    case RefADTFunction(decl) => decl.returnType
+    case RefModelProcess(decl) => decl.returnType
+    case RefModelAction(decl) => decl.returnType
+    case RefCPPFunctionDefinition(decl) => CPP.typeOrReturnTypeFromDeclaration(decl.specs, decl.declarator)
+    case RefCPPGlobalDeclaration(decls, initIdx) => CPP.typeOrReturnTypeFromDeclaration(decls.decl.specs, decls.decl.inits(initIdx).decl)
+    case RefInstanceMethod(decl) => decl.returnType
+    case RefInstanceFunction(decl) => decl.returnType
+    case RefInstancePredicate(decl) => decl.returnType
+    case BuiltinInstanceMethod(f) => applicable match {
+      case _ => throw Unreachable("BuiltinInstanceMethod resolution of CPPInvocation cannot invoke anything.")
+    }
+  }
+
+  override def precedence: Int = Precedence.POSTFIX
+
+  override def layout(implicit ctx: Ctx): Doc =
+    Group(assoc(applicable) <> "(" <> Doc.args(args) <> ")" <> DocUtil.givenYields(givenArgs, yields))
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPLocalDeclarationImpl.scala b/src/col/vct/col/ast/lang/CPPLocalDeclarationImpl.scala
new file mode 100644
index 0000000000..66a52cbf5f
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPLocalDeclarationImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPLocalDeclaration
+import vct.col.print.{Ctx, Doc}
+
+trait CPPLocalDeclarationImpl[G] { this: CPPLocalDeclaration[G] =>
+  override def layout(implicit ctx: Ctx): Doc = decl.show
+}
diff --git a/src/col/vct/col/ast/lang/CPPLocalImpl.scala b/src/col/vct/col/ast/lang/CPPLocalImpl.scala
new file mode 100644
index 0000000000..5246f352dd
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPLocalImpl.scala
@@ -0,0 +1,32 @@
+package vct.col.ast.lang
+
+import vct.col.ast.{CPPLocal, CPPPrimitiveType, Type}
+import vct.col.print.{Ctx, Doc, Text}
+import vct.col.resolve.ctx._
+import vct.col.resolve.lang.CPP
+import vct.col.typerules.Types
+
+trait CPPLocalImpl[G] { this: CPPLocal[G] =>
+  override lazy val t: Type[G] = ref.get match {
+    case ref: RefCPPParam[G] => CPP.typeOrReturnTypeFromDeclaration(ref.decl.specifiers, ref.decl.declarator)
+    case ref: RefAxiomaticDataType[G] => Types.notAValue(ref)
+    case RefVariable(decl) => decl.t
+    case ref: RefCPPFunctionDefinition[G] => Types.notAValue(ref)
+    case ref @ RefCPPGlobalDeclaration(decls, initIdx) =>
+      val declInfo = CPP.getDeclaratorInfo(decls.decl.inits(initIdx).decl)
+      declInfo.params match {
+        case Some(_) => Types.notAValue(ref) // Function declaration
+        case None => declInfo.typeOrReturnType(CPPPrimitiveType(decls.decl.specs)) // Static declaration
+      }
+    case ref @ RefCPPLocalDeclaration(decls, initIdx) =>
+      val declInfo = CPP.getDeclaratorInfo(decls.decl.inits(initIdx).decl)
+      declInfo.params match {
+        case Some(_) => Types.notAValue(ref) // Function declaration
+        case None => declInfo.typeOrReturnType(CPPPrimitiveType(decls.decl.specs)) // Static declaration
+      }
+    case RefModelField(field) => field.t
+    case target: SpecInvocationTarget[G] => Types.notAValue(target)
+  }
+
+  override def layout(implicit ctx: Ctx): Doc = Text(name)
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPLongImpl.scala b/src/col/vct/col/ast/lang/CPPLongImpl.scala
new file mode 100644
index 0000000000..205b138cd5
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPLongImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPLong
+import vct.col.print.{Ctx, Doc, Text}
+
+trait CPPLongImpl[G] { this: CPPLong[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text("long")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPNameImpl.scala b/src/col/vct/col/ast/lang/CPPNameImpl.scala
new file mode 100644
index 0000000000..e8377813d0
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPNameImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPName
+import vct.col.print.{Ctx, Doc, Text}
+
+trait CPPNameImpl[G] { this: CPPName[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text(name)
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPNamespaceDefinitionImpl.scala b/src/col/vct/col/ast/lang/CPPNamespaceDefinitionImpl.scala
new file mode 100644
index 0000000000..afb2ebf8df
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPNamespaceDefinitionImpl.scala
@@ -0,0 +1,13 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPNamespaceDefinition
+import vct.col.print._
+
+trait CPPNamespaceDefinitionImpl[G] { this: CPPNamespaceDefinition[G] =>
+
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      Text("namespace") <+> Text(name) <+>
+      "{" <>> Doc.stack(declarations) <+/> "}"
+    ))
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPParamImpl.scala b/src/col/vct/col/ast/lang/CPPParamImpl.scala
new file mode 100644
index 0000000000..aefeaadb3a
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPParamImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPParam
+import vct.col.print.{Ctx, Doc}
+
+trait CPPParamImpl[G] { this: CPPParam[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.spread(specifiers) <+> declarator
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPPointerDeclaratorImpl.scala b/src/col/vct/col/ast/lang/CPPPointerDeclaratorImpl.scala
new file mode 100644
index 0000000000..67e08082b5
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPPointerDeclaratorImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPPointerDeclarator
+import vct.col.print.{Ctx, Doc}
+
+trait CPPPointerDeclaratorImpl[G] { this: CPPPointerDeclarator[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    inner.show <> Doc.fold(pointers)(_ <> _)
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPPointerImpl.scala b/src/col/vct/col/ast/lang/CPPPointerImpl.scala
new file mode 100644
index 0000000000..88edbb44ca
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPPointerImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPPointer
+import vct.col.print.{Ctx, Doc, Text}
+
+trait CPPPointerImpl[G] { this: CPPPointer[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text("*")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPPrimitiveTypeImpl.scala b/src/col/vct/col/ast/lang/CPPPrimitiveTypeImpl.scala
new file mode 100644
index 0000000000..320e841cc9
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPPrimitiveTypeImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPPrimitiveType
+import vct.col.print.{Ctx, Doc}
+
+trait CPPPrimitiveTypeImpl[G] { this: CPPPrimitiveType[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Doc.spread(specifiers)
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPPureImpl.scala b/src/col/vct/col/ast/lang/CPPPureImpl.scala
new file mode 100644
index 0000000000..30cbeb5353
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPPureImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPPure
+import vct.col.print.{Ctx, Doc, Text}
+
+trait CPPPureImpl[G] { this: CPPPure[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Doc.inlineSpec(Text("pure"))
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPShortImpl.scala b/src/col/vct/col/ast/lang/CPPShortImpl.scala
new file mode 100644
index 0000000000..6bc77908c4
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPShortImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPShort
+import vct.col.print.{Ctx, Doc, Text}
+
+trait CPPShortImpl[G] { this: CPPShort[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text("short")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPSignedImpl.scala b/src/col/vct/col/ast/lang/CPPSignedImpl.scala
new file mode 100644
index 0000000000..b4502c7236
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPSignedImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPSigned
+import vct.col.print.{Ctx, Doc, Text}
+
+trait CPPSignedImpl[G] { this: CPPSigned[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text("signed")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPSpecificationModifierImpl.scala b/src/col/vct/col/ast/lang/CPPSpecificationModifierImpl.scala
new file mode 100644
index 0000000000..b569102e66
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPSpecificationModifierImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPSpecificationModifier
+
+trait CPPSpecificationModifierImpl[G] { this: CPPSpecificationModifier[G] =>
+
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPSpecificationTypeImpl.scala b/src/col/vct/col/ast/lang/CPPSpecificationTypeImpl.scala
new file mode 100644
index 0000000000..3568a0c777
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPSpecificationTypeImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPSpecificationType
+import vct.col.print.{Ctx, Doc}
+
+trait CPPSpecificationTypeImpl[G] { this: CPPSpecificationType[G] =>
+  override def layout(implicit ctx: Ctx): Doc = t.show
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPStatementImpl.scala b/src/col/vct/col/ast/lang/CPPStatementImpl.scala
new file mode 100644
index 0000000000..38840a879f
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPStatementImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPStatement
+
+trait CPPStatementImpl[G] { this: CPPStatement[G] =>
+
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPTArrayImpl.scala b/src/col/vct/col/ast/lang/CPPTArrayImpl.scala
new file mode 100644
index 0000000000..e6a78feafe
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPTArrayImpl.scala
@@ -0,0 +1,10 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPTArray
+import vct.col.print.{Ctx, Doc, Group}
+
+trait CPPTArrayImpl[G] { this: CPPTArray[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Group(innerType.show <> "[" <> Doc.args(size.toSeq) <> "]")
+}
+
diff --git a/src/col/vct/col/ast/lang/CPPTranslationUnitImpl.scala b/src/col/vct/col/ast/lang/CPPTranslationUnitImpl.scala
new file mode 100644
index 0000000000..e60e344d6a
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPTranslationUnitImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPTranslationUnit
+import vct.col.print.{Ctx, Doc}
+
+trait CPPTranslationUnitImpl[G] { this: CPPTranslationUnit[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Doc.stack(declarations)
+}
diff --git a/src/col/vct/col/ast/lang/CPPTypeImpl.scala b/src/col/vct/col/ast/lang/CPPTypeImpl.scala
new file mode 100644
index 0000000000..17e6176125
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPTypeImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPType
+
+trait CPPTypeImpl[G] { this: CPPType[G] =>
+
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPTypeSpecifierImpl.scala b/src/col/vct/col/ast/lang/CPPTypeSpecifierImpl.scala
new file mode 100644
index 0000000000..7d747b3063
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPTypeSpecifierImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPTypeSpecifier
+
+trait CPPTypeSpecifierImpl[G] { this: CPPTypeSpecifier[G] =>
+
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPTypedFunctionDeclaratorImpl.scala b/src/col/vct/col/ast/lang/CPPTypedFunctionDeclaratorImpl.scala
new file mode 100644
index 0000000000..de89578f31
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPTypedFunctionDeclaratorImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPTypedFunctionDeclarator
+import vct.col.print.{Ctx, Doc, Group, Text}
+
+trait CPPTypedFunctionDeclaratorImpl[G] { this: CPPTypedFunctionDeclarator[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Group(inner.show <> "(" <> Doc.args(params ++ (if(varargs) Seq(Text("...")) else Nil)) <> ")")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPTypedefNameImpl.scala b/src/col/vct/col/ast/lang/CPPTypedefNameImpl.scala
new file mode 100644
index 0000000000..d800538716
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPTypedefNameImpl.scala
@@ -0,0 +1,13 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPTypedefName
+import vct.col.print.{Ctx, Doc, Text}
+
+trait CPPTypedefNameImpl[G] { this: CPPTypedefName[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text(nestedName)
+
+  def appendName(postfix: String): CPPTypedefName[G] = {
+    nestedName ++= postfix
+    this
+  }
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPUnsignedImpl.scala b/src/col/vct/col/ast/lang/CPPUnsignedImpl.scala
new file mode 100644
index 0000000000..1f5073907f
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPUnsignedImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPUnsigned
+import vct.col.print.{Ctx, Doc, Text}
+
+trait CPPUnsignedImpl[G] { this: CPPUnsigned[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text("unsigned")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/CPPVoidImpl.scala b/src/col/vct/col/ast/lang/CPPVoidImpl.scala
new file mode 100644
index 0000000000..ca1dfe05ea
--- /dev/null
+++ b/src/col/vct/col/ast/lang/CPPVoidImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.CPPVoid
+import vct.col.print.{Ctx, Doc, Text}
+
+trait CPPVoidImpl[G] { this: CPPVoid[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text("void")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/SYCLQueueImpl.scala b/src/col/vct/col/ast/lang/SYCLQueueImpl.scala
new file mode 100644
index 0000000000..edd7f3044a
--- /dev/null
+++ b/src/col/vct/col/ast/lang/SYCLQueueImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.lang
+
+import vct.col.ast.SYCLQueue
+import vct.col.print.{Ctx, Doc, Text}
+
+trait SYCLQueueImpl[G] { this: SYCLQueue[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text("sycl::queue")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/statement/terminal/LabelImpl.scala b/src/col/vct/col/ast/statement/terminal/LabelImpl.scala
index 2450239e19..2bb7699518 100644
--- a/src/col/vct/col/ast/statement/terminal/LabelImpl.scala
+++ b/src/col/vct/col/ast/statement/terminal/LabelImpl.scala
@@ -8,14 +8,14 @@ trait LabelImpl[G] { this: Label[G] =>
     case Ctx.PVL => Seq(layoutLabel) ++ stat.blockElementsForLayout
     case Ctx.Silver => Seq(layoutLabel) ++ stat.blockElementsForLayout
     case Ctx.Java => Seq(this)
-    case Ctx.C | Ctx.Cuda | Ctx.OpenCL => Seq(layoutLabel) ++ stat.blockElementsForLayout
+    case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP => Seq(layoutLabel) ++ stat.blockElementsForLayout
   }
 
   def layoutLabel(implicit ctx: Ctx): Doc = ctx.syntax match {
     case Ctx.PVL => Text("label") <+> ctx.name(decl) <> ";"
     case Ctx.Silver => Text("label") <+> ctx.name(decl)
     case Ctx.Java => Text(ctx.name(decl)) <> ":"
-    case Ctx.C | Ctx.Cuda | Ctx.OpenCL => Text(ctx.name(decl)) <> ":"
+    case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP => Text(ctx.name(decl)) <> ":"
   }
 
   override def layout(implicit ctx: Ctx): Doc =
diff --git a/src/col/vct/col/ast/type/TBoolImpl.scala b/src/col/vct/col/ast/type/TBoolImpl.scala
index 38b24f8a1d..3b44c268a2 100644
--- a/src/col/vct/col/ast/type/TBoolImpl.scala
+++ b/src/col/vct/col/ast/type/TBoolImpl.scala
@@ -1,13 +1,13 @@
 package vct.col.ast.`type`
 
 import vct.col.ast.TBool
-import vct.col.print.{Ctx, Doc, Group, Text}
+import vct.col.print.{Ctx, Doc, Text}
 
 trait TBoolImpl[G] { this: TBool[G] =>
   override def layout(implicit ctx: Ctx): Doc = ctx.syntax match {
     case Ctx.PVL => Text("boolean")
     case Ctx.Silver => Text("Bool")
     case Ctx.Java => Text("boolean")
-    case Ctx.C | Ctx.Cuda | Ctx.OpenCL => Text("bool")
+    case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP => Text("bool")
   }
 }
\ No newline at end of file
diff --git a/src/col/vct/col/ast/type/TSYCLQueueImpl.scala b/src/col/vct/col/ast/type/TSYCLQueueImpl.scala
new file mode 100644
index 0000000000..db3a3467c6
--- /dev/null
+++ b/src/col/vct/col/ast/type/TSYCLQueueImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.`type`
+
+import vct.col.ast.TSYCLQueue
+import vct.col.print.{Ctx, Doc, Text}
+
+trait TSYCLQueueImpl[G] { this: TSYCLQueue[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text("sycl::queue")
+}
\ No newline at end of file
diff --git a/src/col/vct/col/ast/type/typeclass/TypeImpl.scala b/src/col/vct/col/ast/type/typeclass/TypeImpl.scala
index e5f01d072b..1dbf62a12f 100644
--- a/src/col/vct/col/ast/type/typeclass/TypeImpl.scala
+++ b/src/col/vct/col/ast/type/typeclass/TypeImpl.scala
@@ -19,6 +19,7 @@ trait TypeImpl[G] { this: Type[G] =>
   def asPointer: Option[TPointer[G]] = CoercionUtils.getAnyPointerCoercion(this).map(_._2)
   def asArray: Option[TArray[G]] = CoercionUtils.getAnyArrayCoercion(this).map(_._2)
   def asCArray: Option[CTArray[G]] = CoercionUtils.getAnyCArrayCoercion(this).map(_._2)
+  def asCPPArray: Option[CPPTArray[G]] = CoercionUtils.getAnyCPPArrayCoercion(this).map(_._2)
   def asOption: Option[TOption[G]] = CoercionUtils.getAnyOptionCoercion(this).map(_._2)
   def asMap: Option[TMap[G]] = CoercionUtils.getAnyMapCoercion(this).map(_._2)
   def asTuple: Option[TTuple[G]] = CoercionUtils.getAnyTupleCoercion(this).map(_._2)
diff --git a/src/col/vct/col/ast/util/CheckFoldUnfoldTarget.scala b/src/col/vct/col/ast/util/CheckFoldUnfoldTarget.scala
index 8ab7faa0a0..f3801b1afb 100644
--- a/src/col/vct/col/ast/util/CheckFoldUnfoldTarget.scala
+++ b/src/col/vct/col/ast/util/CheckFoldUnfoldTarget.scala
@@ -36,6 +36,11 @@ trait CheckFoldUnfoldTarget[G] extends NodeFamilyImpl[G] { this: NodeFamily[G] =
       case RefInstancePredicate(decl) => checkNonAbstract(decl, inv)
       case _ => Some(NotAPredicateApplication(e))
     }
+    case inv: CPPInvocation[G] => inv.ref.get match {
+      case RefPredicate(decl) => checkNonAbstract(decl, inv)
+      case RefInstancePredicate(decl) => checkNonAbstract(decl, inv)
+      case _ => Some(NotAPredicateApplication(e))
+    }
     case _ => Some(NotAPredicateApplication(e))
   }
 
diff --git a/src/col/vct/col/feature/Feature.scala b/src/col/vct/col/feature/Feature.scala
index 67cdb4c457..1f9e34ff0e 100644
--- a/src/col/vct/col/feature/Feature.scala
+++ b/src/col/vct/col/feature/Feature.scala
@@ -78,6 +78,7 @@ case object AxiomaticDataTypes extends Feature
 case object SmtOperators extends Feature
 case object JavaSpecific extends Feature
 case object CSpecific extends Feature
+case object CPPSpecific extends Feature
 case object PvlSpecific extends Feature
 case object SilverSpecific extends Feature
 case object Contracts extends Feature
diff --git a/src/col/vct/col/feature/FeatureRainbow.scala b/src/col/vct/col/feature/FeatureRainbow.scala
index 11c6947792..44326fc9cf 100644
--- a/src/col/vct/col/feature/FeatureRainbow.scala
+++ b/src/col/vct/col/feature/FeatureRainbow.scala
@@ -112,6 +112,8 @@ class FeatureRainbow[G] {
     case node: CoerceClassAnyClass[G] => Coercions
     case node: CoerceColToCPrimitive[G] => Coercions
     case node: CoerceCPrimitiveToCol[G] => Coercions
+    case node: CoerceColToCPPPrimitive[G] => Coercions
+    case node: CoerceCPPPrimitiveToCol[G] => Coercions
     case node: CoerceFloatRat[G] => Coercions
     case node: CoerceFracZFrac[G] => Coercions
     case node: CoerceIdentity[G] => Coercions
@@ -208,6 +210,32 @@ class FeatureRainbow[G] {
     case node: OpenCLKernel[G] => CSpecific
     case node: SharedMemSize[G] => CSpecific
 
+    case node: CPPArrayDeclarator[G] => CPPSpecific
+    case node: CPPBool[G] => CPPSpecific
+    case node: CPPDeclaration[G] => CPPSpecific
+    case node: CPPFunctionDefinition[G] => CPPSpecific
+    case node: CPPGlobalDeclaration[G] => CPPSpecific
+    case node: CPPInit[G] => CPPSpecific
+    case node: CPPInline[G] => CPPSpecific
+    case node: CPPInt[G] => CPPSpecific
+    case node: CPPInvocation[G] => CPPSpecific
+    case node: CPPLocal[G] => CPPSpecific
+    case node: CPPLocalDeclaration[G] => CPPSpecific
+    case node: CPPLong[G] => CPPSpecific
+    case node: CPPName[G] => CPPSpecific
+    case node: CPPNamespaceDefinition[G] => CPPSpecific
+    case node: CPPParam[G] => CPPSpecific
+    case node: CPPPrimitiveType[G] => CPPSpecific
+    case node: CPPPure[G] => CPPSpecific
+    case node: CPPShort[G] => CPPSpecific
+    case node: CPPSigned[G] => CPPSpecific
+    case node: CPPSpecificationType[G] => CPPSpecific
+    case node: CPPTranslationUnit[G] => CPPSpecific
+    case node: CPPTypedefName[G] => CPPSpecific
+    case node: CPPTypedFunctionDeclarator[G] => CPPSpecific
+    case node: CPPUnsigned[G] => CPPSpecific
+    case node: CPPVoid[G] => CPPSpecific
+
     case node: CurrentThreadId[G] => CurrentThread
 
     case node: UntypedLiteralSeq[G] => DynamicallyTypedCollection
@@ -643,6 +671,10 @@ class FeatureRainbow[G] {
     case node: CGoto[G] => return Seq(CSpecific, Gotos)
     case node: CPointer[G] => return Seq(CSpecific, Pointers)
     case node: CPointerDeclarator[G] => return Seq(CSpecific, Pointers)
+    case node: CPPChar[G] => return Seq(CPPSpecific, TextTypes)
+    case node: CPPDeclarationStatement[G] => return Seq(CPPSpecific, UnscopedDeclaration)
+    case node: CPPPointer[G] => return Seq(CPPSpecific, Pointers)
+    case node: CPPPointerDeclarator[G] => return Seq(CPPSpecific, Pointers)
     case node: Result[G] => return scanFlatly(node.applicable.decl)
     case node: SilverNewRef[G] => return Seq(Assignment, Resources)
 
diff --git a/src/col/vct/col/print/Ctx.scala b/src/col/vct/col/print/Ctx.scala
index 8b3970d4a5..9ec0e78f7b 100644
--- a/src/col/vct/col/print/Ctx.scala
+++ b/src/col/vct/col/print/Ctx.scala
@@ -2,7 +2,6 @@ package vct.col.print
 
 import vct.col.ast.{Declaration, Node}
 import vct.col.ref.Ref
-import vct.col.resolve.ctx.Referrable
 
 import scala.util.Try
 
@@ -12,6 +11,7 @@ object Ctx {
   case object Silver extends Syntax
   case object Java extends Syntax
   case object C extends Syntax
+  case object CPP extends Syntax
   case object Cuda extends Syntax
   case object OpenCL extends Syntax
 }
diff --git a/src/col/vct/col/print/Namer.scala b/src/col/vct/col/print/Namer.scala
index 2d43790e85..6f1522674d 100644
--- a/src/col/vct/col/print/Namer.scala
+++ b/src/col/vct/col/print/Namer.scala
@@ -4,7 +4,6 @@ import hre.util.ScopedStack
 import vct.col.ast._
 
 import scala.collection.mutable
-import scala.reflect.ClassTag
 
 case class Namer[G](syntax: Ctx.Syntax) {
   private val stack = ScopedStack[Node[G]]()
@@ -58,6 +57,7 @@ case class Namer[G](syntax: Ctx.Syntax) {
     case _: JavaConstructor[G] => ()
     case _: PVLConstructor[G] => ()
     case _: CFunctionDefinition[G] => ()
+    case _: CPPFunctionDefinition[G] => ()
   }
 
   def unpackName(name: String): (String, Int) = {
@@ -104,6 +104,8 @@ case class Namer[G](syntax: Ctx.Syntax) {
       case decl: ParInvariantDecl[G] => nameKeyed(nearest { case _: ParInvariant[G] => () }, decl)
       case decl: CLocalDeclaration[G] => nameKeyed(nearestVariableScope, decl)
       case decl: CParam[G] => nameKeyed(nearestCallable, decl)
+      case decl: CPPLocalDeclaration[G] => nameKeyed(nearestVariableScope, decl)
+      case decl: CPPParam[G] => nameKeyed(nearestCallable, decl)
       case decl: JavaLocalDeclaration[G] => nameKeyed(nearestCallable, decl)
       case decl: VeyMontThread[G] => nameKeyed(nearest { case _: VeyMontSeqProg[G] => () }, decl)
       case decl: JavaParam[G] => nameKeyed(nearestCallable, decl)
diff --git a/src/col/vct/col/resolve/ResolutionError.scala b/src/col/vct/col/resolve/ResolutionError.scala
index 8a368c4744..c2331fb7ca 100644
--- a/src/col/vct/col/resolve/ResolutionError.scala
+++ b/src/col/vct/col/resolve/ResolutionError.scala
@@ -6,7 +6,7 @@ import vct.result.VerificationError.{SystemError, UserError}
 
 trait ResolutionError extends UserError
 
-case class MultipleForwardDeclarationContractError(declaration: CGlobalDeclaration[_]) extends ResolutionError {
+case class MultipleForwardDeclarationContractError(declaration: GlobalDeclaration[_]) extends ResolutionError {
   override def code: String = "multipleForwardDeclarationContract"
 
   override def text: String = declaration.o.messageInContext("Cannot simultaneously bind a contract to multiple global declarations.")
diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala
index 753c423d67..4c3d528245 100644
--- a/src/col/vct/col/resolve/Resolve.scala
+++ b/src/col/vct/col/resolve/Resolve.scala
@@ -10,7 +10,7 @@ import vct.col.origin._
 import vct.col.resolve.ResolveReferences.scanScope
 import vct.col.ref.Ref
 import vct.col.resolve.ctx._
-import vct.col.resolve.lang.{C, Java, PVL, Spec}
+import vct.col.resolve.lang.{C, CPP, Java, PVL, Spec}
 import vct.col.resolve.Resolve.{MalformedBipAnnotation, SpecContractParser, SpecExprParser, getLit, isBip}
 import vct.col.resolve.lang.JavaAnnotationData.{BipComponent, BipData, BipGuard, BipInvariant, BipPort, BipPure, BipStatePredicate, BipTransition}
 import vct.col.rewrite.InitialGeneration
@@ -127,6 +127,10 @@ case object ResolveTypes {
       t.ref = Some(C.findCTypeName(name, ctx).getOrElse(
         throw NoSuchNameError("struct", name, t)
       ))
+    case t@CPPTypedefName(nestedName) =>
+      t.ref = Some(CPP.findCPPTypeName(nestedName, ctx).getOrElse(
+        throw NoSuchNameError("class, struct, or namespace", nestedName, t)
+      ))
     case t @ PVLNamedType(name, typeArgs) =>
       t.ref = Some(PVL.findTypeName(name, ctx).getOrElse(
         throw NoSuchNameError("class", name, t)))
@@ -212,6 +216,7 @@ case object ResolveReferences extends LazyLogging {
     // Remove shared memory locations from the body level of a GPU kernel, we want to reason about them at the top level
     case CDeclarationStatement(decl) if !(inGPUKernel && decl.decl.specs.collectFirst{case GPULocal() => ()}.isDefined)
     => Seq(decl)
+    case CPPDeclarationStatement(decl) => Seq(decl)
     case JavaLocalDeclarationStatement(decl) => Seq(decl)
     case LocalDecl(v) => Seq(v)
     case other => other.subnodes.flatMap(scanScope(_, inGPUKernel))
@@ -301,7 +306,6 @@ case object ResolveReferences extends LazyLogging {
       if(func.decl.contract.nonEmpty && func.decl.inits.size > 1) {
         throw MultipleForwardDeclarationContractError(func)
       }
-
       func.decl.inits.zipWithIndex.foldLeft(
         ctx.declare(func.decl.contract.givenArgs ++ func.decl.contract.yieldsArgs)
       ) {
@@ -311,6 +315,24 @@ case object ResolveReferences extends LazyLogging {
             .declare(info.params.getOrElse(Nil))
             .copy(currentResult=info.params.map(_ => RefCGlobalDeclaration(func, idx)))
       }
+    case func: CPPFunctionDefinition[G] =>
+      ctx
+        .copy(currentResult = Some(RefCPPFunctionDefinition(func)))
+        .declare(CPP.paramsFromDeclarator(func.declarator) ++ scanLabels(func.body) ++ func.contract.givenArgs ++ func.contract.yieldsArgs)
+    case ns: CPPNamespaceDefinition[G] => ctx.declare(ns.declarations)
+    case func: CPPGlobalDeclaration[G] =>
+      if (func.decl.contract.nonEmpty && func.decl.inits.size > 1) {
+        throw MultipleForwardDeclarationContractError(func)
+      }
+      func.decl.inits.zipWithIndex.foldLeft(
+        ctx.declare(func.decl.contract.givenArgs ++ func.decl.contract.yieldsArgs)
+      ) {
+        case (ctx, (init, idx)) =>
+          val info = CPP.getDeclaratorInfo(init.decl)
+          ctx
+            .declare(info.params.getOrElse(Nil))
+            .copy(currentResult = info.params.map(_ => RefCPPGlobalDeclaration(func, idx)))
+      }
     case func: LlvmFunctionDefinition[G] => ctx
       .copy(currentResult = Some(RefLlvmFunctionDefinition(func)))
     case par: ParStatement[G] => ctx
@@ -327,6 +349,8 @@ case object ResolveReferences extends LazyLogging {
   def resolveFlatly[G](node: Node[G], ctx: ReferenceResolutionContext[G]): Unit = node match {
     case local@CLocal(name) =>
       local.ref = Some(C.findCName(name, ctx).getOrElse(throw NoSuchNameError("local", name, local)))
+    case local@CPPLocal(name) =>
+      local.ref = Some(CPP.findCPPName(name, ctx).getOrElse(throw NoSuchNameError("local", name, local)))
     case local @ JavaLocal(name) =>
       val start: Option[JavaNameTarget[G]] = if (ctx.javaBipGuardsEnabled) {
         Java.findJavaBipGuard(ctx, name).map(RefJavaBipGuard(_))
@@ -377,6 +401,10 @@ case object ResolveReferences extends LazyLogging {
       inv.ref = Some(C.resolveInvocation(obj, ctx))
       Spec.resolveGiven(givenMap, inv.ref.get, inv)
       Spec.resolveYields(ctx, yields, inv.ref.get, inv)
+    case inv@CPPInvocation(obj, _, givenMap, yields) =>
+      inv.ref = Some(CPP.resolveInvocation(obj))
+      Spec.resolveGiven(givenMap, inv.ref.get, inv)
+      Spec.resolveYields(ctx, yields, inv.ref.get, inv)
     case inv@GpgpuCudaKernelInvocation(name, blocks, threads, args, givenMap, yields) =>
       val kernel = C.findCName(name, ctx).getOrElse(throw NoSuchNameError("kernel", name, inv))
       inv.ref = Some(kernel match {
@@ -464,6 +492,11 @@ case object ResolveReferences extends LazyLogging {
     case decl: CInit[G] =>
       decl.ref = C.findDefinition(decl.decl, ctx)
 
+    case defn: CPPFunctionDefinition[G] =>
+      defn.ref = CPP.findForwardDeclaration(defn.declarator, ctx)
+    case decl: CPPInit[G] =>
+      decl.ref = CPP.findDefinition(decl.decl, ctx)
+
     case goto@CGoto(name) =>
       goto.ref = Some(Spec.findLabel(name, ctx).getOrElse(throw NoSuchNameError("label", name, goto)))
     case goto@Goto(lbl) =>
diff --git a/src/col/vct/col/resolve/ctx/Referrable.scala b/src/col/vct/col/resolve/ctx/Referrable.scala
index 8a9ee40091..9f48b5aa07 100644
--- a/src/col/vct/col/resolve/ctx/Referrable.scala
+++ b/src/col/vct/col/resolve/ctx/Referrable.scala
@@ -3,7 +3,7 @@ package vct.col.resolve.ctx
 import vct.col.ast._
 import vct.col.origin.SourceNameOrigin
 import vct.col.resolve.NameLost
-import vct.col.resolve.lang.C
+import vct.col.resolve.lang.{C, CPP}
 
 /**
  * Collection of all things that can be cross-referenced in the AST. This includes all declarations, indices at
@@ -19,6 +19,12 @@ sealed trait Referrable[G] {
     case RefCFunctionDefinition(decl) => C.nameFromDeclarator(decl.declarator)
     case RefCGlobalDeclaration(decls, initIdx) => C.nameFromDeclarator(decls.decl.inits(initIdx).decl)
     case RefCLocalDeclaration(decls, initIdx) => C.nameFromDeclarator(decls.decl.inits(initIdx).decl)
+    case RefCPPTranslationUnit(_) => ""
+    case RefCPPParam(decl) => CPP.nameFromDeclarator(decl.declarator)
+    case RefCPPFunctionDefinition(decl) => CPP.nameFromDeclarator(decl.declarator)
+    case RefCPPNamespaceDefinition(_) => ""
+    case RefCPPGlobalDeclaration(decls, initIdx) => CPP.nameFromDeclarator(decls.decl.inits(initIdx).decl)
+    case RefCPPLocalDeclaration(decls, initIdx) => CPP.nameFromDeclarator(decls.decl.inits(initIdx).decl)
     case RefJavaNamespace(_) => ""
     case RefUnloadedJavaNamespace(_) => ""
     case RefJavaClass(decl) => decl.name
@@ -84,6 +90,11 @@ case object Referrable {
     case decl: CParam[G] => RefCParam(decl)
     case decl: CFunctionDefinition[G] => RefCFunctionDefinition(decl)
     case decl: CGlobalDeclaration[G] => return decl.decl.inits.indices.map(RefCGlobalDeclaration(decl, _))
+    case decl: CPPTranslationUnit[G] => RefCPPTranslationUnit(decl)
+    case decl: CPPParam[G] => RefCPPParam(decl)
+    case decl: CPPFunctionDefinition[G] => RefCPPFunctionDefinition(decl)
+    case decl: CPPNamespaceDefinition[G] => RefCPPNamespaceDefinition(decl)
+    case decl: CPPGlobalDeclaration[G] => return decl.decl.inits.indices.map(RefCPPGlobalDeclaration(decl, _))
     case decl: JavaNamespace[G] => RefJavaNamespace(decl)
     case decl: JavaClass[G] => RefJavaClass(decl)
     case decl: JavaInterface[G] => RefJavaClass(decl)
@@ -122,6 +133,7 @@ case object Referrable {
     case decl: ModelProcess[G] => RefModelProcess(decl)
     case decl: ModelAction[G] => RefModelAction(decl)
     case decl: CLocalDeclaration[G] => return decl.decl.inits.indices.map(RefCLocalDeclaration(decl, _))
+    case decl: CPPLocalDeclaration[G] => return decl.decl.inits.indices.map(RefCPPLocalDeclaration(decl, _))
     case decl: JavaLocalDeclaration[G] => return decl.decls.indices.map(RefJavaLocalDeclaration(decl, _))
     case decl: PVLConstructor[G] => RefPVLConstructor(decl)
     case decl: VeyMontSeqProg[G] => RefSeqProg(decl)
@@ -150,13 +162,15 @@ name in Java, we can just search for in-scope JavaNameTarget's with the correct
 
 sealed trait JavaTypeNameTarget[G] extends Referrable[G] with JavaDerefTarget[G]
 sealed trait CTypeNameTarget[G] extends Referrable[G]
+sealed trait CPPTypeNameTarget[G] extends Referrable[G]
 sealed trait PVLTypeNameTarget[G] extends Referrable[G]
-sealed trait SpecTypeNameTarget[G] extends JavaTypeNameTarget[G] with CTypeNameTarget[G] with PVLTypeNameTarget[G]
+sealed trait SpecTypeNameTarget[G] extends JavaTypeNameTarget[G] with CTypeNameTarget[G] with CPPTypeNameTarget[G] with PVLTypeNameTarget[G]
 
 sealed trait JavaNameTarget[G] extends Referrable[G]
 sealed trait CNameTarget[G] extends Referrable[G]
+sealed trait CPPNameTarget[G] extends Referrable[G]
 sealed trait PVLNameTarget[G] extends Referrable[G]
-sealed trait SpecNameTarget[G] extends CNameTarget[G] with JavaNameTarget[G] with PVLNameTarget[G]
+sealed trait SpecNameTarget[G] extends CNameTarget[G] with CPPNameTarget[G] with JavaNameTarget[G] with PVLNameTarget[G]
 
 sealed trait CDerefTarget[G] extends Referrable[G]
 sealed trait JavaDerefTarget[G] extends Referrable[G]
@@ -165,12 +179,16 @@ sealed trait SpecDerefTarget[G] extends CDerefTarget[G] with JavaDerefTarget[G]
 
 sealed trait JavaInvocationTarget[G] extends Referrable[G]
 sealed trait CInvocationTarget[G] extends Referrable[G]
+sealed trait CPPInvocationTarget[G] extends Referrable[G]
 sealed trait PVLInvocationTarget[G] extends Referrable[G]
 sealed trait LlvmInvocationTarget[G] extends Referrable[G]
 sealed trait SpecInvocationTarget[G]
   extends JavaInvocationTarget[G]
     with CNameTarget[G]
-    with CDerefTarget[G] with CInvocationTarget[G]
+    with CDerefTarget[G]
+    with CInvocationTarget[G]
+    with CPPNameTarget[G]
+    with CPPInvocationTarget[G]
     with PVLInvocationTarget[G]
 
 sealed trait ThisTarget[G] extends Referrable[G]
@@ -187,6 +205,12 @@ case class RefCParam[G](decl: CParam[G]) extends Referrable[G] with CNameTarget[
 case class RefCFunctionDefinition[G](decl: CFunctionDefinition[G]) extends Referrable[G] with CNameTarget[G] with CInvocationTarget[G] with ResultTarget[G]
 case class RefCGlobalDeclaration[G](decls: CGlobalDeclaration[G], initIdx: Int) extends Referrable[G] with CNameTarget[G] with CInvocationTarget[G] with ResultTarget[G]
 case class RefCLocalDeclaration[G](decls: CLocalDeclaration[G], initIdx: Int) extends Referrable[G] with CNameTarget[G]
+case class RefCPPTranslationUnit[G](decl: CPPTranslationUnit[G]) extends Referrable[G]
+case class RefCPPParam[G](decl: CPPParam[G]) extends Referrable[G] with CPPNameTarget[G]
+case class RefCPPFunctionDefinition[G](decl: CPPFunctionDefinition[G]) extends Referrable[G] with CPPNameTarget[G] with CPPInvocationTarget[G] with ResultTarget[G]
+case class RefCPPNamespaceDefinition[G](decl: CPPNamespaceDefinition[G]) extends Referrable[G]
+case class RefCPPGlobalDeclaration[G](decls: CPPGlobalDeclaration[G], initIdx: Int) extends Referrable[G] with CPPNameTarget[G] with CPPInvocationTarget[G] with ResultTarget[G]
+case class RefCPPLocalDeclaration[G](decls: CPPLocalDeclaration[G], initIdx: Int) extends Referrable[G] with CPPNameTarget[G]
 case class RefJavaNamespace[G](decl: JavaNamespace[G]) extends Referrable[G]
 case class RefUnloadedJavaNamespace[G](names: Seq[String]) extends Referrable[G] with JavaNameTarget[G] with JavaDerefTarget[G]
 case class RefJavaClass[G](decl: JavaClassOrInterface[G]) extends Referrable[G] with JavaTypeNameTarget[G] with JavaNameTarget[G] with JavaDerefTarget[G] with ThisTarget[G]
diff --git a/src/col/vct/col/resolve/lang/C.scala b/src/col/vct/col/resolve/lang/C.scala
index 0baa8fc084..8b7f27889a 100644
--- a/src/col/vct/col/resolve/lang/C.scala
+++ b/src/col/vct/col/resolve/lang/C.scala
@@ -2,7 +2,6 @@ package vct.col.resolve.lang
 
 import hre.util.FuncTools
 import vct.col.ast._
-import vct.col.ast.`type`.TFloats
 import vct.col.origin._
 import vct.col.resolve._
 import vct.col.resolve.ctx._
diff --git a/src/col/vct/col/resolve/lang/CPP.scala b/src/col/vct/col/resolve/lang/CPP.scala
new file mode 100644
index 0000000000..e121108f6c
--- /dev/null
+++ b/src/col/vct/col/resolve/lang/CPP.scala
@@ -0,0 +1,173 @@
+package vct.col.resolve.lang
+
+import hre.util.FuncTools
+import vct.col.ast._
+import vct.col.origin._
+import vct.col.resolve._
+import vct.col.resolve.ctx._
+import vct.col.typerules.Types
+import vct.result.VerificationError.UserError
+
+case object CPP {
+  implicit private val o: Origin = DiagnosticOrigin
+
+  case class CPPTypeNotSupported(node: Option[Node[_]]) extends UserError {
+    override def code: String = "cppTypeNotSupported"
+
+    override def text: String = {
+      (node match {
+        case Some(node) => node.o.messageInContext(_)
+        case None => (text: String) => text
+      })("This type is not supported by VerCors.")
+    }
+  }
+
+  val NUMBER_LIKE_PREFIXES: Seq[Seq[CPPDeclarationSpecifier[_]]] = Seq(
+    Nil,
+    Seq(CPPUnsigned()),
+    Seq(CPPSigned()),
+  )
+
+  val NUMBER_LIKE_TYPES: Seq[Seq[CPPDeclarationSpecifier[_]]] = Seq(
+    Seq(CPPInt()),
+    Seq(CPPLong()),
+    Seq(CPPLong(), CPPInt()),
+    Seq(CPPLong(), CPPLong()),
+    Seq(CPPLong(), CPPLong(), CPPInt()),
+  )
+
+  val NUMBER_LIKE_SPECIFIERS: Seq[Seq[CPPDeclarationSpecifier[_]]] =
+    for (prefix <- NUMBER_LIKE_PREFIXES; t <- NUMBER_LIKE_TYPES)
+      yield prefix ++ t
+
+  case class DeclaratorInfo[G](params: Option[Seq[CPPParam[G]]], typeOrReturnType: Type[G] => Type[G], name: String)
+
+  def getDeclaratorInfo[G](decl: CPPDeclarator[G]): DeclaratorInfo[G] = decl match {
+    case CPPPointerDeclarator(pointers, inner) =>
+      val innerInfo = getDeclaratorInfo(inner)
+      DeclaratorInfo(
+        innerInfo.params,
+        t => innerInfo.typeOrReturnType(FuncTools.repeat[Type[G]](TPointer(_), pointers.size, t)),
+        innerInfo.name)
+    case array @ CPPArrayDeclarator(inner, size) =>
+      val innerInfo = getDeclaratorInfo(inner)
+      DeclaratorInfo(innerInfo.params, t => innerInfo.typeOrReturnType(CPPTArray(size, t)(array.blame)), innerInfo.name)
+    case CPPTypedFunctionDeclarator(params, _, inner) =>
+      val innerInfo = getDeclaratorInfo(inner)
+      DeclaratorInfo(params = Some(params), typeOrReturnType = (t => t), innerInfo.name)
+    case CPPName(name) => DeclaratorInfo(params = None, typeOrReturnType = (t => t), name)
+  }
+
+  def getPrimitiveType[G](specs: Seq[CPPDeclarationSpecifier[G]], context: Option[Node[G]] = None): Type[G] =
+    specs.collect { case spec: CPPTypeSpecifier[G] => spec } match {
+      case Seq(CPPVoid()) => TVoid()
+      case Seq(CPPChar()) => TChar()
+      case t if CPP.NUMBER_LIKE_SPECIFIERS.contains(t) => TInt()
+      case Seq(CPPSpecificationType(t@TFloat(_, _))) => t
+      case Seq(CPPBool()) => TBool()
+      case Seq(SYCLQueue()) => TSYCLQueue()
+      case Seq(defn@CPPTypedefName(_)) => Types.notAValue(defn.ref.get)
+      case Seq(CPPSpecificationType(typ)) => typ
+      case spec +: _ => throw CPPTypeNotSupported(context.orElse(Some(spec)))
+      case _ => throw CPPTypeNotSupported(context)
+    }
+
+  def nameFromDeclarator(declarator: CPPDeclarator[_]): String =
+    getDeclaratorInfo(declarator).name
+
+  def typeOrReturnTypeFromDeclaration[G](specs: Seq[CPPDeclarationSpecifier[G]], decl: CPPDeclarator[G]): Type[G] =
+    getDeclaratorInfo(decl).typeOrReturnType(CPPPrimitiveType(specs))
+
+  def paramsFromDeclarator[G](declarator: CPPDeclarator[G]): Seq[CPPParam[G]] =
+    getDeclaratorInfo(declarator).params.get
+
+  def findCPPTypeName[G](name: String, ctx: TypeResolutionContext[G]): Option[CPPTypeNameTarget[G]] =
+    ctx.stack.flatten.collectFirst {
+      case target: CPPTypeNameTarget[G] if target.name == name => target
+    }
+
+  def replacePotentialSYCLClassInstance[G](name: String, ctx: ReferenceResolutionContext[G]): String = {
+    if (name.contains('.') && name.count(x => x == '.') == 1) {
+      // Class method, replace with SYCL equivalent
+      val classVarName = name.split('.').head
+      val methodName = name.split('.').last
+
+      // Get type (so class) of variable (instance)
+      val classTarget = ctx.stack.flatten.collectFirst {
+        case target: CPPNameTarget[G] if target.name == classVarName => target
+      }
+      val className = classTarget match {
+        case Some(RefCPPLocalDeclaration(decl, _)) => Some(getPrimitiveType(decl.decl.specs))
+        case Some(RefCPPGlobalDeclaration(decl, _)) => Some(getPrimitiveType(decl.decl.specs))
+        case _ => None
+      }
+      // Replace class reference name to a namespace name
+      if (className.isDefined) {
+        return name.replace(classVarName + ".", "VERCORS::" + className.get.toString + "::VERCORS__")
+      }
+    }
+    name
+  }
+
+  def findCPPName[G](name: String, ctx: ReferenceResolutionContext[G]): Option[CPPNameTarget[G]] = {
+    val targetName: String = replacePotentialSYCLClassInstance(name, ctx)
+
+    var nameSeq = targetName.split("::")
+    if (nameSeq.length == 1) {
+      ctx.stack.flatten.collectFirst {
+        case target: CPPNameTarget[G] if target.name == targetName => target
+      }
+    } else {
+      val ctxTarget: Option[RefCPPNamespaceDefinition[G]] = ctx.stack.flatten.collectFirst {
+        case namespace: RefCPPNamespaceDefinition[G] if namespace.decl.name == nameSeq.head => namespace
+      }
+
+      ctxTarget match {
+        case Some(ref) =>
+          nameSeq = nameSeq.drop(1);
+          var foundNamespace: Option[CPPNamespaceDefinition[G]] = Some(ref.decl)
+          var returnVal: Option[CPPNameTarget[G]] = None;
+          while (nameSeq.nonEmpty) {
+            if (foundNamespace.isEmpty) {
+              return None
+            }
+
+            if (nameSeq.length > 1) {
+              // Look for nested namespaces
+              foundNamespace = foundNamespace.get.declarations.collectFirst {
+                case namespace: CPPNamespaceDefinition[G] if namespace.name == nameSeq.head => namespace
+              }
+            } else {
+              // Look for final nameTarget
+              returnVal = foundNamespace.get.declarations.collectFirst {
+                case funcDef: CPPFunctionDefinition[G] if getDeclaratorInfo(funcDef.declarator).name == nameSeq.head  => RefCPPFunctionDefinition(funcDef)
+                case globalDecl: CPPGlobalDeclaration[G] if getDeclaratorInfo(globalDecl.decl.inits.head.decl).name == nameSeq.head => RefCPPGlobalDeclaration(globalDecl, 0)
+              }
+            }
+            nameSeq = nameSeq.drop(1)
+          }
+          returnVal
+        case None => None
+      }
+    }
+  }
+
+  def findForwardDeclaration[G](declarator: CPPDeclarator[G], ctx: ReferenceResolutionContext[G]): Option[RefCPPGlobalDeclaration[G]] =
+    ctx.stack.flatten.collectFirst {
+      case target: RefCPPGlobalDeclaration[G] if target.name == nameFromDeclarator(declarator) => target
+    }
+
+  def findDefinition[G](declarator: CPPDeclarator[G], ctx: ReferenceResolutionContext[G]): Option[RefCPPFunctionDefinition[G]] =
+    ctx.stack.flatten.collectFirst {
+      case target: RefCPPFunctionDefinition[G] if target.name == nameFromDeclarator(declarator) => target
+    }
+
+  def resolveInvocation[G](obj: Expr[G]): CPPInvocationTarget[G] =
+    obj.t match {
+      case t: TNotAValue[G] => t.decl.get match {
+        case target: CPPInvocationTarget[G] => target
+        case _ => throw NotApplicable(obj)
+      }
+      case _ => throw NotApplicable(obj)
+    }
+}
diff --git a/src/col/vct/col/resolve/lang/Spec.scala b/src/col/vct/col/resolve/lang/Spec.scala
index ea4d94818c..0a54ed53db 100644
--- a/src/col/vct/col/resolve/lang/Spec.scala
+++ b/src/col/vct/col/resolve/lang/Spec.scala
@@ -16,6 +16,9 @@ case object Spec {
     case RefCLocalDeclaration(decls, _) => decls.decl.contract
     case RefCGlobalDeclaration(decls, _) => decls.decl.contract
     case RefCFunctionDefinition(decl) => decl.contract
+    case RefCPPLocalDeclaration(decls, _) => decls.decl.contract
+    case RefCPPGlobalDeclaration(decls, _) => decls.decl.contract
+    case RefCPPFunctionDefinition(decl) => decl.contract
     case RefJavaConstructor(decl) => decl.contract
     case RefJavaMethod(decl) => decl.contract
     case RefPVLConstructor(decl) => decl.contract
diff --git a/src/col/vct/col/rewrite/NonLatchingRewriter.scala b/src/col/vct/col/rewrite/NonLatchingRewriter.scala
index a5fc43f125..1e2ec1d4b7 100644
--- a/src/col/vct/col/rewrite/NonLatchingRewriter.scala
+++ b/src/col/vct/col/rewrite/NonLatchingRewriter.scala
@@ -1,6 +1,5 @@
 package vct.col.rewrite
 
-import hre.debug.TimeTravel
 import vct.col.ast._
 import vct.col.util.CurrentProgramRewriteContext
 import vct.result.VerificationError
@@ -41,6 +40,12 @@ class NonLatchingRewriter[Pre, Post]() extends AbstractRewriter[Pre, Post] {
   override def dispatch(node: CInit[Pre]): CInit[Post] = rewriteDefault(node)
   override def dispatch(node: CDeclaration[Pre]): CDeclaration[Post] = rewriteDefault(node)
 
+  override def dispatch(node: CPPDeclarator[Pre]): CPPDeclarator[Post] = rewriteDefault(node)
+  override def dispatch(node: CPPDeclarationSpecifier[Pre]): CPPDeclarationSpecifier[Post] = rewriteDefault(node)
+  override def dispatch(node: CPPPointer[Pre]): CPPPointer[Post] = rewriteDefault(node)
+  override def dispatch(node: CPPInit[Pre]): CPPInit[Post] = rewriteDefault(node)
+  override def dispatch(node: CPPDeclaration[Pre]): CPPDeclaration[Post] = rewriteDefault(node)
+
   override def dispatch(node: JavaVariableDeclaration[Pre]): JavaVariableDeclaration[Post] = rewriteDefault(node)
   override def dispatch(node: JavaModifier[Pre]): JavaModifier[Post] = rewriteDefault(node)
   override def dispatch(node: JavaImport[Pre]): JavaImport[Post] = rewriteDefault(node)
diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala
index a6b0912489..446d1bcadb 100644
--- a/src/col/vct/col/typerules/CoercingRewriter.scala
+++ b/src/col/vct/col/typerules/CoercingRewriter.scala
@@ -177,6 +177,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case CoerceJavaClassAnyClass(_) => e
       case CoerceCPrimitiveToCol(_, _) => e
       case CoerceColToCPrimitive(_, _) => e
+      case CoerceCPPPrimitiveToCol(_, _) => e
+      case CoerceColToCPPPrimitive(_, _) => e
       case CoerceNullRef() => e
       case CoerceNullArray(_) => e
       case CoerceNullClass(_) => e
@@ -217,7 +219,11 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
     case node: CTypeQualifier[Pre] => node
     case node: CPointer[Pre] => node
     case node: CInit[Pre] => node
-    case node: CDeclaration[Pre] => node
+    case node: CPPDeclarator[Pre] => node
+    case node: CPPDeclarationSpecifier[Pre] => node
+    case node: CPPDeclaration[Pre] => node
+    case node: CPPPointer[Pre] => node
+    case node: CPPInit[Pre] => node
     case node: GpuMemoryFence[Pre] => node
     case node: JavaModifier[Pre] => node
     case node: JavaImport[Pre] => node
@@ -351,6 +357,26 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
   def postCoerce(node: GpuMemoryFence[Pre]): GpuMemoryFence[Post] = rewriteDefault(node)
   override final def dispatch(node: GpuMemoryFence[Pre]): GpuMemoryFence[Post] = postCoerce(coerce(preCoerce(node)))
 
+  def preCoerce(node: CPPDeclarator[Pre]): CPPDeclarator[Pre] = node
+  def postCoerce(node: CPPDeclarator[Pre]): CPPDeclarator[Post] = rewriteDefault(node)
+  override final def dispatch(node: CPPDeclarator[Pre]): CPPDeclarator[Post] = postCoerce(coerce(preCoerce(node)))
+
+  def preCoerce(node: CPPDeclarationSpecifier[Pre]): CPPDeclarationSpecifier[Pre] = node
+  def postCoerce(node: CPPDeclarationSpecifier[Pre]): CPPDeclarationSpecifier[Post] = rewriteDefault(node)
+  override final def dispatch(node: CPPDeclarationSpecifier[Pre]): CPPDeclarationSpecifier[Post] = postCoerce(coerce(preCoerce(node)))
+
+  def preCoerce(node: CPPDeclaration[Pre]): CPPDeclaration[Pre] = node
+  def postCoerce(node: CPPDeclaration[Pre]): CPPDeclaration[Post] = rewriteDefault(node)
+  override final def dispatch(node: CPPDeclaration[Pre]): CPPDeclaration[Post] = postCoerce(coerce(preCoerce(node)))
+
+  def preCoerce(node: CPPPointer[Pre]): CPPPointer[Pre] = node
+  def postCoerce(node: CPPPointer[Pre]): CPPPointer[Post] = rewriteDefault(node)
+  override final def dispatch(node: CPPPointer[Pre]): CPPPointer[Post] = postCoerce(coerce(preCoerce(node)))
+
+  def preCoerce(node: CPPInit[Pre]): CPPInit[Pre] = node
+  def postCoerce(node: CPPInit[Pre]): CPPInit[Post] = rewriteDefault(node)
+  override final def dispatch(node: CPPInit[Pre]): CPPInit[Post] = postCoerce(coerce(preCoerce(node)))
+
   def preCoerce(node: JavaName[Pre]): JavaName[Pre] = node
   def postCoerce(node: JavaName[Pre]): JavaName[Post] = rewriteDefault(node)
   override final def dispatch(node: JavaName[Pre]): JavaName[Post] = postCoerce(coerce(preCoerce(node)))
@@ -878,6 +904,9 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         val (coercedXs, TSeq(element)) = seq(xs)
         val sharedType = Types.leastCommonSuperType(x.t, element)
         Cons(coerce(x, sharedType), coerce(xs, TSeq(sharedType)))
+      case inv@CPPInvocation(applicable, args, givenArgs, yields) =>
+        CPPInvocation(applicable, args, givenArgs, yields)(inv.blame)
+      case CPPLocal(name) => e
       case StringConcat(left, right) =>
         StringConcat(string(left), string(right))
       case acc @ CStructAccess(struct, field) =>
@@ -1543,6 +1572,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case CGoto(label) => CGoto(label)
       case c @ Commit(obj) => Commit(cls(obj))(c.blame)
       case Continue(label) => Continue(label)
+      case CPPDeclarationStatement(decl) => CPPDeclarationStatement(decl)
       case DefaultCase() => DefaultCase()
       case Eval(expr) => Eval(expr)
       case e @ Exhale(assn) => Exhale(res(assn))(e.blame)
@@ -1604,6 +1634,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
     decl match {
       case unit: CTranslationUnit[Pre] =>
         new CTranslationUnit(unit.declarations)
+      case unit: CPPTranslationUnit[Pre] =>
+        new CPPTranslationUnit(unit.declarations)
       case variable: HeapVariable[Pre] =>
         new HeapVariable(variable.t)
       case rule: SimplificationRule[Pre] =>
@@ -1628,6 +1660,12 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         definition
       case declaration: CGlobalDeclaration[Pre] =>
         declaration
+      case definition: CPPFunctionDefinition[Pre] =>
+        definition
+      case namespace: CPPNamespaceDefinition[Pre] =>
+        namespace
+      case declaration: CPPGlobalDeclaration[Pre] =>
+        declaration
       case namespace: JavaNamespace[Pre] =>
         namespace
       case clazz: JavaClass[Pre] =>
@@ -1694,6 +1732,10 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         param
       case decl: CLocalDeclaration[Pre] =>
         decl
+      case param: CPPParam[Pre] =>
+        param
+      case decl: CPPLocalDeclaration[Pre] =>
+        decl
       case declaration: JavaLocalDeclaration[Pre] =>
         new JavaLocalDeclaration[Pre](declaration.modifiers, declaration.t, declaration.decls.map {
           case JavaVariableDeclaration(name, dims, None) => JavaVariableDeclaration(name, dims, None)
@@ -1929,6 +1971,57 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
     }
   }
 
+  def coerce(node: CPPDeclarator[Pre]): CPPDeclarator[Pre] = {
+    implicit val o: Origin = node.o
+    node match {
+      case CPPPointerDeclarator(pointers, inner) =>
+        CPPPointerDeclarator(pointers, inner)
+      case array @ CPPArrayDeclarator(inner, size) =>
+        CPPArrayDeclarator(inner, size.map(int))(array.blame)
+      case CPPTypedFunctionDeclarator(params, varargs, inner) =>
+        CPPTypedFunctionDeclarator(params, varargs, inner)
+      case CPPName(name) =>
+        CPPName(name)
+    }
+  }
+
+  def coerce(node: CPPDeclarationSpecifier[Pre]): CPPDeclarationSpecifier[Pre] = {
+    implicit val o: Origin = node.o
+    node match {
+      case CPPPure() => CPPPure()
+      case CPPInline() => CPPInline()
+      case CPPVoid() => CPPVoid()
+      case CPPChar() => CPPChar()
+      case CPPShort() => CPPShort()
+      case CPPInt() => CPPInt()
+      case CPPLong() => CPPLong()
+      case CPPSigned() => CPPSigned()
+      case CPPUnsigned() => CPPUnsigned()
+      case CPPBool() => CPPBool()
+      case CPPTypedefName(name) => CPPTypedefName(name)
+      case CPPSpecificationType(t) => CPPSpecificationType(t)
+      case SYCLQueue() => SYCLQueue()
+    }
+  }
+
+  def coerce(node: CPPDeclaration[Pre]): CPPDeclaration[Pre] = {
+    implicit val o: Origin = node.o
+    val CPPDeclaration(contract, specs, init) = node
+    CPPDeclaration(contract, specs, init)
+  }
+
+  def coerce(node: CPPPointer[Pre]): CPPPointer[Pre] = {
+    implicit val o: Origin = node.o
+    val CPPPointer() = node
+    CPPPointer()
+  }
+
+  def coerce(node: CPPInit[Pre]): CPPInit[Pre] = {
+    implicit val o: Origin = node.o
+    val CPPInit(decl, init) = node
+    CPPInit(decl, init)
+  }
+
   def coerce(node: JavaName[Pre]): JavaName[Pre] = {
     implicit val o: Origin = node.o
     val JavaName(names) = node
diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala
index 6d87e9f72f..1e12e8dc3b 100644
--- a/src/col/vct/col/typerules/CoercionUtils.scala
+++ b/src/col/vct/col/typerules/CoercionUtils.scala
@@ -57,6 +57,8 @@ case object CoercionUtils {
 
       case (_ @ CTArray(_, innerType), _ @ TArray(element)) if element == innerType =>
         CoerceCArrayPointer(element)
+      case (_@CPPTArray(_, innerType), _@TArray(element)) if element == innerType =>
+        CoerceCPPArrayPointer(element)
 
       case (TBool(), TResource()) => CoerceBoolResource()
       case (TFraction(), TZFraction()) => CoerceFracZFrac()
@@ -122,6 +124,26 @@ case object CoercionUtils {
           case None => return None
         }
 
+      case (source@CPPPrimitiveType(specs), target) =>
+        specs.collectFirst { case spec: CPPSpecificationType[G] => spec } match {
+          case Some(CPPSpecificationType(t)) =>
+            CoercionSequence(Seq(
+              CoerceCPPPrimitiveToCol(source, t),
+              getCoercion(t, target).getOrElse(return None),
+            ))
+          case None => return None
+        }
+
+      case (source, target@CPPPrimitiveType(specs)) =>
+        specs.collectFirst { case spec: CPPSpecificationType[G] => spec } match {
+          case Some(CPPSpecificationType(t)) =>
+            CoercionSequence(Seq(
+              getCoercion(source, t).getOrElse(return None),
+              CoerceColToCPPPrimitive(t, target),
+            ))
+          case None => return None
+        }
+
       // Something with TVar?
 
       // Unsafe coercions
@@ -157,26 +179,48 @@ case object CoercionUtils {
       case None => None
     }
 
+  def getAnyCPPCoercion[G](source: Type[G]): Option[(Coercion[G], Type[G])] = source match {
+    case t: CPPPrimitiveType[G] =>
+      t.specifiers.collectFirst { case spec: CPPSpecificationType[G] => spec }.map {
+        case CPPSpecificationType(inner) => (CoerceCPPPrimitiveToCol(t, inner), inner)
+      }
+    case _ => None
+  }
+
+  def chainCPPCoercion[G, T](source: CPPPrimitiveType[G], next: Type[G] => Option[(Coercion[G], T)]): Option[(Coercion[G], T)] =
+    getAnyCPPCoercion(source) match {
+      case Some(inner) => next(inner._2) match {
+        case Some((coercion, finalType)) =>
+          Some((CoercionSequence(Seq(coercion, inner._1)), finalType))
+        case None => None
+      }
+      case None => None
+    }
+
   def getAnySeqCoercion[G](source: Type[G]): Option[(Coercion[G], TSeq[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnySeqCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySeqCoercion)
     case t: TSeq[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
 
   def getAnySetCoercion[G](source: Type[G]): Option[(Coercion[G], TSet[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnySetCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySetCoercion)
     case t: TSet[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
 
   def getAnyBagCoercion[G](source: Type[G]): Option[(Coercion[G], TBag[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnyBagCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyBagCoercion)
     case t: TBag[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
 
   def getAnySizedCoercion[G](source: Type[G]): Option[(Coercion[G], SizedType[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnySizedCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySizedCoercion)
     case t: TSeq[G] => Some((CoerceIdentity(source), t))
     case t: TSet[G] => Some((CoerceIdentity(source), t))
     case t: TBag[G] => Some((CoerceIdentity(source), t))
@@ -189,6 +233,8 @@ case object CoercionUtils {
     case t: TPointer[G] => Some((CoerceIdentity(source), t))
     case t: CTPointer[G] => Some((CoerceIdentity(source), TPointer(t.innerType)))
     case t: CTArray[G] => Some((CoerceCArrayPointer(t.innerType), TPointer(t.innerType)))
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyPointerCoercion)
+    case t: CPPTArray[G] => Some((CoerceCPPArrayPointer(t.innerType), TPointer(t.innerType)))
     case _: TNull[G] =>
       val t = TPointer[G](TAny())
       Some((CoerceNullPointer(t), t))
@@ -201,8 +247,15 @@ case object CoercionUtils {
     case _ => None
   }
 
+  def getAnyCPPArrayCoercion[G](source: Type[G]): Option[(Coercion[G], CPPTArray[G])] = source match {
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyCPPArrayCoercion)
+    case t: CPPTArray[G] => Some((CoerceIdentity(source), t))
+    case _ => None
+  }
+
   def getAnyArrayCoercion[G](source: Type[G]): Option[(Coercion[G], TArray[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnyArrayCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyArrayCoercion)
     case t: TArray[G] => Some((CoerceIdentity(source), t))
     case _: TNull[G] =>
       val t = TArray[G](TAny())
@@ -212,6 +265,7 @@ case object CoercionUtils {
 
   def getAnyMatrixArrayCoercion[G](source: Type[G]): Option[(Coercion[G], TArray[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnyMatrixArrayCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyMatrixArrayCoercion)
     case t @ TArray(TArray(_)) => Some((CoerceIdentity(source), t))
     case TArray(TNull()) => Some(???)
     case TNull() =>
@@ -222,36 +276,42 @@ case object CoercionUtils {
 
   def getAnyOptionCoercion[G](source: Type[G]): Option[(Coercion[G], TOption[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnyOptionCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyOptionCoercion)
     case t: TOption[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
 
   def getAnyMapCoercion[G](source: Type[G]): Option[(Coercion[G], TMap[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnyMapCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyMapCoercion)
     case t: TMap[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
 
   def getAnyTupleCoercion[G](source: Type[G]): Option[(Coercion[G], TTuple[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnyTupleCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyTupleCoercion)
     case t: TTuple[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
 
   def getAnyMatrixCoercion[G](source: Type[G]): Option[(Coercion[G], TMatrix[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnyMatrixCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyMatrixCoercion)
     case t: TMatrix[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
 
   def getAnyModelCoercion[G](source: Type[G]): Option[(Coercion[G], TModel[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnyModelCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyModelCoercion)
     case t: TModel[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
 
   def getAnyClassCoercion[G](source: Type[G]): Option[(Coercion[G], TClass[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnyClassCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyClassCoercion)
     case t: TClass[G] => Some((CoerceIdentity(source), t))
 
     case t: TUnion[G] =>
@@ -271,30 +331,35 @@ case object CoercionUtils {
 
   def getAnyEitherCoercion[G](source: Type[G]): Option[(Coercion[G], TEither[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnyEitherCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyEitherCoercion)
     case t: TEither[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
 
   def getAnyBitvecCoercion[G](source: Type[G]): Option[(Coercion[G], TSmtlibBitVector[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnyBitvecCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyBitvecCoercion)
     case t: TSmtlibBitVector[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
 
   def getAnySmtlibFloatCoercion[G](source: Type[G]): Option[(Coercion[G], TSmtlibFloatingPoint[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnySmtlibFloatCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySmtlibFloatCoercion)
     case t: TSmtlibFloatingPoint[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
 
   def getAnySmtlibArrayCoercion[G](source: Type[G]): Option[(Coercion[G], TSmtlibArray[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnySmtlibArrayCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySmtlibArrayCoercion)
     case t: TSmtlibArray[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
 
   def getAnySmtlibSeqCoercion[G](source: Type[G]): Option[(Coercion[G], TSmtlibSeq[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnySmtlibSeqCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySmtlibSeqCoercion)
     case t: TSmtlibSeq[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
diff --git a/src/colhelper/ColDefs.scala b/src/colhelper/ColDefs.scala
index 85ce4d714a..0f1e03cc6e 100644
--- a/src/colhelper/ColDefs.scala
+++ b/src/colhelper/ColDefs.scala
@@ -37,6 +37,8 @@ object ColDefs {
     "ParInvariantDecl",
     "CLocalDeclaration",
     "CParam",
+    "CPPLocalDeclaration",
+    "CPPParam",
     "JavaLocalDeclaration",
     "VeyMontThread",
     "JavaParam",
@@ -70,6 +72,7 @@ object ColDefs {
       "InstanceFunction", "InstanceMethod",
       "JavaConstructor", "JavaMethod",
       "CFunctionDefinition",
+      "CPPFunctionDefinition",
       "PVLConstructor",
       "LlvmFunctionDefinition"
       // Potentially ParBlocks and other execution contexts (lambdas?) should be a scope too.
@@ -84,6 +87,13 @@ object ColDefs {
     "CParam" -> Seq(
       "CGlobalDeclaration", "CFunctionDefinition",
     ),
+    "CPPLocalDeclaration" -> Seq(
+      "CPPGlobalDeclaration", "CPPFunctionDefinition",
+      "Scope",
+    ),
+    "CPPParam" -> Seq(
+      "CPPGlobalDeclaration", "CPPFunctionDefinition",
+    ),
     "JavaLocalDeclaration" -> Seq(
       "JavaConstructor", "JavaMethod",
       "Scope",
diff --git a/src/main/vct/main/stages/Parsing.scala b/src/main/vct/main/stages/Parsing.scala
index c4b32e76bd..fa24a72562 100644
--- a/src/main/vct/main/stages/Parsing.scala
+++ b/src/main/vct/main/stages/Parsing.scala
@@ -5,11 +5,10 @@ import hre.stages.Stage
 import vct.col.rewrite.Generation
 import vct.main.stages.Parsing.{Language, UnknownFileExtension}
 import vct.options.Options
-import vct.parsers.transform.{BlameProvider, ReadableOriginProvider}
 import vct.parsers._
+import vct.parsers.transform.{BlameProvider, ReadableOriginProvider}
 import vct.resources.Resources
 import vct.result.VerificationError.UserError
-import viper.api
 import viper.api.transform.ColSilverParser
 
 import java.nio.file.Path
@@ -21,7 +20,9 @@ case object Parsing {
     def fromFilename(filename: String): Option[Language] =
       filename.split('.').last match {
         case "cl" | "c" | "cu" => Some(C)
+        case "cpp" => Some(CPP)
         case "i" => Some(InterpretedC)
+        case "ipp" => Some(InterpretedCPP)
         case "java" => Some(Java)
         case "pvl" => Some(PVL)
         case "sil" | "vpr" => Some(Silver)
@@ -32,6 +33,8 @@ case object Parsing {
 
     case object C extends Language
     case object InterpretedC extends Language
+    case object CPP extends Language
+    case object InterpretedCPP extends Language
     case object Java extends Language
     case object PVL extends Language
     case object Silver extends Language
@@ -63,6 +66,10 @@ case class Parsing[G <: Generation]
   cSystemInclude: Path = Resources.getCIncludePath,
   cOtherIncludes: Seq[Path] = Nil,
   cDefines: Map[String, String] = Map.empty,
+  ccpp: Path = Resources.getCPPcPath,
+  cppSystemInclude: Path = Resources.getCPPIncludePath,
+  cppOtherIncludes: Seq[Path] = Nil,
+  cppDefines: Map[String, String] = Map.empty,
 ) extends Stage[Seq[Readable], ParseResult[G]] {
   override def friendlyName: String = "Parsing"
   override def progressWeight: Int = 4
@@ -78,6 +85,8 @@ case class Parsing[G <: Generation]
       val parser = language match {
         case Language.C => ColCParser(originProvider, blameProvider, cc, cSystemInclude, cOtherIncludes, cDefines)
         case Language.InterpretedC => ColIParser(originProvider, blameProvider)
+        case Language.CPP => ColCPPParser(originProvider, blameProvider, ccpp, cppSystemInclude, cppOtherIncludes, cppDefines)
+        case Language.InterpretedCPP => ColIPPParser(originProvider, blameProvider)
         case Language.Java => ColJavaParser(originProvider, blameProvider)
         case Language.PVL => ColPVLParser(originProvider, blameProvider)
         case Language.Silver => ColSilverParser(originProvider, blameProvider)
diff --git a/src/main/vct/main/stages/Resolution.scala b/src/main/vct/main/stages/Resolution.scala
index 7ab5de1c95..f1504cf014 100644
--- a/src/main/vct/main/stages/Resolution.scala
+++ b/src/main/vct/main/stages/Resolution.scala
@@ -2,31 +2,24 @@ package vct.main.stages
 
 import com.typesafe.scalalogging.LazyLogging
 import hre.stages.Stage
-import vct.col.ast.{AddrOf, ApplicableContract, CGlobalDeclaration, Expr, LlvmFunctionContract, Program, Refute, Verification, VerificationContext}
 import org.antlr.v4.runtime.CharStreams
+import vct.col.ast._
 import vct.col.check.CheckError
-import vct.col.rewrite.lang.{LangSpecificToCol, LangTypesToCol}
-import vct.col.origin.{ExpectedError, FileSpanningOrigin, LLVMOrigin, Origin}
-import vct.col.resolve.lang.{C, Java}
+import vct.col.origin.{FileSpanningOrigin, LLVMOrigin, Origin}
 import vct.col.resolve.{Resolve, ResolveReferences, ResolveTypes}
 import vct.col.rewrite.Generation
 import vct.col.rewrite.bip.IsolateBipGlue
+import vct.col.rewrite.lang.{LangSpecificToCol, LangTypesToCol}
 import vct.importer.JavaLibraryLoader
-import vct.main.Main.TemporarilyUnsupported
 import vct.main.stages.Resolution.InputResolutionError
-import vct.main.stages.Transformation.TransformationCheckError
 import vct.options.Options
 import vct.options.types.ClassPathEntry
-import vct.parsers.ParseResult
-import vct.parsers.transform.BlameProvider
-import vct.parsers.{ColJavaParser, ColLLVMParser, FileNotFound, ParseResult}
 import vct.parsers.transform.{BlameProvider, ReadableOriginProvider, RedirectOriginProvider}
+import vct.parsers.{ColJavaParser, ColLLVMParser, FileNotFound, ParseResult}
 import vct.resources.Resources
 import vct.result.VerificationError.UserError
-import viper.silver.frontend.DefaultStates.Initial
 
 import java.io.{FileNotFoundException, Reader}
-import java.nio.file.Path
 
 case object Resolution {
   case class InputResolutionError(errors: Seq[CheckError]) extends UserError {
diff --git a/src/main/vct/options/Options.scala b/src/main/vct/options/Options.scala
index 5f512df5ec..d1295c7e85 100644
--- a/src/main/vct/options/Options.scala
+++ b/src/main/vct/options/Options.scala
@@ -1,10 +1,10 @@
 package vct.options
 
-import scopt.{OParser, OptionDef}
+import scopt.OParser
 import scopt.Read._
 import vct.main.BuildInfo
 import vct.main.stages.Parsing.Language
-import vct.options.types.{Backend, ClassPathEntry, Mode, PathOrStd, ReadLanguage, Verbosity}
+import vct.options.types._
 import vct.resources.Resources
 
 import java.nio.file.{Path, Paths}
@@ -349,6 +349,8 @@ case class Options
   adtPath: Path = Resources.getAdtPath,
   cc: Path = Resources.getCcPath,
   cIncludePath: Path = Resources.getCIncludePath,
+  ccpp: Path = Resources.getCPPcPath,
+  cppIncludePath: Path = Resources.getCPPIncludePath,
   classPath: Seq[ClassPathEntry] = Seq(ClassPathEntry.DefaultJre, ClassPathEntry.SourcePackageRoot),
   z3Path: Path = viper.api.Resources.getZ3Path,
   boogiePath: Path = viper.api.Resources.getBoogiePath,
diff --git a/src/main/vct/options/types/ReadLanguage.scala b/src/main/vct/options/types/ReadLanguage.scala
index aa64ca6c6e..92e8915eca 100644
--- a/src/main/vct/options/types/ReadLanguage.scala
+++ b/src/main/vct/options/types/ReadLanguage.scala
@@ -7,6 +7,8 @@ case object ReadLanguage extends ReadEnum[Language] {
     "java" -> Language.Java,
     "c" -> Language.C,
     "i" -> Language.InterpretedC,
+    "cpp" -> Language.CPP,
+    "ipp" -> Language.InterpretedCPP,
     "pvl" -> Language.PVL,
     "silver" -> Language.Silver,
     "systemc" -> Language.SystemC,
diff --git a/src/main/vct/resources/Resources.scala b/src/main/vct/resources/Resources.scala
index 9507218be9..61af891ad2 100644
--- a/src/main/vct/resources/Resources.scala
+++ b/src/main/vct/resources/Resources.scala
@@ -1,11 +1,7 @@
 package vct.resources
 
-import hre.platform.Platform
-import hre.resource.ResourceUtil.{getPlatformBinary, getResource}
-import vct.result.VerificationError.SystemError
+import hre.resource.ResourceUtil.getResource
 
-import java.io.File
-import java.net.URISyntaxException
 import java.nio.file.{Path, Paths}
 
 case object Resources {
@@ -14,7 +10,9 @@ case object Resources {
 
   def getAdtPath: Path = getResource("/adt")
   def getCIncludePath: Path = getResource("/c")
+  def getCPPIncludePath: Path = getResource("/cpp")
   def getJrePath: Path = getResource("/jdk")
   def getCcPath: Path = Paths.get("clang")
+  def getCPPcPath: Path = Paths.get("clang++")
   def getSystemCConfig: Path = getResource("/systemc/config")
 }
diff --git a/src/parsers/antlr4/CPPParser.g4 b/src/parsers/antlr4/CPPParser.g4
new file mode 100644
index 0000000000..b029041617
--- /dev/null
+++ b/src/parsers/antlr4/CPPParser.g4
@@ -0,0 +1,19 @@
+parser grammar CPPParser;
+options {tokenVocab = LangCPPLexer;}
+import LangCPPParser, SpecParser;
+
+@parser::members {
+    public int specLevel = 0;
+}
+
+langExpr: expression;
+langId: clangppIdentifier;
+langConstInt: literal;
+langType: typeSpecifier;
+langStatement: statement;
+langStatic: EOF EOF;
+langGlobalDecl: declaration;
+langClassDecl: EOF EOF;
+
+startSpec: LineStartSpec {specLevel++;} | BlockStartSpec {specLevel++;} | BlockStartSpecImmediate {specLevel++;};
+endSpec: EndSpec {specLevel--;};
diff --git a/src/parsers/antlr4/LangCLexer.g4 b/src/parsers/antlr4/LangCLexer.g4
index ad7a04e181..4035d02477 100644
--- a/src/parsers/antlr4/LangCLexer.g4
+++ b/src/parsers/antlr4/LangCLexer.g4
@@ -17,6 +17,7 @@ VAL_TRUE: 'true';
 VAL_FALSE: 'false';
 VAL_SIZEOF: EOF EOF;
 VAL_PACKAGE: 'package';
+CONS: '::';
 
 Placeholder : EOF EOF ;
 
diff --git a/src/parsers/antlr4/LangCPPLexer.g4 b/src/parsers/antlr4/LangCPPLexer.g4
new file mode 100644
index 0000000000..a0cece3c57
--- /dev/null
+++ b/src/parsers/antlr4/LangCPPLexer.g4
@@ -0,0 +1,321 @@
+lexer grammar LangCPPLexer;
+import SpecLexer;
+
+@lexer::members {
+    private static boolean inBlockSpec = false;
+    private static boolean inLineSpec = false;
+}
+
+channels {
+  EXPECTED_ERROR_CHANNEL,
+  LINE_DIRECTIVE_CHANNEL
+}
+
+// lexer tokens needed for the SpecParser
+VAL_INLINE: EOF EOF;
+VAL_ASSERT: 'assert';
+VAL_PACKAGE: 'package';
+VAL_BOOL: EOF EOF;
+
+IntegerLiteral:
+	DecimalLiteral Integersuffix?
+	| OctalLiteral Integersuffix?
+	| HexadecimalLiteral Integersuffix?
+	| BinaryLiteral Integersuffix?;
+
+CharacterLiteral:
+	('u' | 'U' | 'L')? '\'' Cchar+ '\'';
+
+FloatingLiteral:
+	Fractionalconstant Exponentpart? Floatingsuffix?
+	| Digitsequence Exponentpart Floatingsuffix?;
+
+StringLiteral:
+	Encodingprefix?
+    (Rawstring
+	|'"' Schar* '"');
+
+BooleanLiteral: False | True;
+
+PointerLiteral: Nullptr;
+
+// EW: Will be moved to own SYCL lexer later
+SYCLQueue: 'sycl::queue';
+
+UserDefinedLiteral:
+	UserDefinedIntegerLiteral
+	| UserDefinedFloatingLiteral
+	| UserDefinedStringLiteral
+	| UserDefinedCharacterLiteral;
+
+MultiLineMacro:
+	'#' (~[\n]*? '\\' '\r'? '\n')+ ~ [\n]+ -> channel (LINE_DIRECTIVE_CHANNEL);
+
+Directive: '#' ~ [\n]* -> channel (LINE_DIRECTIVE_CHANNEL);
+
+Alignas: 'alignas';
+Alignof: 'alignof';
+Asm: 'asm';
+Auto: 'auto';
+Bool: 'bool';
+Break: 'break';
+Case: 'case';
+Catch: 'catch';
+Char: 'char';
+Char16: 'char16_t';
+Char32: 'char32_t';
+Class: 'class';
+Const: 'const';
+Constexpr: 'constexpr';
+Const_cast: 'const_cast';
+Continue: 'continue';
+Decltype: 'decltype';
+Default: 'default';
+Delete: 'delete';
+Do: 'do';
+Double: 'double';
+Dynamic_cast: 'dynamic_cast';
+Else: 'else';
+Enum: 'enum';
+Explicit: 'explicit';
+Export: 'export';
+Extern: 'extern';
+False: 'false';
+Final: 'final';
+Float: 'float';
+For: 'for';
+Friend: 'friend';
+Goto: 'goto';
+If: 'if';
+Inline: 'inline';
+Int: 'int';
+Long: 'long';
+Mutable: 'mutable';
+Namespace: 'namespace';
+New: 'new';
+Noexcept: 'noexcept';
+Nullptr: 'nullptr';
+Operator: 'operator';
+Override: 'override';
+Private: 'private';
+Protected: 'protected';
+Public: 'public';
+Register: 'register';
+Reinterpret_cast: 'reinterpret_cast';
+Return: 'return';
+Short: 'short';
+Signed: 'signed';
+Sizeof: 'sizeof';
+Static: 'static';
+Static_assert: 'static_assert';
+Static_cast: 'static_cast';
+Struct: 'struct';
+Switch: 'switch';
+Template: 'template';
+This: 'this';
+Thread_local: '_thread_local';
+Throw: 'throw';
+True: 'true';
+Try: 'try';
+Typedef: 'typedef';
+Typeid_: 'typeid';
+Typename_: 'typename';
+Union: 'union';
+Unsigned: 'unsigned';
+Using: 'using';
+Virtual: 'virtual';
+Void: 'void';
+Volatile: 'volatile';
+Wchar: 'wchar_t';
+While: 'while';
+
+LeftParen: '(';
+RightParen: ')';
+LeftBracket: '[';
+RightBracket: ']';
+LeftBrace: '{';
+RightBrace: '}';
+Plus: '+';
+Minus: '-';
+Star: '*';
+Div: '/';
+Mod: '%';
+Caret: '^';
+And: '&';
+Or: '|';
+Tilde: '~';
+Not: '!';
+NotWord: 'not';
+Assign: '=';
+Less: '<';
+Greater: '>';
+PlusAssign: '+=';
+MinusAssign: '-=';
+StarAssign: '*=';
+DivAssign: '/=';
+ModAssign: '%=';
+XorAssign: '^=';
+AndAssign: '&=';
+OrAssign: '|=';
+LeftShiftAssign: '<<=';
+RightShiftAssign: '>>=';
+Equal: '==';
+NotEqual: '!=';
+LessEqual: '<=';
+GreaterEqual: '>=';
+AndAnd: '&&' | 'and';
+OrOr: '||' | 'or';
+PlusPlus: '++';
+MinusMinus: '--';
+Comma: ',';
+ArrowStar: '->*';
+Arrow: '->';
+Question: '?';
+Colon: ':';
+Doublecolon: '::';
+Semi: ';';
+Dot: '.';
+DotStar: '.*';
+Ellipsis: '...';
+fragment Hexquad:
+	HEXADECIMALDIGIT HEXADECIMALDIGIT HEXADECIMALDIGIT HEXADECIMALDIGIT;
+
+fragment Universalcharactername:
+	'\\u' Hexquad
+	| '\\U' Hexquad Hexquad;
+
+fragment Identifiernondigit: NONDIGIT | Universalcharactername;
+
+fragment NONDIGIT: [a-zA-Z_];
+
+fragment DIGIT: [0-9];
+
+DecimalLiteral: NONZERODIGIT ('\''? DIGIT)*;
+
+OctalLiteral: '0' ('\''? OCTALDIGIT)*;
+
+HexadecimalLiteral: ('0x' | '0X') HEXADECIMALDIGIT (
+		'\''? HEXADECIMALDIGIT
+	)*;
+
+BinaryLiteral: ('0b' | '0B') BINARYDIGIT ('\''? BINARYDIGIT)*;
+
+fragment NONZERODIGIT: [1-9];
+
+fragment OCTALDIGIT: [0-7];
+
+fragment HEXADECIMALDIGIT: [0-9a-fA-F];
+
+fragment BINARYDIGIT: [01];
+
+Integersuffix:
+	Unsignedsuffix Longsuffix?
+	| Unsignedsuffix Longlongsuffix?
+	| Longsuffix Unsignedsuffix?
+	| Longlongsuffix Unsignedsuffix?;
+
+fragment Unsignedsuffix: [uU];
+
+fragment Longsuffix: [lL];
+
+fragment Longlongsuffix: 'll' | 'LL';
+
+fragment Cchar:
+	~ ['\\\r\n]
+	| Escapesequence
+	| Universalcharactername;
+
+fragment Escapesequence:
+	Simpleescapesequence
+	| Octalescapesequence
+	| Hexadecimalescapesequence;
+
+fragment Simpleescapesequence:
+	'\\\''
+	| '\\"'
+	| '\\?'
+	| '\\\\'
+	| '\\a'
+	| '\\b'
+	| '\\f'
+	| '\\n'
+	| '\\r'
+	| ('\\' ('\r' '\n'? | '\n'))
+	| '\\t'
+	| '\\v';
+
+fragment Octalescapesequence:
+	'\\' OCTALDIGIT
+	| '\\' OCTALDIGIT OCTALDIGIT
+	| '\\' OCTALDIGIT OCTALDIGIT OCTALDIGIT;
+
+fragment Hexadecimalescapesequence: '\\x' HEXADECIMALDIGIT+;
+
+fragment Fractionalconstant:
+	Digitsequence? '.' Digitsequence
+	| Digitsequence '.';
+
+fragment Exponentpart:
+	'e' SIGN? Digitsequence
+	| 'E' SIGN? Digitsequence;
+
+fragment SIGN: [+-];
+
+fragment Digitsequence: DIGIT ('\''? DIGIT)*;
+
+fragment Floatingsuffix: [flFL];
+
+fragment Encodingprefix: 'u8' | 'u' | 'U' | 'L';
+
+fragment Schar:
+	~ ["\\\r\n]
+	| Escapesequence
+	| Universalcharactername;
+
+fragment Rawstring: 'R"' (( '\\' ["()] )|~[\r\n (])*? '(' ~[)]*? ')'  (( '\\' ["()]) | ~[\r\n "])*? '"';
+
+UserDefinedIntegerLiteral:
+	DecimalLiteral Udsuffix
+	| OctalLiteral Udsuffix
+	| HexadecimalLiteral Udsuffix
+	| BinaryLiteral Udsuffix;
+
+UserDefinedFloatingLiteral:
+	Fractionalconstant Exponentpart? Udsuffix
+	| Digitsequence Exponentpart Udsuffix;
+
+UserDefinedStringLiteral: StringLiteral Udsuffix;
+
+UserDefinedCharacterLiteral: CharacterLiteral Udsuffix;
+
+fragment Udsuffix: Identifier;
+
+BlockStartSpecImmediate: '/*' [ \t\u000C]* '@' {inBlockSpec = true;};
+
+BlockCommentStart: '/*' -> mode(COMMENT), skip;
+
+LineCommentStart: '//' -> mode(LINE_COMMENT), skip;
+
+EndSpec:
+    '@'? '*/' {inBlockSpec}? {inBlockSpec = false;}
+    | ('\n'|'\r\n') {inLineSpec}? {inLineSpec = false;};
+
+Whitespace: [ \t]+ -> skip;
+
+Newline: ('\r' '\n'? | '\n') -> skip;
+
+
+mode DEFAULT_MODE;
+Identifier: Identifiernondigit (Identifiernondigit | DIGIT)*;
+
+ExtraAt: ('\n'|'\r\n') [ \t\u000C]* '@' {inBlockSpec}? -> skip;
+
+mode COMMENT;
+BlockCommentStop: '*/' -> mode(DEFAULT_MODE), skip;
+BlockStartSpec: ('\n'|'\r\n') [ \t\u000C]* '@' {inBlockSpec = true;} -> mode(DEFAULT_MODE);
+BlockCommentContent: .+? -> skip;
+
+mode LINE_COMMENT;
+LineCommentStop: ('\n'|'\r\n') -> mode(DEFAULT_MODE), skip;
+LineStartSpec: '@' {inLineSpec = true;} -> mode(DEFAULT_MODE);
+LineCommentContent: .+? -> skip;
\ No newline at end of file
diff --git a/src/parsers/antlr4/LangCPPParser.g4 b/src/parsers/antlr4/LangCPPParser.g4
new file mode 100644
index 0000000000..b6a2ab4328
--- /dev/null
+++ b/src/parsers/antlr4/LangCPPParser.g4
@@ -0,0 +1,906 @@
+/*******************************************************************************
+ * The MIT License (MIT)
+ *
+ * Copyright (c) 2015 Camilo Sanchez (Camiloasc1) 2020 Martin Mirchev (Marti2203)
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+ * associated documentation files (the "Software"), to deal in the Software without restriction,
+ * including without limitation the rights to use, copy, modify, merge, publish, distribute,
+ * sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all copies or
+ * substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+ * NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+ * DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ * ****************************************************************************
+ */
+
+// Grammar for C++ 14
+parser grammar LangCPPParser;
+
+// Root
+translationUnit: declarationseq? EOF;
+
+// Identifiers
+clangppIdentifier:
+    Identifier
+    | valIdentifier;
+
+// Expressions
+primaryExpression:
+    valExpr
+	| literal+
+	| This
+	| LeftParen expression RightParen
+	| idExpression
+	| lambdaExpression;
+
+annotatedPrimaryExpression: valEmbedWith? primaryExpression valEmbedThen?;
+
+idExpression: unqualifiedId | qualifiedId;
+
+unqualifiedId:
+	clangppIdentifier
+	| operatorFunctionId
+	| conversionFunctionId
+	| literalOperatorId
+	| Tilde (className | decltypeSpecifier)
+	| templateId;
+
+qualifiedId: nestedNameSpecifier Template? unqualifiedId;
+
+nestedNameSpecifier:
+	theTypeName Doublecolon
+	| namespaceName Doublecolon
+	| decltypeSpecifier Doublecolon
+	| Doublecolon
+	| nestedNameSpecifier clangppIdentifier Doublecolon
+	| nestedNameSpecifier Template? simpleTemplateId Doublecolon;
+
+lambdaExpression:
+	lambdaIntroducer lambdaDeclarator? compoundStatement;
+
+lambdaIntroducer: LeftBracket lambdaCapture? RightBracket;
+
+lambdaCapture:
+	captureList
+	| captureDefault (Comma captureList)?;
+
+captureDefault: And | Assign;
+
+captureList: capture (Comma capture)* Ellipsis?;
+
+capture: simpleCapture | initcapture;
+
+simpleCapture: And? clangppIdentifier | This;
+
+initcapture: And? clangppIdentifier initializer;
+
+lambdaDeclarator:
+	LeftParen parameterDeclarationClause? RightParen Mutable? exceptionSpecification?
+		attributeSpecifierSeq? trailingReturnType?;
+
+postfixExpression:
+	annotatedPrimaryExpression
+	| postfixExpression LeftBracket expression RightBracket
+	| postfixExpression LeftBracket bracedInitList RightBracket
+	| postfixExpression LeftParen expressionList? RightParen valEmbedGiven? valEmbedYields?
+	| postfixExpression Dot Template? idExpression
+	| postfixExpression Dot pseudoDestructorName
+	| postfixExpression Arrow Template? idExpression
+	| postfixExpression Arrow pseudoDestructorName
+	| postfixExpression PlusPlus
+	| postfixExpression MinusMinus
+	| postfixExpression specPostfix
+	| simpleTypeSpecifier LeftParen expressionList? RightParen valEmbedGiven? valEmbedYields?
+	| simpleTypeSpecifier bracedInitList
+	| typeNameSpecifier LeftParen expressionList? RightParen valEmbedGiven? valEmbedYields?
+	| typeNameSpecifier bracedInitList
+	| (
+		Dynamic_cast
+		| Static_cast
+		| Reinterpret_cast
+		| Const_cast
+	) Less theTypeId Greater LeftParen expression RightParen
+	| typeIdOfTheTypeId LeftParen (expression | theTypeId) RightParen;
+
+specPostfix: {specLevel>0}? valPostfix;
+
+/*
+ add a middle layer to eliminate duplicated function declarations
+ */
+
+typeIdOfTheTypeId: Typeid_;
+
+expressionList: initializerList;
+
+pseudoDestructorName:
+	nestedNameSpecifier? (theTypeName Doublecolon)? Tilde theTypeName
+	| nestedNameSpecifier Template simpleTemplateId Doublecolon Tilde theTypeName
+	| Tilde decltypeSpecifier;
+
+unaryExpression:
+	postfixExpression
+	| PlusPlus unaryExpression
+	| MinusMinus unaryExpression
+	| unaryOperator unaryExpression
+	| Sizeof unaryExpression
+	| Sizeof (
+		LeftParen theTypeId RightParen
+		| Ellipsis LeftParen clangppIdentifier RightParen
+	)
+	| Alignof LeftParen theTypeId RightParen
+	| noExceptExpression
+	| newExpression
+	| deleteExpression
+	| specPrefix unaryExpression;
+
+specPrefix: {specLevel>0}? valPrefix;
+
+unaryOperator: And | Star | Plus | Minus | Tilde | Not | NotWord;
+
+newExpression:
+	Doublecolon? New newPlacement? newTypePtr newInitializer? valEmbedGiven? valEmbedYields?;
+
+newPlacement: LeftParen expressionList RightParen;
+
+newTypePtr:
+    newTypeId
+	| LeftParen theTypeId RightParen;
+
+newTypeId: typeSpecifierSeq newDeclarator?;
+
+newDeclarator:
+	pointerOperator newDeclarator?
+	| noPointerNewDeclarator;
+
+noPointerNewDeclarator:
+	LeftBracket expression RightBracket attributeSpecifierSeq?
+	| noPointerNewDeclarator LeftBracket constantExpression RightBracket attributeSpecifierSeq?;
+
+newInitializer:
+	LeftParen expressionList? RightParen
+	| bracedInitList;
+
+deleteExpression:
+	Doublecolon? Delete (LeftBracket RightBracket)? castExpression;
+
+noExceptExpression: Noexcept LeftParen expression RightParen;
+
+castExpression:
+	unaryExpression
+	| LeftParen theTypeId RightParen castExpression;
+
+pointerMemberExpression:
+    prependExpression
+	| pointerMemberExpression DotStar prependExpression
+	| pointerMemberExpression ArrowStar prependExpression;
+
+prependExpression:
+		castExpression
+    | castExpression prependOp prependExpression;
+
+prependOp: {specLevel>0}? valPrependOp;
+
+multiplicativeExpression:
+    pointerMemberExpression
+	| multiplicativeExpression multiplicativeOp pointerMemberExpression;
+
+multiplicativeOp:
+    Star
+    | Div
+    | Mod
+    | {specLevel>0}? valMulOp;
+
+additiveExpression:
+    multiplicativeExpression
+	| additiveExpression Plus multiplicativeExpression
+	| additiveExpression Minus multiplicativeExpression;
+
+shiftExpression:
+	additiveExpression
+	| shiftExpression Less Less additiveExpression
+	| shiftExpression Greater Greater additiveExpression;
+
+relationalExpression:
+    shiftExpression
+    | relationalExpression relationalOp shiftExpression;
+
+relationalOp:
+    (Less | Greater | LessEqual | GreaterEqual)
+    |   {specLevel>0}? valInOp;
+
+equalityExpression:
+	relationalExpression
+	| equalityExpression Equal relationalExpression
+	| equalityExpression NotEqual relationalExpression;
+
+andExpression:
+    equalityExpression
+    | andExpression And equalityExpression;
+
+exclusiveOrExpression:
+    andExpression
+    | exclusiveOrExpression Caret andExpression;
+
+inclusiveOrExpression:
+    exclusiveOrExpression
+    | inclusiveOrExpression Or exclusiveOrExpression;
+
+logicalAndExpression:
+    inclusiveOrExpression
+    | logicalAndExpression logicalAndOp inclusiveOrExpression;
+
+logicalAndOp:
+    AndAnd
+    | {specLevel>0}? valAndOp;
+
+logicalOrExpression:
+	logicalAndExpression
+	| logicalOrExpression OrOr logicalAndExpression;
+
+implicationExpression:
+		logicalOrExpression
+    | logicalOrExpression implicationOp implicationExpression;
+
+implicationOp: {specLevel>0}? valImpOp;
+
+conditionalExpression:
+	implicationExpression
+	| implicationExpression Question expression Colon assignmentExpression;
+
+assignmentExpression:
+	valEmbedWith? conditionalExpression valEmbedThen?
+	| valEmbedWith? logicalOrExpression assignmentOperator initializerClause valEmbedThen?
+	| throwExpression;
+
+assignmentOperator:
+	Assign
+	| StarAssign
+	| DivAssign
+	| ModAssign
+	| PlusAssign
+	| MinusAssign
+	| RightShiftAssign
+	| LeftShiftAssign
+	| AndAssign
+	| XorAssign
+	| OrAssign;
+
+expression:
+    assignmentExpression
+    | expression Comma assignmentExpression;
+
+constantExpression: conditionalExpression;
+
+// Statements
+statement:
+    attributeSpecifierSeq? statementTwo
+	| labeledStatement
+	| blockDeclaration;
+
+statementTwo:
+    expressionStatement
+    | compoundStatement
+    | selectionStatement
+    | iterationStatement
+    | jumpStatement
+    | tryBlock
+    | valEmbedStatementBlock
+    | {specLevel>0}? valStatement;
+
+labeledStatement:
+	attributeSpecifierSeq? (
+		clangppIdentifier
+		| Case constantExpression
+		| Default
+	) Colon statement;
+
+expressionStatement: expression? Semi;
+
+compoundStatement: LeftBrace statementSeq? RightBrace;
+
+statementSeq: statement+;
+
+selectionStatement:
+	ifStatement
+	| switchStatement;
+
+ifStatement:
+	If LeftParen condition RightParen statement Else statement
+	| If LeftParen condition RightParen statement;
+
+switchStatement: Switch LeftParen condition RightParen statement;
+
+condition:
+	expression
+	| attributeSpecifierSeq? declSpecifierSeq declarator (
+		Assign initializerClause
+		| bracedInitList
+	);
+
+iterationStatement:
+	valEmbedContract? While LeftParen condition RightParen valEmbedContract? statement
+	| Do statement While LeftParen expression RightParen Semi
+	| valEmbedContract? For LeftParen forInitStatement condition? Semi expression? RightParen valEmbedContract? statement
+	| valEmbedContract? For LeftParen forRangeDeclaration Colon forRangeInitializer RightParen valEmbedContract? statement;
+
+forInitStatement: expressionStatement | simpleDeclaration;
+
+forRangeDeclaration:
+	attributeSpecifierSeq? declSpecifierSeq declarator;
+
+forRangeInitializer: expression | bracedInitList;
+
+jumpStatement:
+	Break Semi
+	| Continue Semi
+	| Return expression Semi
+	| Return bracedInitList Semi
+	| Return Semi
+	| Goto clangppIdentifier Semi;
+
+// Declarations
+declarationseq:
+	declaration Semi*
+	| declarationseq declaration Semi*;
+
+declaration:
+	functionDefinition
+	| blockDeclaration
+	| templateDeclaration
+	| explicitInstantiation
+	| explicitSpecialization
+	| linkageSpecification
+	| namespaceDefinition
+	| emptyDeclaration
+	| attributeDeclaration
+	| valEmbedGlobalDeclarationBlock;
+
+blockDeclaration:
+	simpleDeclaration
+	| asmDefinition
+	| namespaceAliasDefinition
+	| usingDeclaration
+	| usingDirective
+	| staticAssertDeclaration
+	| aliasDeclaration
+	| opaqueEnumDeclaration;
+
+aliasDeclaration:
+	Using clangppIdentifier attributeSpecifierSeq? Assign theTypeId Semi;
+
+simpleDeclaration:
+	valEmbedContract? declSpecifierSeq? initDeclaratorList? Semi
+	| valEmbedContract? attributeSpecifierSeq declSpecifierSeq? initDeclaratorList Semi;
+
+staticAssertDeclaration:
+	Static_assert LeftParen constantExpression Comma StringLiteral RightParen Semi;
+
+emptyDeclaration: Semi;
+
+attributeDeclaration: attributeSpecifierSeq Semi;
+
+declSpecifier:
+	storageClassSpecifier
+	| typeSpecifier
+	| functionSpecifier
+	| Friend
+	| Typedef
+	| Constexpr
+	| valEmbedModifier;
+
+declSpecifierSeq: declSpecifier+? attributeSpecifierSeq?;
+
+storageClassSpecifier:
+	Register
+	| Static
+	| Thread_local
+	| Extern
+	| Mutable;
+
+functionSpecifier: Inline | Virtual | Explicit;
+
+typedefName: clangppIdentifier;
+
+typeSpecifier:
+	trailingTypeSpecifier
+	| classSpecifier
+	| enumSpecifier;
+
+trailingTypeSpecifier:
+	simpleTypeSpecifier
+	| elaboratedTypeSpecifier
+	| typeNameSpecifier
+	| cvQualifier;
+
+typeSpecifierSeq: typeSpecifier+ attributeSpecifierSeq?;
+
+trailingTypeSpecifierSeq:
+	trailingTypeSpecifier+ attributeSpecifierSeq?;
+
+simpleTypeLengthModifier:
+	Short
+	| Long;
+
+simpleTypeSignednessModifier:
+	Unsigned
+	| Signed;
+
+simpleTypeSpecifier:
+	nestedNameSpecifier? theTypeName
+	| nestedNameSpecifier Template simpleTemplateId
+	| simpleTypeSignednessModifier
+	| simpleTypeSignednessModifier? simpleTypeLengthModifier+
+	| simpleTypeSignednessModifier? Char
+	| simpleTypeSignednessModifier? Char16
+	| simpleTypeSignednessModifier? Char32
+	| simpleTypeSignednessModifier? Wchar
+	| Bool
+	| simpleTypeSignednessModifier? simpleTypeLengthModifier* Int
+	| Float
+	| simpleTypeLengthModifier? Double
+	| Void
+	| SYCLQueue // EW: Will be moved to own SYCL Parser later
+	| Auto
+	| {specLevel>0}? valType
+	| decltypeSpecifier;
+
+theTypeName:
+	className
+	| enumName
+	| typedefName
+	| simpleTemplateId;
+
+decltypeSpecifier:
+	Decltype LeftParen (expression | Auto) RightParen;
+
+elaboratedTypeSpecifier:
+	classKey (
+		attributeSpecifierSeq? nestedNameSpecifier? clangppIdentifier
+		| simpleTemplateId
+		| nestedNameSpecifier Template? simpleTemplateId
+	)
+	| Enum nestedNameSpecifier? clangppIdentifier;
+
+enumName: clangppIdentifier;
+
+enumSpecifier:
+	enumHead LeftBrace (enumeratorList Comma?)? RightBrace;
+
+enumHead:
+	enumkey attributeSpecifierSeq? (
+		nestedNameSpecifier? clangppIdentifier
+	)? enumbase?;
+
+opaqueEnumDeclaration:
+	enumkey attributeSpecifierSeq? clangppIdentifier enumbase? Semi;
+
+enumkey: Enum (Class | Struct)?;
+
+enumbase: Colon typeSpecifierSeq;
+
+enumeratorList:
+	enumeratorDefinition (Comma enumeratorDefinition)*;
+
+enumeratorDefinition: enumerator (Assign constantExpression)?;
+
+enumerator: clangppIdentifier;
+
+namespaceName: originalNamespaceName | namespaceAlias;
+
+originalNamespaceName: clangppIdentifier;
+
+namespaceDefinition:
+	Inline? Namespace clangppIdentifier? LeftBrace declarationseq? RightBrace;
+
+namespaceAlias: clangppIdentifier;
+
+namespaceAliasDefinition:
+	Namespace clangppIdentifier Assign qualifiednamespacespecifier Semi;
+
+qualifiednamespacespecifier: nestedNameSpecifier? namespaceName;
+
+usingDeclaration:
+	Using ((Typename_? nestedNameSpecifier) | Doublecolon) unqualifiedId Semi;
+
+usingDirective:
+	attributeSpecifierSeq? Using Namespace nestedNameSpecifier? namespaceName Semi;
+
+asmDefinition: Asm LeftParen StringLiteral RightParen Semi;
+
+linkageSpecification:
+	Extern StringLiteral (
+		LeftBrace declarationseq? RightBrace
+		| declaration
+	);
+
+attributeSpecifierSeq: attributeSpecifier+;
+
+attributeSpecifier:
+	LeftBracket LeftBracket attributeList? RightBracket RightBracket
+	| alignmentspecifier;
+
+alignmentspecifier:
+	Alignas LeftParen (theTypeId | constantExpression) Ellipsis? RightParen;
+
+attributeList: attribute (Comma attribute)* Ellipsis?;
+
+attribute: (attributeNamespace Doublecolon)? clangppIdentifier attributeArgumentClause?;
+
+attributeNamespace: clangppIdentifier;
+
+attributeArgumentClause: LeftParen balancedTokenSeq? RightParen;
+
+balancedTokenSeq: balancedtoken+;
+
+balancedtoken:
+	LeftParen balancedTokenSeq RightParen
+	| LeftBracket balancedTokenSeq RightBracket
+	| LeftBrace balancedTokenSeq RightBrace
+	| ~(
+		LeftParen
+		| RightParen
+		| LeftBrace
+		| RightBrace
+		| LeftBracket
+		| RightBracket
+	)+;
+
+// Declarators
+initDeclaratorList:
+    initDeclarator
+    | initDeclaratorList Comma initDeclarator;
+
+initDeclarator: declarator initializer?;
+
+declarator:
+	pointerDeclarator
+	| noPointerDeclarator parametersAndQualifiers trailingReturnType;
+
+pointerDeclarator: pointerDeclaratorPrefix* noPointerDeclarator;
+
+pointerDeclaratorPrefix: pointerOperatorWithDoubleStar Const?;
+
+noPointerDeclarator:
+	declaratorid attributeSpecifierSeq?
+	| noPointerDeclarator parametersAndQualifiers
+	| noPointerDeclarator LeftBracket constantExpression? RightBracket attributeSpecifierSeq?
+	| LeftParen pointerDeclarator RightParen;
+
+parametersAndQualifiers:
+	LeftParen parameterDeclarationClause? RightParen cvqualifierseq? refqualifier?
+		exceptionSpecification? attributeSpecifierSeq?;
+
+trailingReturnType:
+	Arrow trailingTypeSpecifierSeq abstractDeclarator?;
+
+pointerOperator:
+	And attributeSpecifierSeq?
+	| AndAnd attributeSpecifierSeq?
+	| nestedNameSpecifier? Star attributeSpecifierSeq? cvqualifierseq?;
+
+// ** is tokenized separately as separating conjunction,
+// so add special case where ** can be used, which is when
+// multiple pointerOperators are allowed to be repeated after each other
+pointerOperatorWithDoubleStar:
+    pointerOperator
+    | nestedNameSpecifier? SEP_CONJ attributeSpecifierSeq? cvqualifierseq?;
+
+cvqualifierseq: cvQualifier+;
+
+cvQualifier: Const | Volatile;
+
+refqualifier: And | AndAnd;
+
+declaratorid: Ellipsis? idExpression;
+
+theTypeId: typeSpecifierSeq abstractDeclarator?;
+
+abstractDeclarator:
+	pointerAbstractDeclarator
+	| noPointerAbstractDeclarator? parametersAndQualifiers trailingReturnType
+	| abstractPackDeclarator;
+
+pointerAbstractDeclarator:
+	noPointerAbstractDeclarator
+	| pointerOperatorWithDoubleStar+ noPointerAbstractDeclarator?;
+
+noPointerAbstractDeclarator:
+	noPointerAbstractDeclarator (
+		parametersAndQualifiers
+		| noPointerAbstractDeclarator LeftBracket constantExpression? RightBracket
+			attributeSpecifierSeq?
+	)
+	| parametersAndQualifiers
+	| LeftBracket constantExpression? RightBracket attributeSpecifierSeq?
+	| LeftParen pointerAbstractDeclarator RightParen;
+
+abstractPackDeclarator:
+	pointerOperatorWithDoubleStar* noPointerAbstractPackDeclarator;
+
+noPointerAbstractPackDeclarator:
+	noPointerAbstractPackDeclarator (
+		parametersAndQualifiers
+		| LeftBracket constantExpression? RightBracket attributeSpecifierSeq?
+	)
+	| Ellipsis;
+
+parameterDeclarationClause:
+	parameterDeclarationList parameterDeclarationVarargs?;
+
+parameterDeclarationVarargs: Comma? Ellipsis;
+
+parameterDeclarationList:
+	parameterDeclaration (Comma parameterDeclaration)*;
+
+parameterDeclaration:
+    declSpecifierSeq declarator
+	| attributeSpecifierSeq? declSpecifierSeq (
+		(declarator | abstractDeclarator?) (
+			Assign initializerClause
+		)?
+	);
+
+functionDefinition:
+	valEmbedContract? attributeSpecifierSeq? declSpecifierSeq? declarator virtualSpecifierSeq? functionBody;
+
+functionBody:
+	constructorInitializer? compoundStatement
+	| functionTryBlock
+	| Assign (Default | Delete) Semi;
+
+initializer:
+	braceOrEqualInitializer
+	| LeftParen expressionList RightParen;
+
+braceOrEqualInitializer:
+	Assign initializerClause
+	| bracedInitList;
+
+// EW: Had to flip the two options to not get parsing errors
+initializerClause: bracedInitList | assignmentExpression;
+
+initializerList:
+	initializerClause Ellipsis?
+	| initializerList Comma initializerClause Ellipsis?;
+
+bracedInitList:
+    LeftBrace RightBrace
+    | LeftBrace initializerList RightBrace
+    | LeftBrace initializerList Comma RightBrace;
+
+// Classes
+className: clangppIdentifier | simpleTemplateId;
+
+classSpecifier:
+	classHead LeftBrace memberSpecification? RightBrace;
+
+classHead:
+	classKey attributeSpecifierSeq? (
+		classHeadName classVirtSpecifier?
+	)? baseClause?
+	| Union attributeSpecifierSeq? (
+		classHeadName classVirtSpecifier?
+	)?;
+
+classHeadName: nestedNameSpecifier? className;
+
+classVirtSpecifier: Final;
+
+classKey: Class | Struct;
+
+memberSpecification:
+	(memberdeclaration | accessSpecifier Colon)+;
+
+memberdeclaration:
+	attributeSpecifierSeq? declSpecifierSeq? memberDeclaratorList? Semi
+	| functionDefinition
+	| usingDeclaration
+	| staticAssertDeclaration
+	| templateDeclaration
+	| aliasDeclaration
+	| emptyDeclaration;
+
+memberDeclaratorList:
+	memberDeclarator (Comma memberDeclarator)*;
+
+memberDeclarator:
+	declarator (
+		virtualSpecifierSeq? pureSpecifier?
+		| braceOrEqualInitializer?
+	)
+	| clangppIdentifier? attributeSpecifierSeq? Colon constantExpression;
+
+virtualSpecifierSeq: virtualSpecifier+;
+
+virtualSpecifier: Override | Final;
+/*
+ purespecifier: Assign '0'//Conflicts with the lexer ;
+ */
+
+pureSpecifier:
+	Assign val = OctalLiteral {if($val.text.compareTo("0")!=0) throw new InputMismatchException(this);
+		};
+
+//Derived classes
+baseClause: Colon baseSpecifierList;
+
+baseSpecifierList:
+	baseSpecifier Ellipsis? (Comma baseSpecifier Ellipsis?)*;
+
+baseSpecifier:
+	attributeSpecifierSeq? (
+		baseTypeSpecifier
+		| Virtual accessSpecifier? baseTypeSpecifier
+		| accessSpecifier Virtual? baseTypeSpecifier
+	);
+
+classOrDeclType:
+	nestedNameSpecifier? className
+	| decltypeSpecifier;
+
+baseTypeSpecifier: classOrDeclType;
+
+accessSpecifier: Private | Protected | Public;
+
+// Special member functions
+conversionFunctionId: Operator conversionTypeId;
+
+conversionTypeId: typeSpecifierSeq conversionDeclarator?;
+
+conversionDeclarator: pointerOperator conversionDeclarator?;
+
+constructorInitializer: Colon memInitializerList;
+
+memInitializerList:
+	memInitializer Ellipsis? (Comma memInitializer Ellipsis?)*;
+
+memInitializer:
+	meminitializerid (
+		LeftParen expressionList? RightParen
+		| bracedInitList
+	);
+
+meminitializerid: classOrDeclType | clangppIdentifier;
+
+// Overloading
+operatorFunctionId: Operator theOperator;
+
+literalOperatorId:
+	Operator (
+		StringLiteral clangppIdentifier
+		| UserDefinedStringLiteral
+	);
+
+// Templates
+templateDeclaration:
+	Template Less templateparameterList Greater declaration;
+
+templateparameterList:
+	templateParameter (Comma templateParameter)*;
+
+templateParameter: typeParameter | parameterDeclaration;
+
+typeParameter:
+	(
+		(Template Less templateparameterList Greater)? Class
+		| Typename_
+	) ((Ellipsis? clangppIdentifier?) | (clangppIdentifier? Assign theTypeId));
+
+simpleTemplateId:
+	templateName Less templateArgumentList? Greater;
+
+templateId:
+	simpleTemplateId
+	| (operatorFunctionId | literalOperatorId) Less templateArgumentList? Greater;
+
+templateName: clangppIdentifier;
+
+templateArgumentList:
+	templateArgument Ellipsis? (Comma templateArgument Ellipsis?)*;
+
+templateArgument: theTypeId | constantExpression | idExpression;
+
+typeNameSpecifier:
+	Typename_ nestedNameSpecifier (
+		clangppIdentifier
+		| Template? simpleTemplateId
+	);
+
+explicitInstantiation: Extern? Template declaration;
+
+explicitSpecialization: Template Less Greater declaration;
+
+// Exception handling
+tryBlock: Try compoundStatement handlerSeq;
+
+functionTryBlock:
+	Try constructorInitializer? compoundStatement handlerSeq;
+
+handlerSeq: handler+;
+
+handler:
+	Catch LeftParen exceptionDeclaration RightParen compoundStatement;
+
+exceptionDeclaration:
+	attributeSpecifierSeq? typeSpecifierSeq (
+		declarator
+		| abstractDeclarator
+	)?
+	| Ellipsis;
+
+throwExpression: Throw assignmentExpression?;
+
+exceptionSpecification:
+	dynamicExceptionSpecification
+	| noeExceptSpecification;
+
+dynamicExceptionSpecification:
+	Throw LeftParen typeIdList? RightParen;
+
+typeIdList: theTypeId Ellipsis? (Comma theTypeId Ellipsis?)*;
+
+noeExceptSpecification:
+	Noexcept LeftParen constantExpression RightParen
+	| Noexcept;
+
+// Preprocessing directives
+
+// Lexer
+theOperator:
+	New (LeftBracket RightBracket)?
+	| Delete (LeftBracket RightBracket)?
+	| Plus
+	| Minus
+	| Star
+	| Div
+	| Mod
+	| Caret
+	| And
+	| Or
+	| Tilde
+	| Not
+	| NotWord
+	| Assign
+	| Greater
+	| Less
+	| GreaterEqual
+	| PlusAssign
+	| MinusAssign
+	| StarAssign
+	| ModAssign
+	| XorAssign
+	| AndAssign
+	| OrAssign
+	| Less Less
+	| Greater Greater
+	| RightShiftAssign
+	| LeftShiftAssign
+	| Equal
+	| NotEqual
+	| LessEqual
+	| AndAnd
+	| OrOr
+	| PlusPlus
+	| MinusMinus
+	| Comma
+	| ArrowStar
+	| Arrow
+	| LeftParen RightParen
+	| LeftBracket RightBracket;
+
+literal:
+	IntegerLiteral
+	| CharacterLiteral
+	| FloatingLiteral
+	| StringLiteral
+	| BooleanLiteral
+	| PointerLiteral
+	| UserDefinedLiteral;
+
diff --git a/src/parsers/antlr4/LangJavaLexer.g4 b/src/parsers/antlr4/LangJavaLexer.g4
index 4e93b3eda8..d927f62ff9 100644
--- a/src/parsers/antlr4/LangJavaLexer.g4
+++ b/src/parsers/antlr4/LangJavaLexer.g4
@@ -17,6 +17,7 @@ VAL_ASSERT    : EOF EOF;
 VAL_TRUE      : EOF EOF;
 VAL_FALSE     : EOF EOF;
 VAL_SIZEOF    : 'sizeof';
+CONS          : '::';
 
 // §3.9 Keywords
 
diff --git a/src/parsers/antlr4/LangLLVMSpecLexer.g4 b/src/parsers/antlr4/LangLLVMSpecLexer.g4
index 8cf5e74cd0..ace814dbbd 100644
--- a/src/parsers/antlr4/LangLLVMSpecLexer.g4
+++ b/src/parsers/antlr4/LangLLVMSpecLexer.g4
@@ -27,6 +27,7 @@ COLON: ':';
 VAL_INLINE: 'inline';
 VAL_ASSERT: 'assert';
 VAL_PACKAGE: 'package';
+CONS: '::';
 
 INC: '++';
 ARROW: '->';
diff --git a/src/parsers/antlr4/SpecLexer.g4 b/src/parsers/antlr4/SpecLexer.g4
index 24cf7ab69b..83fac3a509 100644
--- a/src/parsers/antlr4/SpecLexer.g4
+++ b/src/parsers/antlr4/SpecLexer.g4
@@ -21,6 +21,7 @@ STAR: '*';
 PIPE: '|';
 PLUS: '+';
 COLON: ':';
+CONS: '::';
 VAL_INLINE: 'inline';
 VAL_ASSERT: 'assert';
 VAL_TRUE: 'true';
@@ -173,7 +174,6 @@ READ: 'read';
 EMPTY: 'empty';
 
 COALESCE: '?.';
-CONS: '::';
 FRAC_DIV: '\\';
 SEP_CONJ: '**';
 IMPLIES: '==>';
diff --git a/src/parsers/vct/parsers/ColCPPParser.scala b/src/parsers/vct/parsers/ColCPPParser.scala
new file mode 100644
index 0000000000..05b79561ff
--- /dev/null
+++ b/src/parsers/vct/parsers/ColCPPParser.scala
@@ -0,0 +1,86 @@
+package vct.parsers
+
+import com.typesafe.scalalogging.LazyLogging
+import hre.io.{RWFile, Readable}
+import org.antlr.v4.runtime.CharStream
+import vct.parsers.CParser.PreprocessorError
+import vct.parsers.transform.{BlameProvider, InterpretedFileOriginProvider, OriginProvider}
+import vct.result.VerificationError.{Unreachable, UserError}
+
+import java.io._
+import java.nio.charset.StandardCharsets
+import java.nio.file.{Path, Paths}
+
+case object CPPParser {
+  case class PreprocessorError(fileName: String, errorCode: Int, error: String) extends UserError {
+    override def code: String = "preprocessorError"
+    override def text: String =
+      s"Preprocesing file $fileName failed with exit code $errorCode:\n$error"
+  }
+}
+
+case class ColCPPParser(override val originProvider: OriginProvider,
+                      override val blameProvider: BlameProvider,
+                      cc: Path,
+                      systemInclude: Path,
+                      otherIncludes: Seq[Path],
+                      defines: Map[String, String]) extends Parser(originProvider, blameProvider) with LazyLogging {
+
+  def interpret(localInclude: Seq[Path], input: String, output: String): Process = {
+    var command = Seq(cc.toString, "-C", "-E")
+
+    command ++= Seq("-nostdinc")
+    command ++= Seq("-isystem", systemInclude.toAbsolutePath.toString)
+
+    command ++= localInclude.map("-I" + _.toAbsolutePath)
+    command ++= otherIncludes.map("-I" + _.toAbsolutePath.toString)
+    command ++= defines.map { case (k, v) => s"-D$k=$v" }
+    command ++= Seq("-o", output)
+    command :+= input
+
+    logger.debug(command.toString())
+
+    new ProcessBuilder(command:_*).start()
+  }
+
+  override def parse[G](stream: CharStream): ParseResult[G] = {
+    throw Unreachable("Should not parse C++ files from an ANTLR CharStream: they need to be interpreted first!")
+  }
+
+  override def parse[G](readable: Readable): ParseResult[G] =
+    try {
+      val interpreted = File.createTempFile("vercors-interpreted-", ".ipp")
+      interpreted.deleteOnExit()
+
+      val process = interpret(
+        localInclude=Option(Paths.get(readable.fileName).getParent).toSeq,
+        input="-",
+        output=interpreted.toString
+      )
+      new Thread(() => {
+        val writer = new OutputStreamWriter(process.getOutputStream, StandardCharsets.UTF_8)
+        try {
+          readable.read { reader =>
+            val written = reader.transferTo(writer)
+            logger.debug(s"Wrote $written bytes to clang++")
+          }
+        } finally {
+          writer.close()
+        }
+      }).start()
+      process.waitFor()
+
+      if(process.exitValue() != 0) {
+        val writer = new StringWriter()
+        new InputStreamReader(process.getInputStream).transferTo(writer)
+        new InputStreamReader(process.getErrorStream).transferTo(writer)
+        writer.close()
+        throw PreprocessorError(readable.fileName, process.exitValue(), writer.toString)
+      }
+
+      val result = ColIPPParser(InterpretedFileOriginProvider(originProvider, RWFile(interpreted)), blameProvider).parse[G](RWFile(interpreted))
+      result
+    } catch {
+      case _: FileNotFoundException => throw FileNotFound(readable.fileName)
+    }
+}
diff --git a/src/parsers/vct/parsers/ColIPPParser.scala b/src/parsers/vct/parsers/ColIPPParser.scala
new file mode 100644
index 0000000000..c73bb21f13
--- /dev/null
+++ b/src/parsers/vct/parsers/ColIPPParser.scala
@@ -0,0 +1,29 @@
+package vct.parsers
+
+import org.antlr.v4.runtime.{CharStream, CommonTokenStream}
+import vct.antlr4.generated.{CPPParser, LangCPPLexer}
+import vct.parsers.transform.{BlameProvider, CPPToCol, OriginProvider}
+
+case class ColIPPParser(override val originProvider: OriginProvider, override val blameProvider: BlameProvider) extends Parser(originProvider, blameProvider) {
+
+  override def parse[G](stream: CharStream): ParseResult[G] = {
+    try {
+      val lexer = new LangCPPLexer(stream)
+      val tokens = new CommonTokenStream(lexer)
+      originProvider.setTokenStream(tokens)
+      val parser = new CPPParser(tokens)
+
+      val (errors, tree) = noErrorsOrThrow(parser, lexer, originProvider) {
+        val errors = expectedErrors(tokens, LangCPPLexer.EXPECTED_ERROR_CHANNEL, LangCPPLexer.VAL_EXPECT_ERROR_OPEN, LangCPPLexer.VAL_EXPECT_ERROR_CLOSE)
+        val tree = parser.translationUnit()
+        (errors, tree)
+      }
+
+      val decls = CPPToCol[G](originProvider, blameProvider, errors).convert(tree)
+      ParseResult(decls, errors.map(_._3))
+    } catch {
+      case m: MatchError =>
+        throw ParseMatchError(m.getMessage())
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/parsers/vct/parsers/ColIParser.scala b/src/parsers/vct/parsers/ColIParser.scala
index 72bc794f40..86ab58c4bc 100644
--- a/src/parsers/vct/parsers/ColIParser.scala
+++ b/src/parsers/vct/parsers/ColIParser.scala
@@ -2,7 +2,6 @@ package vct.parsers
 
 import org.antlr.v4.runtime.{CharStream, CommonTokenStream}
 import vct.antlr4.generated.{CParser, LangCLexer}
-import vct.col.ast.GlobalDeclaration
 import vct.parsers.transform.{BlameProvider, CToCol, OriginProvider}
 
 case class ColIParser(override val originProvider: OriginProvider, override val blameProvider: BlameProvider) extends Parser(originProvider, blameProvider) {
diff --git a/src/parsers/vct/parsers/transform/CPPToCol.scala b/src/parsers/vct/parsers/transform/CPPToCol.scala
new file mode 100644
index 0000000000..ab1769b90b
--- /dev/null
+++ b/src/parsers/vct/parsers/transform/CPPToCol.scala
@@ -0,0 +1,1312 @@
+package vct.parsers.transform
+
+import org.antlr.v4.runtime.{ParserRuleContext, Token}
+import vct.antlr4.generated.CPPParser._
+import vct.antlr4.generated.CPPParserPatterns._
+import vct.col.ast._
+import vct.col.ast.`type`.TFloats
+import vct.col.origin._
+import vct.col.ref.{Ref, UnresolvedRef}
+import vct.col.util.AstBuildHelpers
+import vct.col.util.AstBuildHelpers._
+import vct.col.{ast => col}
+
+import scala.annotation.nowarn
+import scala.jdk.CollectionConverters._
+
+@nowarn("msg=match may not be exhaustive&msg=Some\\(")
+case class CPPToCol[G](override val originProvider: OriginProvider, override val blameProvider: BlameProvider, override val errors: Seq[(Token, Token, ExpectedError)])
+  extends ToCol(originProvider, blameProvider, errors) {
+
+  def convert(implicit unit: TranslationUnitContext): Seq[GlobalDeclaration[G]] = unit match {
+    case TranslationUnit0(maybeDeclSeq, _) => Seq(new CPPTranslationUnit(maybeDeclSeq.toSeq.flatMap(convert(_))))
+  }
+
+  def convert(implicit declSeq: DeclarationseqContext): Seq[GlobalDeclaration[G]] = declSeq match {
+    case Declarationseq0(decl, _) => convert(decl)
+    case Declarationseq1(declSeq, decl, _) => convert(declSeq) ++ convert(decl)
+  }
+
+  // Only support block declarations, function declarations, namespace declarations, empty declarations, and VerCors global declarations
+  def convert(implicit decl: DeclarationContext): Seq[GlobalDeclaration[G]] = decl match {
+    case Declaration0(funcDecl) => Seq(convert(funcDecl))
+    case Declaration1(blockDecl) => Seq(new CPPGlobalDeclaration(convert(blockDecl)))
+    case Declaration6(namespaceDecl) => Seq(convert(namespaceDecl))
+    case Declaration7(_) => Seq()
+    case Declaration9(globalSpecDecl) => convert(globalSpecDecl)
+    case x => ??(x)
+  }
+
+  // Do not support inline and unnamed namespaces
+  def convert(implicit nsDef: NamespaceDefinitionContext): CPPNamespaceDefinition[G] = nsDef match {
+    case NamespaceDefinition0(None, _, Some(name), _, maybeBody, _) => new CPPNamespaceDefinition(convert(name), maybeBody.toSeq.flatMap(convert(_)))
+    case x => ??(x)
+  }
+
+  // Not supporting attribute specifiers and virtual specifiers
+  def convert(implicit funcDef: FunctionDefinitionContext): CPPFunctionDefinition[G] = funcDef match {
+    case FunctionDefinition0(maybeContract, None, maybeDeclSpecs, declarator, None, body) =>
+      withContract(maybeContract, contract =>
+        new CPPFunctionDefinition(contract.consumeApplicableContract(blame(funcDef)), maybeDeclSpecs.toSeq.flatMap(convert(_)), convert(declarator), convert(body))(blame(funcDef))
+      )
+    case x => ??(x)
+  }
+
+  // Not supporting try blocks, '= default;', '= delete;', and constructor initializer ': name1, name2'
+  def convert(implicit funcBody: FunctionBodyContext): Statement[G] = funcBody match {
+    case FunctionBody0(None, compoundStmnt) => convert(compoundStmnt)
+    case x => ??(x)
+  }
+
+  def convert(implicit compoundStmnt: CompoundStatementContext): Statement[G] = compoundStmnt match {
+    case CompoundStatement0(_, None, _) => Scope(Nil, Block(Seq()))
+    case CompoundStatement0(_, Some(stmntSeq), _) => Scope(Nil, Block(convert(stmntSeq)))
+  }
+
+  def convert(implicit stmntSeq: StatementSeqContext): Seq[Statement[G]] = stmntSeq match {
+    case StatementSeq0(stmnts) => stmnts.map(convert(_))
+  }
+
+  // Do not support labeled statements and attribute specifiers before them
+  def convert(implicit stmnt: StatementContext): Statement[G] = stmnt match {
+    case Statement0(None, stmnt2) => convert(stmnt2)
+    case Statement2(blockDecl) => CPPDeclarationStatement(new CPPLocalDeclaration(convert(blockDecl)))
+    case x => ??(x)
+  }
+
+  // Do not support try blocks
+  def convert(implicit stmnt: StatementTwoContext): Statement[G] = stmnt match {
+    case StatementTwo0(exprStmnt) => convert(exprStmnt)
+    case StatementTwo1(compoundStmnt) => convert(compoundStmnt)
+    case StatementTwo2(selectionStmnt) => convert(selectionStmnt)
+    case StatementTwo3(iterStmnt) => convert(iterStmnt)
+    case StatementTwo4(jumpStmnt) => convert(jumpStmnt)
+    case StatementTwo6(embedStats) => convert(embedStats)
+    case StatementTwo7(embedStat) => convert(embedStat)
+    case x => ??(x)
+  }
+
+  // Do not support asm definitions, namespace alias definitions, using declarations and directives,
+  // static assert declarations, alias declarations, and opaque enum declarations
+  def convert(implicit blockDecl: BlockDeclarationContext): CPPDeclaration[G] = blockDecl match {
+    case BlockDeclaration0(simpleDecl) => convert(simpleDecl)
+    case x => ??(x)
+  }
+
+  // Not supporting attribute specifiers
+  def convert(implicit simpleDecl: SimpleDeclarationContext): CPPDeclaration[G] = simpleDecl match {
+    case SimpleDeclaration0(maybeContract, Some(declSpecs), maybeInits, _) =>
+      withContract(maybeContract, contract =>
+        new CPPDeclaration[G](contract.consumeApplicableContract(blame(simpleDecl)),
+          specs = convert(declSpecs), inits = maybeInits.map(convert(_)) getOrElse Nil)
+      )
+    case x => ??(x)
+  }
+
+  def convert(implicit exprStmnt: ExpressionStatementContext): Statement[G] = exprStmnt match {
+    case ExpressionStatement0(None, _) => Block(Nil)
+    case ExpressionStatement0(Some(expr), _) => Eval(convert(expr))
+  }
+
+  def convert(implicit expr: ExpressionContext): Expr[G] = expr match {
+    case Expression0(inner) => convert(inner)
+    case Expression1(first, _, result) => With(Eval(convert(first)), convert(result))
+  }
+
+  // Do not support switch statement
+  def convert(implicit selectionStmnt: SelectionStatementContext): Statement[G] = selectionStmnt match {
+    case SelectionStatement0(ifStmnt) => convert(ifStmnt)
+    case x => ??(x)
+  }
+
+  def convert(implicit ifStmnt: IfStatementContext): Statement[G] = ifStmnt match {
+    case IfStatement0(_, _, cond, _, whenTrue, _, whenFalse) => Branch(Seq((convert(cond), convert(whenTrue)), (tt, convert(whenFalse))))
+    case IfStatement1(_, _, cond, _, whenTrue) => Branch(Seq((convert(cond), convert(whenTrue))))
+  }
+
+  // Do not support do-while loops, 'for(item : list) {}' and expression instead of declaration in a for-loop
+  def convert(implicit iterStmnt: IterationStatementContext): Statement[G] = iterStmnt match {
+    case IterationStatement0(contract1, _, _, cond, _, contract2, body) => withContract(contract1, contract2, c => {
+      Scope(Nil, Loop[G](Block(Nil), convert(cond), Block(Nil), c.consumeLoopContract(iterStmnt), convert(body)))
+    })
+    case IterationStatement1(_, _, _, _, _, _, _) => ??(iterStmnt)
+    case IterationStatement2(contract1, _, _, ForInitStatement1(simpleDecl), cond, _, update, _, contract2, body) =>
+      withContract(contract1, contract2, c => {
+        Scope(Nil, Loop[G](CPPDeclarationStatement(new CPPLocalDeclaration(convert(simpleDecl))), cond.map(convert(_)).getOrElse(tt), evalOrNop(update), c.consumeLoopContract(iterStmnt), convert(body)))
+      })
+    case x => ??(x)
+  }
+
+  // Do not support goto or return of a bracedInitList
+  def convert(implicit jumpStmnt: JumpStatementContext): Statement[G] = jumpStmnt match {
+    case JumpStatement0(_, _) => col.Break(None)
+    case JumpStatement1(_, _) => col.Continue(None)
+    case JumpStatement2(_, expr, _) => col.Return(convert(expr))
+    case JumpStatement4(_, _) => col.Return(col.Void())
+    case x => ??(x)
+  }
+
+  // Do not support assignments in condition
+  def convert(implicit cond: ConditionContext): Expr[G] = cond match {
+    case Condition0(expr) => convert(expr)
+    case x => ??(x)
+  }
+
+  // Do not support throw expression
+  def convert(implicit expr: AssignmentExpressionContext): Expr[G] = expr match {
+    case AssignmentExpression0(pre, inner, post) =>
+      convertEmbedWith(pre, convertEmbedThen(post, convert(inner)))
+    case AssignmentExpression1(pre, targetNode, op, valueNode, post) =>
+      val e = convert(op, targetNode, valueNode, expr)
+      convertEmbedWith(pre, convertEmbedThen(post, e))
+    case x => ??(x)
+  }
+
+  // Do not support bit operators
+  def convert(op: AssignmentOperatorContext, targetNode: LogicalOrExpressionContext, valueNode: InitializerClauseContext, expr: AssignmentExpressionContext)(implicit o: Origin): Expr[G] = {
+    val target = convert(targetNode)
+    val value = convert(valueNode)
+    PreAssignExpression(target, op match {
+      case AssignmentOperator0(_) => value
+      case AssignmentOperator1(_) => AmbiguousMult(target, value)
+      case AssignmentOperator2(_) => FloorDiv(target, value)(blame(expr))
+      case AssignmentOperator3(_) => col.Mod(target, value)(blame(expr))
+      case AssignmentOperator4(_) => col.AmbiguousPlus(target, value)(blame(valueNode))
+      case AssignmentOperator5(_) => col.AmbiguousMinus(target, value)(blame(valueNode))
+      case _ => ??(op)
+    })(blame(expr))
+  }
+
+  def convert(implicit expr: ConditionalExpressionContext): Expr[G] = expr match {
+    case ConditionalExpression0(inner) => convert(inner)
+    case ConditionalExpression1(cond, _, whenTrue, _, whenFalse) =>
+      Select(convert(cond), convert(whenTrue), convert(whenFalse))
+  }
+
+  def convert(implicit expr: ImplicationExpressionContext): Expr[G] = expr match {
+    case ImplicationExpression0(inner) => convert(inner)
+    case ImplicationExpression1(left, op, right) => convert(op, convert(left), convert(right))
+  }
+
+  def convert(op: ImplicationOpContext, left: Expr[G], right: Expr[G])(implicit o: Origin): Expr[G] = op match {
+    case ImplicationOp0(ValImpOp0(_)) => Wand(left, right)
+    case ImplicationOp0(ValImpOp1(_)) => Implies(left, right)
+  }
+
+  def convert(implicit expr: LogicalOrExpressionContext): Expr[G] = expr match {
+    case LogicalOrExpression0(inner) => convert(inner)
+    case LogicalOrExpression1(left, _, right) => AmbiguousOr(convert(left), convert(right))
+  }
+
+  def convert(implicit expr: LogicalAndExpressionContext): Expr[G] = expr match {
+    case LogicalAndExpression0(inner) => convert(inner)
+    case LogicalAndExpression1(left, op, right) => op match {
+      case LogicalAndOp0(_) => col.And(convert(left), convert(right))
+      case LogicalAndOp1(valOp) => convert(expr, valOp, convert(left), convert(right))
+    }
+  }
+
+  def convert(implicit expr: InclusiveOrExpressionContext): Expr[G] = expr match {
+    case InclusiveOrExpression0(inner) => convert(inner)
+    case InclusiveOrExpression1(left, _, right) => BitOr(convert(left), convert(right))
+  }
+
+  def convert(implicit expr: ExclusiveOrExpressionContext): Expr[G] = expr match {
+    case ExclusiveOrExpression0(inner) => convert(inner)
+    case ExclusiveOrExpression1(left, _, right) => BitXor(convert(left), convert(right))
+  }
+
+  def convert(implicit expr: AndExpressionContext): Expr[G] = expr match {
+    case AndExpression0(inner) => convert(inner)
+    case AndExpression1(left, _, right) => BitAnd(convert(left), convert(right))
+  }
+
+  def convert(implicit expr: EqualityExpressionContext): Expr[G] = expr match {
+    case EqualityExpression0(inner) => convert(inner)
+    case EqualityExpression1(left, _, right) => Eq(convert(left), convert(right))
+    case EqualityExpression2(left, _, right) => Neq(convert(left), convert(right))
+  }
+
+  def convert(implicit expr: RelationalExpressionContext): Expr[G] = expr match {
+    case RelationalExpression0(inner) => convert(inner)
+    case RelationalExpression1(left, RelationalOp0(op), right) => op match {
+      case "<" => col.AmbiguousLess(convert(left), convert(right))
+      case ">" => col.AmbiguousGreater(convert(left), convert(right))
+      case "<=" => AmbiguousLessEq(convert(left), convert(right))
+      case ">=" => AmbiguousGreaterEq(convert(left), convert(right))
+    }
+    case RelationalExpression1(left, RelationalOp1(specOp), right) =>
+      convert(expr, specOp, convert(left), convert(right))
+  }
+
+  def convert(implicit expr: ShiftExpressionContext): Expr[G] = expr match {
+    case ShiftExpression0(inner) => convert(inner)
+    case ShiftExpression1(left, _, _, right) => BitShl(convert(left), convert(right))
+    case ShiftExpression2(left, _, _, right) => BitShr(convert(left), convert(right))
+  }
+
+  def convert(implicit expr: AdditiveExpressionContext): Expr[G] = expr match {
+    case AdditiveExpression0(inner) => convert(inner)
+    case AdditiveExpression1(left, _, right) => AmbiguousPlus(convert(left), convert(right))(blame(expr))
+    case AdditiveExpression2(left, _, right) => col.AmbiguousMinus(convert(left), convert(right))(blame(expr))
+  }
+
+  def convert(implicit expr: MultiplicativeExpressionContext): Expr[G] = expr match {
+    case MultiplicativeExpression0(inner) => convert(inner)
+    case MultiplicativeExpression1(left, op, right) => op match {
+      case MultiplicativeOp0(_) => AmbiguousMult(convert(left), convert(right))
+      case MultiplicativeOp1(_) => FloorDiv(convert(left), convert(right))(blame(expr))
+      case MultiplicativeOp2(_) => col.Mod(convert(left), convert(right))(blame(expr))
+      case MultiplicativeOp3(_) => col.Div(convert(left), convert(right))(blame(expr))
+    }
+  }
+
+  // Do not support operators .* and ->*
+  def convert(implicit expr: PointerMemberExpressionContext): Expr[G] = expr match {
+    case PointerMemberExpression0(inner) => convert(inner)
+    case x => ??(x)
+  }
+
+  def convert(implicit expr: PrependExpressionContext): Expr[G] = expr match {
+    case PrependExpression0(inner) => convert(inner)
+    case PrependExpression1(left, PrependOp0(specOp), right) => convert(expr, specOp, convert(left), convert(right))
+  }
+
+  // Do not support cast expressions
+  def convert(expr: CastExpressionContext): Expr[G] = expr match {
+    case CastExpression0(inner) => convert(inner)
+    case CastExpression1(_, typeName, _, expr) => ??(expr)
+  }
+
+  // Do not support bracedInitList
+  def convert(implicit initClause: InitializerClauseContext): Expr[G] = initClause match {
+    case InitializerClause0(expr) => ??(expr)
+    case InitializerClause1(expr) => convert(expr)
+  }
+
+  // Do not support '...'
+  def convert(implicit expr: InitializerListContext): Seq[Expr[G]] = expr match {
+    case InitializerList0(initClause, None) => Seq(convert(initClause))
+    case InitializerList1(initList, _, initClause, None) => convert(initList) :+ convert(initClause)
+    case x => ??(x)
+  }
+
+  // Do not support sizeof, alignof, noexcept, and delete expressions
+  def convert(implicit expr: UnaryExpressionContext): Expr[G] = expr match {
+    case UnaryExpression0(inner) => convert(inner)
+    case UnaryExpression1(_, arg) =>
+      val target = convert(arg)
+      PreAssignExpression(target, col.AmbiguousPlus(target, const(1))(blame(expr)))(blame(expr))
+    case UnaryExpression2(_, arg) =>
+      val target = convert(arg)
+      PreAssignExpression(target, col.AmbiguousMinus(target, const(1))(blame(expr)))(blame(expr))
+    case UnaryExpression3(UnaryOperator0(_), arg) => AddrOf(convert(arg))
+    case UnaryExpression3(UnaryOperator1(_), arg) => DerefPointer(convert(arg))(blame(expr))
+    case UnaryExpression3(UnaryOperator2(_), arg) => convert(arg)
+    case UnaryExpression3(UnaryOperator3(_), arg) => UMinus(convert(arg))
+    case UnaryExpression3(UnaryOperator5(_), arg) => col.Not(convert(arg))
+    case UnaryExpression3(UnaryOperator6(_), arg) => col.Not(convert(arg))
+    case UnaryExpression8(expr) => ??(expr)
+    case UnaryExpression10(SpecPrefix0(op), inner) => convert(expr, op, convert(inner))
+    case x => ??(x)
+  }
+
+  def convert(implicit decls: InitDeclaratorListContext): Seq[CPPInit[G]] = decls match {
+    case InitDeclaratorList0(decl) => Seq(convert(decl))
+    case InitDeclaratorList1(init, _, last) => convert(init) :+ convert(last)
+  }
+
+  def convert(implicit decl: InitDeclaratorContext): CPPInit[G] = decl match {
+    case InitDeclarator0(inner, None) => CPPInit(convert(inner), None)
+    case InitDeclarator0(inner, Some(init)) => CPPInit(convert(inner), Some(convert(init)))
+  }
+
+  def convert(implicit expr: InitializerContext): Expr[G] = expr match {
+    case Initializer0(expr) => convert(expr)
+    case Initializer1(_, _, _) => ??(expr)
+  }
+
+  // Do not support bracedInitList
+  def convert(implicit expr: BraceOrEqualInitializerContext): Expr[G] = expr match {
+    case BraceOrEqualInitializer0(_, expr) => convert(expr)
+    case BraceOrEqualInitializer1(expr) => ??(expr)
+  }
+
+  // Do not support templactes, typeNameSpecifiers, bracedInitLists,
+  def convert(implicit expr: PostfixExpressionContext): Expr[G] = expr match {
+    case PostfixExpression0(inner) => convert(inner)
+    case PostfixExpression1(arr, _, idx, _) => AmbiguousSubscript(convert(arr), convert(idx))(blame(expr))
+    case PostfixExpression3(target, _, args, _, given, yields) =>
+      CPPInvocation(convert(target), args.map(convert(_)) getOrElse Nil,
+        convertEmbedGiven(given), convertEmbedYields(yields))(blame(expr))
+    case PostfixExpression4(classVar, _, None, idExpr) =>
+      convert(classVar) match {
+        case CPPLocal(className) => CPPLocal(className + "." + convert(idExpr).nestedName)(blame(expr))
+        case _ => ??(expr)
+      }
+    case PostfixExpression8(targetNode, _) =>
+      val target = convert(targetNode)
+      PostAssignExpression(target, col.AmbiguousPlus(target, const(1))(blame(expr)))(blame(expr))
+    case PostfixExpression9(targetNode, _) =>
+      val target = convert(targetNode)
+      PostAssignExpression(target, col.AmbiguousMinus(target, const(1))(blame(expr)))(blame(expr))
+    case PostfixExpression10(e, SpecPostfix0(postfix)) => convert(expr, postfix, convert(e))
+    case x => ??(x)
+  }
+
+  def convert(implicit exprList: ExpressionListContext): Seq[Expr[G]] = exprList match {
+    case ExpressionList0(initList) => convert(initList)
+  }
+
+  def convert(implicit expr: AnnotatedPrimaryExpressionContext): Expr[G] = expr match {
+    case AnnotatedPrimaryExpression0(pre, inner, post) =>
+      convertEmbedWith(pre, convertEmbedThen(post, convert(inner)))
+  }
+
+  // Dot not support lambdas, or more than 1 literal
+  def convert(implicit expr: PrimaryExpressionContext): Expr[G] = expr match {
+    case PrimaryExpression0(inner) => convert(inner)
+    case PrimaryExpression1(literals) if literals.length == 1 => convert(literals.head)
+    case PrimaryExpression2(_) => AmbiguousThis()
+    case PrimaryExpression3(_, inner, _) => convert(inner)
+    case PrimaryExpression4(inner) => CPPLocal(convert(inner).nestedName)(blame(expr))(origin(expr))
+    case x => ??(x)
+  }
+
+  // Do not support extended chars and strings and user-defined literals
+  def convert(implicit literal: LiteralContext): Expr[G] = literal match {
+    case Literal0(intLit) => parseInt(intLit).getOrElse(??(literal))
+    case Literal1(charLit) => parseChar(charLit).getOrElse(??(literal))
+    case Literal2(floatLit) => parseFloat(floatLit).getOrElse(??(literal))
+    case Literal3(strLit) => parseString(strLit).getOrElse(??(literal))
+    case Literal4(value) => BooleanValue(value == "true")
+    case Literal5(_) => Null()
+    case Literal6(_) => ??(literal)
+  }
+
+  def convert(implicit idExpr: IdExpressionContext): CPPTypedefName[G] = idExpr match {
+    case IdExpression0(id) => convert(id)
+    case IdExpression1(id) => convert(id)
+  }
+
+  def parseFloat(numFlag: String)(implicit o: Origin): Option[Expr[G]] = {
+    try {
+      Some(numFlag.last match {
+        case 'f' | 'F' => FloatValue(BigDecimal(numFlag.init), TFloats.ieee754_32bit)
+        case 'l' | 'L' => FloatValue(BigDecimal(numFlag.init), TFloats.ieee754_64bit)
+        case _ => FloatValue(BigDecimal(numFlag), TFloats.ieee754_32bit)
+      })
+    } catch {
+      case _: NumberFormatException => None
+    }
+  }
+
+  def parseInt(i: String)(implicit o: Origin): Option[Expr[G]] =
+    try {
+      Some(IntegerValue(BigInt(i)))
+    } catch {
+      case _: NumberFormatException => None
+    }
+
+  private def parseChar(value: String)(implicit o: Origin): Option[Expr[G]] = {
+    val fixedValue = fixEscapeAndUnicodeChars(value)
+    val pattern = "^'(.|\n|\r)'$".r
+    fixedValue match {
+      case pattern(char, _*) => Some(CharValue(char.codePointAt(0)))
+      case _ => None
+    }
+  }
+
+  private def parseString(value: String)(implicit o: Origin): Option[Expr[G]] = {
+    val fixedValue = fixEscapeAndUnicodeChars(value)
+    val pattern = "^\"((.|\n|\r)*)\"$".r
+    fixedValue match {
+      case pattern(str, _*) => Some(StringValue(str))
+      case _ => None
+    }
+  }
+
+  // ANTLR separates escape sequences such into separate characters, so '\n' will be '\' and 'n'
+  // This function combines them back into 1 character
+  private def fixEscapeAndUnicodeChars(str: String): String = {
+    var result = str
+
+    val unicodePattern = "\\\\u([0-9a-fA-F]{4})".r
+    var patMatchOpt = unicodePattern.findFirstMatchIn(result)
+    while (patMatchOpt.isDefined) {
+      val patMatch = patMatchOpt.get
+      result = result.substring(0, patMatch.start) + new String(patMatch.group(1).sliding(2, 2).toArray.map(Integer.parseInt(_, 16).toByte), "UNICODE") + result.substring(patMatch.end)
+      patMatchOpt = unicodePattern.findFirstMatchIn(result)
+    }
+
+    val escapePattern = "\\\\(['\"\\\\nrt])".r
+    val escapeMap: Map[String, String] = Map("'" -> "'", "\"" -> "\"", "\\" -> "\\", "n" -> "\n", "r" -> "\r", "t" -> "\t")
+    patMatchOpt = escapePattern.findFirstMatchIn(result)
+    while (patMatchOpt.isDefined) {
+      val patMatch = patMatchOpt.get
+      result = result.substring(0, patMatch.start) + escapeMap(patMatch.group(1)) + result.substring(patMatch.end)
+      patMatchOpt = unicodePattern.findFirstMatchIn(result)
+    }
+
+    result
+  }
+
+  // Not supporting attribute specifiers
+  def convert(implicit declSpecSeq: DeclSpecifierSeqContext): Seq[CPPDeclarationSpecifier[G]] = declSpecSeq match {
+    case DeclSpecifierSeq0(declSpec, None) => declSpec.flatMap(convert(_))
+    case x => ??(x)
+  }
+
+  // Do not support storage specifiers, function specifiers, friends, typedefs, consts.
+  def convert(implicit declSpec: DeclSpecifierContext): Seq[CPPDeclarationSpecifier[G]] = declSpec match {
+    case DeclSpecifier1(typeSpec) => convert(typeSpec)
+    case DeclSpecifier6(valEmbedModifier) => withModifiers(valEmbedModifier, m => {
+      if (m.consume(m.pure))
+        Seq(new CPPPure[G]())
+      else if (m.consume(m.inline))
+        Seq(new CPPInline[G]())
+      else
+        fail(m.nodes.head, "This modifier cannot be attached to a declaration in C++")
+    })
+    case x => ??(x)
+  }
+
+  // Do not support enum or class declarations, such as 'class className { members }' as type specifiers
+  def convert(implicit typeSpec: TypeSpecifierContext): Seq[CPPTypeSpecifier[G]] = typeSpec match {
+    case TypeSpecifier0(trailingTypeSpec) => convert(trailingTypeSpec)
+    case x => ??(x)
+  }
+
+  // Do not support elaboratedTypeSpec, typeNameSpec, and cvQualifier
+  def convert(implicit typeSpec: TrailingTypeSpecifierContext): Seq[CPPTypeSpecifier[G]] = typeSpec match {
+    case TrailingTypeSpecifier0(simpleTypeSpec) => convert(simpleTypeSpec)
+    case x => ??(x)
+  }
+
+  // Do not support types: template, char16_t, char32_t, wchar_t, auto, decltype(), and combination of namespace and typename
+  def convert(implicit typeSpec: SimpleTypeSpecifierContext): Seq[CPPTypeSpecifier[G]] = typeSpec match {
+    case SimpleTypeSpecifier0(None, typeName) => Seq(convert(typeName))
+    case SimpleTypeSpecifier2(signedness) => Seq(convert(signedness))
+    case SimpleTypeSpecifier3(Some(signedness), typeLengthMods) => Seq(convert(signedness)) ++ typeLengthMods.map(convert(_))
+    case SimpleTypeSpecifier3(None, typeLengthMods) => typeLengthMods.map(convert(_))
+    case SimpleTypeSpecifier4(Some(signedness), _) => Seq(convert(signedness), new CPPChar[G]())
+    case SimpleTypeSpecifier4(None, _) => Seq(new CPPChar[G]())
+    case SimpleTypeSpecifier8(_) => Seq(new CPPBool[G]())
+    case SimpleTypeSpecifier9(Some(signedness), typeLengthMods, _) => Seq(convert(signedness)) ++ typeLengthMods.map(convert(_)) :+ new CPPInt[G]()
+    case SimpleTypeSpecifier9(None, typeLengthMods, _) => typeLengthMods.map(convert(_)) :+ new CPPInt[G]()
+    case SimpleTypeSpecifier10(_) => Seq(CPPSpecificationType(TFloats.ieee754_32bit))
+    case SimpleTypeSpecifier11(Some(typeLengthMod), _) => Seq(convert(typeLengthMod), CPPSpecificationType(TFloats.ieee754_64bit))
+    case SimpleTypeSpecifier11(None, _) => Seq(CPPSpecificationType(TFloats.ieee754_64bit))
+    case SimpleTypeSpecifier12(_) => Seq(new CPPVoid[G]())
+    case SimpleTypeSpecifier13(_) => Seq(new SYCLQueue[G]())
+    case SimpleTypeSpecifier15(valType) => Seq(CPPSpecificationType(convert(valType)))
+    case x => ??(x)
+  }
+
+  def convert(implicit signedness: SimpleTypeSignednessModifierContext): CPPTypeSpecifier[G] = signedness match {
+    case SimpleTypeSignednessModifier0(_) => new CPPUnsigned[G]()
+    case SimpleTypeSignednessModifier1(_) => new CPPSigned[G]()
+  }
+
+  def convert(implicit simpleTypeLengthMod: SimpleTypeLengthModifierContext): CPPTypeSpecifier[G] = simpleTypeLengthMod match {
+    case SimpleTypeLengthModifier0(_) => new CPPShort[G]()
+    case SimpleTypeLengthModifier1(_) => new CPPLong[G]()
+  }
+
+  // Do not support template or decltypes, or a typename as identifier in the nestedname
+  def convert(implicit nestedNameSpec: NestedNameSpecifierContext): CPPTypedefName[G] = nestedNameSpec match {
+    case NestedNameSpecifier0(theTypeName, sep) =>
+      convert(theTypeName) match {
+        case name@CPPTypedefName(_) => name.appendName(sep)
+        case x => ??(theTypeName)
+      }
+    case NestedNameSpecifier1(namespaceName, sep) => convert(namespaceName).appendName(sep)
+    case NestedNameSpecifier3(sep) => CPPTypedefName(sep)
+    case NestedNameSpecifier4(inner, id, sep) =>
+      convert(inner) match {
+        case name@CPPTypedefName(_) => name.appendName(convert(id)).appendName(sep)
+        case _ => ??(inner)
+      }
+    case x => ??(x)
+  }
+
+  def convert(implicit namespaceName: NamespaceNameContext): CPPTypedefName[G] = namespaceName match {
+    case NamespaceName0(OriginalNamespaceName0(id)) => CPPTypedefName(convert(id))
+    case NamespaceName1(NamespaceAlias0(id)) => CPPTypedefName(convert(id))
+  }
+
+  // Do not support enum-names, typedef-names and template-names
+  def convert(implicit theTypeName: TheTypeNameContext): CPPTypeSpecifier[G] = theTypeName match {
+    case TheTypeName0(className) => convert(className)
+    case x => ??(x)
+  }
+
+  // Do not support template-names
+  def convert(implicit className: ClassNameContext): CPPTypeSpecifier[G] = className match {
+    case ClassName0(name) => CPPTypedefName(convert(name))
+    case x => ??(x)
+  }
+
+  // Do not support trailing return types
+  def convert(implicit declarator: DeclaratorContext): CPPDeclarator[G] = declarator match {
+    case Declarator0(pointerDeclarator) => convert(pointerDeclarator)
+    case Declarator1(_, _, _) => ??(declarator)
+  }
+
+  def convert(implicit pointerDeclarator: PointerDeclaratorContext): CPPDeclarator[G] = pointerDeclarator match {
+    case PointerDeclarator0(pointerDeclaratorPrefix, noPointerDeclarator)
+      if pointerDeclaratorPrefix.isEmpty => convert(noPointerDeclarator)
+    case PointerDeclarator0(pointerDeclaratorPrefix, noPointerDeclarator)
+      if pointerDeclaratorPrefix.nonEmpty =>
+        val pointers = pointerDeclaratorPrefix.flatMap(convert(_))
+        CPPPointerDeclarator(pointers, convert(noPointerDeclarator))
+  }
+
+  // Do not support postfix 'const'
+  def convert(implicit pointer: PointerDeclaratorPrefixContext): Seq[CPPPointer[G]] = pointer match {
+    case PointerDeclaratorPrefix0(pointerOp, None) => convert(pointerOp)
+    case x => ??(x)
+  }
+
+  // Do not support nestedNameSpecifier, attributeSpeciefierSeq, and cvQualifierSeq
+  def convert(implicit pointerOp: PointerOperatorWithDoubleStarContext): Seq[CPPPointer[G]] = pointerOp match {
+    case PointerOperatorWithDoubleStar0(pointerOp) => convert(pointerOp)
+    case PointerOperatorWithDoubleStar1(None, _, None, None) => Seq(CPPPointer(), CPPPointer())
+    case x => ??(x)
+  }
+
+  // Do not support '&' and '&&' and nestedNameSpecifier, attributeSpeciefierSeq, and cvQualifierSeq
+  def convert(implicit pointerOp: PointerOperatorContext): Seq[CPPPointer[G]] = pointerOp match {
+    case PointerOperator2(None, _, None, None) => Seq(CPPPointer())
+    case x => ??(x)
+  }
+
+  // Do not support attributeSpeciefierSeq
+  def convert(noPointerDeclarator: NoPointerDeclaratorContext)(implicit o: Origin): CPPDeclarator[G] = noPointerDeclarator match {
+    case NoPointerDeclarator0(declaratorId, None) => convert(declaratorId)
+    case NoPointerDeclarator1(innerDeclarator, paramsAndQuals) =>
+      val (params, varargs) = convert(paramsAndQuals)
+      CPPTypedFunctionDeclarator[G](params, varargs, convert(innerDeclarator))
+    case NoPointerDeclarator2(innerDeclarator, _, None, _, None) =>
+      convert(innerDeclarator) match {
+        case CPPArrayDeclarator(_, _) => ??(noPointerDeclarator) // Do not support > 1 dimensions
+        case inner => CPPArrayDeclarator(inner, None)(blame(noPointerDeclarator))
+      }
+    case NoPointerDeclarator2(innerDeclarator, _, Some(constExpr), _, None) =>
+      convert(innerDeclarator) match {
+        case CPPArrayDeclarator(_, _) => ??(noPointerDeclarator) // Do not support > 1 dimensions
+        case inner => CPPArrayDeclarator(inner, Some(convert(constExpr)))(blame(noPointerDeclarator))
+      }
+    case NoPointerDeclarator3(_, pointerDecl, _) => ??(pointerDecl)
+    case x => ??(x)
+  }
+
+  def convert(implicit constExpr: ConstantExpressionContext): Expr[G] = constExpr match {
+    case ConstantExpression0(condExpr) => convert(condExpr)
+  }
+
+  // Do not support cvQualifier, refqualifier, exceptionSpec and attributeSpec
+  def convert(implicit paramsAndQuals: ParametersAndQualifiersContext): (Seq[CPPParam[G]], Boolean) = paramsAndQuals match {
+    case ParametersAndQualifiers0(_, None, _, None, None, None, None) => (Seq(), false)
+    case ParametersAndQualifiers0(_, Some(paramDeclClause), _, None, None, None, None) => convert(paramDeclClause)
+  }
+
+  def convert(implicit paramDeclClause: ParameterDeclarationClauseContext): (Seq[CPPParam[G]], Boolean) = paramDeclClause match {
+    case ParameterDeclarationClause0(paramDeclList, None) => (convert(paramDeclList), false)
+    case ParameterDeclarationClause0(paramDeclList, Some(_)) => (convert(paramDeclList), true)
+  }
+
+  def convert(implicit paramDeclList: ParameterDeclarationListContext): Seq[CPPParam[G]] = paramDeclList match {
+    case value: ParameterDeclarationList0Context => value.parameterDeclaration.asScala.toSeq.map(convert(_))
+  }
+
+  // only support params in form of 'declSpecifiers declarator'
+  def convert(implicit paramDecl: ParameterDeclarationContext): CPPParam[G] = paramDecl match {
+    case ParameterDeclaration0(declSpecs, declarator) => new CPPParam[G](convert(declSpecs), convert(declarator))
+    case x => ??(x)
+  }
+
+  // Do not support if spread operator '...' is used
+  def convert(implicit declaratorId: DeclaratoridContext): CPPDeclarator[G] = declaratorId match {
+    case Declaratorid0(None, idExpr) => CPPName(convert(idExpr).nestedName)
+    case x => ??(x)
+  }
+
+  // Do not support operatorFunctionId, conversionFunctionId, literalOperatorId, templateId, and things starting with a tilde
+  def convert(implicit unqualifiedId: UnqualifiedIdContext): CPPTypedefName[G] = unqualifiedId match {
+    case UnqualifiedId0(clangppId) => CPPTypedefName(convert(clangppId))
+    case x => ??(x)
+  }
+
+  // Do not support template
+  def convert(implicit qualifiedId: QualifiedIdContext): CPPTypedefName[G] = qualifiedId match {
+    case QualifiedId0(nestedNameSpec, None, id) => CPPTypedefName(convert(nestedNameSpec).nestedName ++ convert(id).nestedName)
+    case x => ??(x)
+  }
+
+  def convert(implicit id: ClangppIdentifierContext): String = id match {
+    case ClangppIdentifier0(text) => text
+    case ClangppIdentifier1(inner) => convert(inner)
+  }
+
+  def convert(expr: LangExprContext): Expr[G] = expr match {
+    case LangExpr0(expr) => convert(expr)
+  }
+
+  def convert(stat: LangStatementContext): Statement[G] = stat match {
+    case LangStatement0(stat) => convert(stat)
+  }
+
+  def convert(implicit t: LangTypeContext): Type[G] = t match {
+    case LangType0(typeSpec) => CPPPrimitiveType(convert(typeSpec))
+  }
+
+  def convert(id: LangIdContext): String = id match {
+    case LangId0(id) => convert(id)
+  }
+
+  def convert(implicit n: LangConstIntContext): BigInt = n match {
+    case LangConstInt0(Literal0(string)) => BigInt(string)
+    case LangConstInt0(Literal1(string)) => BigInt(string)
+    case LangConstInt0(Literal2(string)) => BigInt(string)
+    case x => ??(x)
+  }
+
+  def local(ctx: ParserRuleContext, name: String): Expr[G] =
+    CPPLocal(name)(blame(ctx))(origin(ctx))
+
+  def convert(decl: LangGlobalDeclContext): Seq[GlobalDeclaration[G]] = decl match {
+    case LangGlobalDecl0(decl) => convert(decl)
+  }
+
+  def convert(decl: LangClassDeclContext): Seq[ClassDeclaration[G]] = Nil
+
+  def withCollector[T](collector: ContractCollector[G], f: ContractCollector[G] => T): T = {
+    val result = f(collector)
+    collector.nodes.headOption match {
+      case Some(node) => fail(node, "This specification clause may not occur here")
+      case None => result
+    }
+  }
+
+  def withContract[T](node: Option[ValEmbedContractContext], f: ContractCollector[G] => T): T = {
+    val collector = new ContractCollector[G]()
+    node.foreach(convert(_, collector))
+    withCollector(collector, f)
+  }
+
+  def withContract[T](node1: Option[ValEmbedContractContext], node2: Option[ValEmbedContractContext], f: ContractCollector[G] => T): T = {
+    val collector = new ContractCollector[G]()
+    node1.foreach(convert(_, collector))
+    node2.foreach(convert(_, collector))
+    withCollector(collector, f)
+  }
+
+  def withContract[T](node: Seq[ValContractClauseContext], f: ContractCollector[G] => T): T = {
+    val collector = new ContractCollector[G]()
+    node.foreach(convert(_, collector))
+    withCollector(collector, f)
+  }
+
+  def withCollector[T](collector: ModifierCollector, f: ModifierCollector => T): T = {
+    val result = f(collector)
+    collector.nodes.headOption match {
+      case Some(node) => fail(node, "This modifier cannot be attached to this declaration")
+      case None => result
+    }
+  }
+
+  def withModifiers[T](node: Seq[ValModifierContext], f: ModifierCollector => T): T = {
+    val collector = new ModifierCollector()
+    node.foreach(convert(_, collector))
+    withCollector(collector, f)
+  }
+
+  def withModifiers[T](node: ValEmbedModifierContext, f: ModifierCollector => T): T = {
+    val collector = new ModifierCollector()
+    convert(node, collector)
+    withCollector(collector, f)
+  }
+
+  def convert(contract: ValEmbedContractContext, collector: ContractCollector[G]): Unit = contract match {
+    case ValEmbedContract0(blocks) => blocks.foreach(convert(_, collector))
+  }
+
+  def convert(contract: ValEmbedContractBlockContext, collector: ContractCollector[G]): Unit = contract match {
+    case ValEmbedContractBlock0(_, clauses, _) => clauses.foreach(convert(_, collector))
+    case ValEmbedContractBlock1(clauses) => clauses.foreach(convert(_, collector))
+  }
+
+  def convert(implicit contract: ValContractClauseContext, collector: ContractCollector[G]): Unit = contract match {
+    case ValContractClause0(_, ids, _) => collector.modifies ++= convert(ids).map((contract, _))
+    case ValContractClause1(_, ids, _) => collector.accessible ++= convert(ids).map((contract, _))
+    case ValContractClause2(_, exp, _) => collector.requires += ((contract, convert(exp)))
+    case ValContractClause3(_, exp, _) => collector.ensures += ((contract, convert(exp)))
+    case ValContractClause4(_, t, id, _) =>
+      val variable = new Variable(convert(t))(SourceNameOrigin(convert(id), origin(contract)))
+      collector.given += ((contract, variable))
+    case ValContractClause5(_, t, id, _) =>
+      val variable = new Variable(convert(t))(SourceNameOrigin(convert(id), origin(contract)))
+      collector.yields += ((contract, variable))
+    case ValContractClause6(_, exp, _) => collector.context_everywhere += ((contract, convert(exp)))
+    case ValContractClause7(_, exp, _) =>
+      collector.requires += ((contract, convert(exp)))
+      collector.ensures += ((contract, convert(exp)))
+    case ValContractClause8(_, exp, _) => collector.loop_invariant += ((contract, convert(exp)))
+    case ValContractClause9(_, exp, _) => collector.kernel_invariant += ((contract, convert(exp)))
+    case ValContractClause10(_, _, t, id, _, exp, _) =>
+      val variable = new Variable(convert(t))(SourceNameOrigin(convert(id), origin(contract)))
+      collector.signals += ((contract, SignalsClause(variable, convert(exp))(originProvider(contract))))
+    case ValContractClause11(_, invariant, _) => collector.lock_invariant += ((contract, convert(invariant)))
+    case ValContractClause12(_, None, _) => collector.decreases += ((contract, DecreasesClauseNoRecursion()))
+    case ValContractClause12(_, Some(clause), _) => collector.decreases += ((contract, convert(clause)))
+  }
+
+  def convert(implicit clause: ValDecreasesMeasureContext): DecreasesClause[G] = clause match {
+    case ValDecreasesMeasure0(_) => DecreasesClauseAssume()
+    case ValDecreasesMeasure1(exps) => DecreasesClauseTuple(convert(exps))
+  }
+
+  def convert(mod: ValEmbedModifierContext, collector: ModifierCollector): Unit = mod match {
+    case ValEmbedModifier0(_, mod, _) => convert(mod, collector)
+    case ValEmbedModifier1(mod) => convert(mod, collector)
+  }
+
+  def convert(mod: ValModifierContext, collector: ModifierCollector): Unit = mod match {
+    case ValModifier0(name) => name match {
+      case "pure" => collector.pure += mod
+      case "inline" => collector.inline += mod
+      case "thread_local" => collector.threadLocal += mod
+    }
+    case ValStatic(_) => collector.static += mod
+  }
+
+  def convertEmbedWith(implicit whiff: Option[ValEmbedWithContext], inner: Expr[G]): Expr[G] = whiff match {
+    case None => inner
+    case Some(ValEmbedWith0(_, whiff, _)) => convertWith(whiff, inner)
+    case Some(ValEmbedWith1(whiff)) => convertWith(Some(whiff), inner)
+  }
+
+  def convertWith(implicit whiff: Option[ValWithContext], inner: Expr[G]): Expr[G] = whiff match {
+    case None => inner
+    case Some(whiff@ValWith0(_, stat)) => With(convert(stat), inner)(origin(whiff))
+  }
+
+  def convertEmbedThen(implicit den: Option[ValEmbedThenContext], inner: Expr[G]): Expr[G] = den match {
+    case None => inner
+    case Some(ValEmbedThen0(_, den, _)) => convertThen(den, inner)
+    case Some(ValEmbedThen1(den)) => convertThen(Some(den), inner)
+  }
+
+  def convertThen(implicit den: Option[ValThenContext], inner: Expr[G]): Expr[G] = den match {
+    case None => inner
+    case Some(den@ValThen0(_, stat)) => Then(inner, convert(stat))(origin(den))
+  }
+
+  def convert(implicit whiff: ValEmbedWithContext): Statement[G] = whiff match {
+    case ValEmbedWith0(_, Some(whiff), _) => convert(whiff)
+    case ValEmbedWith0(_, None, _) => Block(Nil)
+    case ValEmbedWith1(whiff) => convert(whiff)
+  }
+
+  def convert(implicit whiff: ValWithContext): Statement[G] = whiff match {
+    case ValWith0(_, stat) => convert(stat)
+  }
+
+  def convert(implicit whiff: ValEmbedThenContext): Statement[G] = whiff match {
+    case ValEmbedThen0(_, Some(whiff), _) => convert(whiff)
+    case ValEmbedThen0(_, None, _) => Block(Nil)
+    case ValEmbedThen1(whiff) => convert(whiff)
+  }
+
+  def convert(implicit whiff: ValThenContext): Statement[G] = whiff match {
+    case ValThen0(_, stat) => convert(stat)
+  }
+
+  def convertEmbedGiven(implicit given: Option[ValEmbedGivenContext]): Seq[(Ref[G, Variable[G]], Expr[G])] = given match {
+    case None => Nil
+    case Some(ValEmbedGiven0(_, inner, _)) => convertGiven(inner)
+    case Some(ValEmbedGiven1(inner)) => convertGiven(Some(inner))
+  }
+
+  def convertGiven(implicit given: Option[ValGivenContext]): Seq[(Ref[G, Variable[G]], Expr[G])] = given match {
+    case None => Nil
+    case Some(ValGiven0(_, _, mappings, _)) => convert(mappings)
+  }
+
+  def convert(implicit mappings: ValGivenMappingsContext): Seq[(Ref[G, Variable[G]], Expr[G])] = mappings match {
+    case ValGivenMappings0(arg, _, v) => Seq((new UnresolvedRef[G, Variable[G]](convert(arg)), convert(v)))
+    case ValGivenMappings1(arg, _, v, _, more) => (new UnresolvedRef[G, Variable[G]](convert(arg)), convert(v)) +: convert(more)
+  }
+
+  def convertEmbedYields(implicit given: Option[ValEmbedYieldsContext]): Seq[(Expr[G], Ref[G, Variable[G]])] = given match {
+    case None => Nil
+    case Some(ValEmbedYields0(_, inner, _)) => convertYields(inner)
+    case Some(ValEmbedYields1(inner)) => convertYields(Some(inner))
+  }
+
+  def convertYields(implicit given: Option[ValYieldsContext]): Seq[(Expr[G], Ref[G, Variable[G]])] = given match {
+    case None => Nil
+    case Some(ValYields0(_, _, mappings, _)) => convert(mappings)
+  }
+
+  def convert(implicit mappings: ValYieldsMappingsContext): Seq[(Expr[G], Ref[G, Variable[G]])] = mappings match {
+    case ValYieldsMappings0(target, _, res) => Seq((local(target, convert(target)), new UnresolvedRef[G, Variable[G]](convert(res))))
+    case ValYieldsMappings1(target, _, res, _, more) => (local(target, convert(target)), new UnresolvedRef[G, Variable[G]](convert(res))) +: convert(more)
+  }
+
+  def convert(implicit exprs: ValExpressionListContext): Seq[Expr[G]] = exprs match {
+    case ValExpressionList0(expr) => Seq(convert(expr))
+    case ValExpressionList1(head, _, tail) => convert(head) +: convert(tail)
+  }
+
+  def convert(implicit ids: ValIdListContext): Seq[String] = ids match {
+    case ValIdList0(id) => Seq(convert(id))
+    case ValIdList1(id, _, ids) => convert(id) +: convert(ids)
+  }
+
+  def convert(implicit ts: ValTypeListContext): Seq[Type[G]] = ts match {
+    case ValTypeList0(t) => Seq(convert(t))
+    case ValTypeList1(t, _, ts) => convert(t) +: convert(ts)
+  }
+
+  def convert(implicit root: ParserRuleContext, impOp: ValImpOpContext, left: Expr[G], right: Expr[G]): Expr[G] = impOp match {
+    case ValImpOp0(_) => Wand(left, right)(origin(impOp))
+    case ValImpOp1(_) => Implies(left, right)(origin(impOp))
+  }
+
+  def convert(implicit root: ParserRuleContext, andOp: ValAndOpContext, left: Expr[G], right: Expr[G]): Expr[G] = andOp match {
+    case ValAndOp0(_) => col.Star(left, right)(origin(andOp))
+  }
+
+  def convert(implicit root: ParserRuleContext, inOp: ValInOpContext, left: Expr[G], right: Expr[G]): Expr[G] = inOp match {
+    case ValInOp0(_) => AmbiguousMember(left, right)
+  }
+
+  def convert(implicit root: ParserRuleContext, mulOp: ValMulOpContext, left: Expr[G], right: Expr[G]): Expr[G] = mulOp match {
+    case ValMulOp0(_) => col.Div(left, right)(blame(mulOp))
+  }
+
+  def convert(implicit root: ParserRuleContext, prependOp: ValPrependOpContext, left: Expr[G], right: Expr[G]): Expr[G] = prependOp match {
+    case ValPrependOp0(_) => Cons(left, right)
+  }
+
+  def convert(implicit root: ParserRuleContext, postfixOp: ValPostfixContext, xs: Expr[G]): Expr[G] = postfixOp match {
+    case ValPostfix0(_, _, to, _) => Take(xs, convert(to))
+    case ValPostfix1(_, from, _, None, _) => Drop(xs, convert(from))
+    case ValPostfix1(_, from, _, Some(to), _) => Slice(xs, convert(from), convert(to))
+    case ValPostfix2(_, idx, _, v, _) => SeqUpdate(xs, convert(idx), convert(v))
+    case ValPostfix3(_, name, _, args, _) => CoalesceInstancePredicateApply(xs, new UnresolvedRef[G, InstancePredicate[G]](convert(name)), args.map(convert(_)).getOrElse(Nil), WritePerm())
+  }
+
+  def convert(implicit root: ParserRuleContext, prefixOp: ValPrefixContext, xs: Expr[G]): Expr[G] = prefixOp match {
+    case ValScale(_, scale, _) => Scale(convert(scale), xs)(blame(prefixOp))
+  }
+
+  def convert(implicit block: ValEmbedStatementBlockContext): Statement[G] = block match {
+    case ValEmbedStatementBlock0(_, stats, _) => Block(stats.map(convert(_)))
+    case ValEmbedStatementBlock1(stats) => Block(stats.map(convert(_)))
+    case ValEmbedStatementBlock2(_, _, _, stat) => Extract(convert(stat))
+    case ValEmbedStatementBlock3(_, _, clauses, _, _, body, _, _, _) =>
+      withContract(clauses, contract => {
+        FramedProof(
+          AstBuildHelpers.foldStar(contract.consume(contract.requires)),
+          Block(body.map(convert(_))),
+          AstBuildHelpers.foldStar(contract.consume(contract.ensures)),
+        )(blame(block))
+      })
+  }
+
+  def convert(implicit stat: ValStatementContext): Statement[G] = stat match {
+    case ValPackage(_, expr, innerStat) => WandPackage(convert(expr), convert(innerStat))(blame(stat))
+    case ValApplyWand(_, wand, _) => WandApply(convert(wand))(blame(stat))
+    case ValFold(_, predicate, _) =>
+      Fold(convert(predicate))(blame(stat))
+    case ValUnfold(_, predicate, _) =>
+      Unfold(convert(predicate))(blame(stat))
+    case ValOpen(_, _, _) => ??(stat)
+    case ValClose(_, _, _) => ??(stat)
+    case ValAssert(_, assn, _) => Assert(convert(assn))(blame(stat))
+    case ValAssume(_, assn, _) => Assume(convert(assn))
+    case ValInhale(_, resource, _) => Inhale(convert(resource))
+    case ValExhale(_, resource, _) => Exhale(convert(resource))(blame(stat))
+    case ValLabel(_, label, _) =>
+      Label(new LabelDecl()(SourceNameOrigin(convert(label), origin(stat))), Block(Nil))
+    case ValRefute(_, assn, _) => Refute(convert(assn))(blame(stat))
+    case ValWitness(_, _, _) => ??(stat)
+    case ValGhost(_, stat) => convert(stat)
+    case ValSend(_, name, _, delta, _, resource, _) =>
+      Send(new SendDecl()(SourceNameOrigin(convert(name), origin(stat))), convert(delta), convert(resource))(blame(stat))
+    case ValRecv(_, name, _) =>
+      Recv(new UnresolvedRef[G, SendDecl[G]](convert(name)))
+    case ValTransfer(_, _, _) => ??(stat)
+    case ValCslSubject(_, _, _) => ??(stat) // FIXME PB: csl_subject seems to be used
+    case ValSpecIgnoreStart(_, _) => SpecIgnoreEnd()
+    case ValSpecIgnoreEnd(_, _) => SpecIgnoreStart()
+    case ValActionModel(_, _, model, _, perm, _, after, _, action, _, impl) =>
+      ModelDo(convert(model), convert(perm), convert(after), convert(action), impl match {
+        case ValActionImpl0(_) => Block(Nil)
+        case ValActionImpl1(inner) => convert(inner)
+      })
+    case ValAtomic(_, _, invariant, _, body) =>
+      ParAtomic(Seq(new UnresolvedRef[G, ParInvariantDecl[G]](convert(invariant))), convert(body))(blame(stat))
+    case ValCommit(_, obj, _) =>
+      Commit(convert(obj))(blame(stat))
+    case ValExtract(_, body) =>
+      Extract(convert(body))
+    case ValFrame(_, clauses, body) =>
+      withContract(clauses, contract => {
+        FramedProof(
+          AstBuildHelpers.foldStar(contract.consume(contract.requires)),
+          convert(body),
+          AstBuildHelpers.foldStar(contract.consume(contract.ensures)),
+        )(blame(stat))
+      })
+  }
+
+  def convert(implicit block: ValBlockContext): Seq[Statement[G]] = block match {
+    case ValBlock0(_, stats, _) => stats.map(convert(_))
+  }
+
+  def convert(implicit arg: ValArgContext): Variable[G] = arg match {
+    case ValArg0(t, id) => new Variable(convert(t))(SourceNameOrigin(convert(id), origin(arg)))
+  }
+
+  def convert(implicit args: ValArgListContext): Seq[Variable[G]] = args match {
+    case ValArgList0(arg) => Seq(convert(arg))
+    case ValArgList1(arg, _, args) => convert(arg) +: convert(args)
+  }
+
+  def convert(implicit decl: ValEmbedGlobalDeclarationBlockContext): Seq[GlobalDeclaration[G]] = decl match {
+    case ValEmbedGlobalDeclarationBlock0(_, globals, _) => globals.flatMap(convert(_))
+    case ValEmbedGlobalDeclarationBlock1(globals) => globals.flatMap(convert(_))
+  }
+
+  def convert(implicit decl: ValGlobalDeclarationContext): Seq[GlobalDeclaration[G]] = decl match {
+    case ValAxiom(_, name, _, axiom, _) =>
+      Seq(new SimplificationRule(convert(axiom))(SourceNameOrigin(convert(name), origin(decl))))
+    case ValPredicate(modifiers, _, name, _, args, _, definition) =>
+      withModifiers(modifiers, mods =>
+        Seq(new Predicate(args.map(convert(_)).getOrElse(Nil), convert(definition),
+          mods.consume(mods.threadLocal), mods.consume(mods.inline))
+        (SourceNameOrigin(convert(name), origin(decl)))))
+    case ValFunction(contract, modifiers, _, t, name, typeArgs, _, args, _, definition) =>
+      Seq(withContract(contract, c =>
+        withModifiers(modifiers, m => {
+          val namedOrigin = SourceNameOrigin(convert(name), origin(decl))
+          new Function(
+            convert(t),
+            args.map(convert(_)).getOrElse(Nil),
+            typeArgs.map(convert(_)).getOrElse(Nil),
+            convert(definition),
+            c.consumeApplicableContract(blame(decl)),
+            m.consume(m.inline))(blame(decl))(namedOrigin)
+        })
+      ))
+    case ValModel(_, name, _, decls, _) =>
+      Seq(new Model(decls.flatMap(convert(_)))(SourceNameOrigin(convert(name), origin(decl))))
+    case ValGhostDecl(_, inner) =>
+      convert(inner)
+    case ValAdtDecl(_, name, typeArgs, _, decls, _) =>
+      Seq(new AxiomaticDataType(decls.map(convert(_)), typeArgs.map(convert(_)).getOrElse(Nil))(
+        SourceNameOrigin(convert(name), origin(decl))))
+  }
+
+  def convert(implicit decl: ValEmbedClassDeclarationBlockContext): Seq[ClassDeclaration[G]] = decl match {
+    case ValEmbedClassDeclarationBlock0(_, decls, _) => decls.flatMap(convert(_, x => x))
+    case ValEmbedClassDeclarationBlock1(decls) => decls.flatMap(convert(_, x => x))
+  }
+
+  def convert[T](implicit decl: ValClassDeclarationContext, transform: ClassDeclaration[G] => T): Seq[T] = decl match {
+    case ValInstancePredicate(modifiers, _, name, _, args, _, definition) =>
+      Seq(withModifiers(modifiers, mods => {
+        transform(new InstancePredicate(args.map(convert(_)).getOrElse(Nil), convert(definition),
+          mods.consume(mods.threadLocal), mods.consume(mods.inline))(
+          SourceNameOrigin(convert(name), origin(decl))))
+      }))
+    case ValInstanceFunction(contract, modifiers, _, t, name, typeArgs, _, args, _, definition) =>
+      Seq(withContract(contract, c => {
+        withModifiers(modifiers, m => {
+          transform(new InstanceFunction(
+            convert(t),
+            args.map(convert(_)).getOrElse(Nil),
+            typeArgs.map(convert(_)).getOrElse(Nil),
+            convert(definition),
+            c.consumeApplicableContract(blame(decl)), m.consume(m.inline))(
+            blame(decl))(
+            SourceNameOrigin(convert(name), origin(decl))))
+        })
+      }))
+    case ValInstanceGhostDecl(_, decl) => convert(decl).map(transform)
+  }
+
+  def convert(implicit decl: ValModelDeclarationContext): Seq[ModelDeclaration[G]] = decl match {
+    case ValModelField(t, name, _) =>
+      convert(name).map(name => {
+        new ModelField(convert(t))(SourceNameOrigin(name, origin(decl)))
+      })
+    case ValModelProcess(contract, _, name, _, args, _, _, definition, _) =>
+      Seq(withContract(contract, c => {
+        new ModelProcess(args.map(convert(_)).getOrElse(Nil), convert(definition),
+          AstBuildHelpers.foldAnd(c.consume(c.requires)), AstBuildHelpers.foldAnd(c.consume(c.ensures)),
+          c.consume(c.modifies).map(new UnresolvedRef[G, ModelField[G]](_)), c.consume(c.accessible).map(new UnresolvedRef[G, ModelField[G]](_)))(
+          blame(decl))(SourceNameOrigin(convert(name), origin(decl)))
+      }))
+    case ValModelAction(contract, _, name, _, args, _, _) =>
+      Seq(withContract(contract, c => {
+        new ModelAction(args.map(convert(_)).getOrElse(Nil),
+          AstBuildHelpers.foldAnd(c.consume(c.requires)), AstBuildHelpers.foldAnd(c.consume(c.ensures)),
+          c.consume(c.modifies).map(new UnresolvedRef[G, ModelField[G]](_)), c.consume(c.accessible).map(new UnresolvedRef[G, ModelField[G]](_)))(
+          SourceNameOrigin(convert(name), origin(decl)))
+      }))
+  }
+
+  def convert(implicit ts: ValTypeVarsContext): Seq[Variable[G]] = ts match {
+    case ValTypeVars0(_, names, _) =>
+      convert(names).map(name => new Variable(TType(TAny()))(SourceNameOrigin(name, origin(ts))))
+  }
+
+  def convert(implicit decl: ValAdtDeclarationContext): ADTDeclaration[G] = decl match {
+    case ValAdtAxiom(_, ax, _) => new ADTAxiom(convert(ax))
+    case ValAdtFunction(_, returnType, name, _, args, _, _) =>
+      new ADTFunction(args.map(convert(_)).getOrElse(Nil), convert(returnType))(
+        SourceNameOrigin(convert(name), origin(decl)))
+  }
+
+  def convert(implicit definition: ValPureDefContext): Option[Expr[G]] = definition match {
+    case ValPureAbstractBody(_) => None
+    case ValPureBody(_, expr, _) => Some(convert(expr))
+  }
+
+  def convert(implicit definition: ValImpureDefContext): Option[Statement[G]] = definition match {
+    case ValImpureAbstractBody(_) => None
+    case ValImpureBody(statement) => Some(convert(statement))
+  }
+
+  def convert(implicit t: ValTypeContext): Type[G] = t match {
+    case ValPrimaryType(name) => name match {
+      case "resource" => TResource()
+      case "process" => TProcess()
+      case "frac" => TFraction()
+      case "zfrac" => TZFraction()
+      case "rational" => TRational()
+      case "bool" => TBool()
+      case "ref" => TRef()
+      case "any" => TAny()
+      case "nothing" => TNothing()
+    }
+    case ValSeqType(_, _, element, _) => TSeq(convert(element))
+    case ValSetType(_, _, element, _) => TSet(convert(element))
+    case ValBagType(_, _, element, _) => TBag(convert(element))
+    case ValOptionType(_, _, element, _) => TOption(convert(element))
+    case ValMapType(_, _, key, _, value, _) => TMap(convert(key), convert(value))
+    case ValTupleType(_, _, t1, _, t2, _) => TTuple(Seq(convert(t1), convert(t2)))
+    case ValPointerType(_, _, element, _) => TPointer(convert(element))
+    case ValTypeType(_, _, element, _) => TType(convert(element))
+    case ValEitherType(_, _, left, _, right, _) => TEither(convert(left), convert(right))
+  }
+
+  def convert(implicit e: ValPrimarySeqContext): Expr[G] = e match {
+    case ValCardinality(_, xs, _) => Size(convert(xs))
+    case ValArrayValues(_, _, a, _, from, _, to, _) => Values(convert(a), convert(from), convert(to))(blame(e))
+  }
+
+  def convert(implicit e: ValPrimaryOptionContext): Expr[G] = e match {
+    case ValSome(_, _, v, _) => OptSome(convert(v))
+  }
+
+  def convert(implicit e: ValPrimaryEitherContext): Expr[G] = e match {
+    case ValLeft(_, _, inner, _) => EitherLeft(convert(inner))
+    case ValRight(_, _, inner, _) => EitherRight(convert(inner))
+  }
+
+  // valsetcompselectors
+  def convert(implicit exprs: ValMapPairsContext): Seq[(Expr[G], Expr[G])] = exprs match {
+    case ValMapPairs0(k, _, v) => Seq((convert(k), convert(v)))
+    case ValMapPairs1(k, _, v, _, tail) => (convert(k), convert(v)) +: convert(tail)
+  }
+
+  def convert(implicit e: ValPrimaryCollectionConstructorContext): Expr[G] = e match {
+    case ValTypedLiteralSeq(_, _, t, _, _, exprs, _) => LiteralSeq(convert(t), exprs.map(convert(_)).getOrElse(Nil))
+    case ValTypedLiteralSet(_, _, t, _, _, exprs, _) => LiteralSet(convert(t), exprs.map(convert(_)).getOrElse(Nil))
+    case ValSetComprehension(_, _, t, _, _, value, _, selectors, _, something, _) => ??(e)
+    case ValTypedLiteralBag(_, _, t, _, _, exprs, _) => LiteralBag(convert(t), exprs.map(convert(_)).getOrElse(Nil))
+    case ValTypedLiteralMap(_, _, key, _, value, _, _, pairs, _) => LiteralMap(convert(key), convert(value), pairs.map(convert(_)).getOrElse(Nil))
+    case ValTypedTuple(_, _, t1, _, t2, _, _, v1, _, v2, _) =>
+      LiteralTuple(Seq(convert(t1), convert(t2)), Seq(convert(v1), convert(v2)))
+    case ValLiteralSeq(_, exprs, _) => UntypedLiteralSeq(convert(exprs))
+    case ValLiteralSet(_, exprs, _) => UntypedLiteralSet(convert(exprs))
+    case ValLiteralBag(_, exprs, _) => UntypedLiteralBag(convert(exprs))
+    case ValEmptySeq(_, t, _) => LiteralSeq(convert(t), Nil)
+    case ValEmptySet(_, t, _) => LiteralSet(convert(t), Nil)
+    case ValEmptyBag(_, t, _) => LiteralBag(convert(t), Nil)
+    case ValRange(_, from, _, to, _) => Range(convert(from), convert(to))
+  }
+
+  def convert(implicit e: ValPrimaryPermissionContext): Expr[G] = e match {
+    case ValCurPerm(_, _, loc, _) => CurPerm(AmbiguousLocation(convert(loc))(blame(e)))
+    case ValPerm(_, _, loc, _, perm, _) => Perm(AmbiguousLocation(convert(loc))(blame(e)), convert(perm))
+    case ValValue(_, _, loc, _) => Value(AmbiguousLocation(convert(loc))(blame(e)))
+    case ValPointsTo(_, _, loc, _, perm, _, v, _) => PointsTo(AmbiguousLocation(convert(loc))(blame(e)), convert(perm), convert(v))
+    case ValHPerm(_, _, loc, _, perm, _) => ModelPerm(convert(loc), convert(perm))
+    case ValAPerm(_, _, loc, _, perm, _) => ActionPerm(convert(loc), convert(perm))
+    case ValArrayPerm(_, _, arr, _, i, _, step, _, count, _, perm, _) => ??(e)
+    case ValMatrix(_, _, m, _, dim1, _, dim2, _) => ValidMatrix(convert(m), convert(dim1), convert(dim2))
+    case ValArray(_, _, arr, _, dim, _) => ValidArray(convert(arr), convert(dim))
+    case ValPointer(_, _, ptr, _, n, _, perm, _) => PermPointer(convert(ptr), convert(n), convert(perm))
+    case ValPointerIndex(_, _, ptr, _, idx, _, perm, _) => PermPointerIndex(convert(ptr), convert(idx), convert(perm))
+    case ValPointerBlockLength(_, _, ptr, _) => PointerBlockLength(convert(ptr))(blame(e))
+    case ValPointerBlockOffset(_, _, ptr, _) => PointerBlockOffset(convert(ptr))(blame(e))
+    case ValPointerLength(_, _, ptr, _) => PointerLength(convert(ptr))(blame(e))
+    case ValPolarityDependent(_, _, onInhale, _, onExhale, _) => PolarityDependent(convert(onInhale), convert(onExhale))
+  }
+
+  def convert(implicit v: ValBindingContext): (Variable[G], Seq[Expr[G]]) = v match {
+    case ValRangeBinding(t, id, _, from, _, to) =>
+      val variable = new Variable[G](convert(t))(SourceNameOrigin(convert(id), origin(id)))
+      val cond = SeqMember[G](Local(variable.ref), Range(convert(from), convert(to)))
+      (variable, Seq(cond))
+    case ValNormalBinding(arg) =>
+      (convert(arg), Nil)
+  }
+
+  def convert(implicit vs: ValBindingsContext): (Seq[Variable[G]], Seq[Expr[G]]) = vs match {
+    case ValBindings0(binding) =>
+      val (v, cs) = convert(binding)
+      (Seq(v), cs)
+    case ValBindings1(binding, _, bindings) =>
+      val (v, cs) = convert(binding)
+      val (vs, ds) = convert(bindings)
+      (v +: vs, cs ++ ds)
+  }
+
+  def convert(implicit e: ValPrimaryBinderContext): Expr[G] = e match {
+    case ValQuantifier(_, symbol, bindings, _, bodyOrCond, maybeBody, _) =>
+      val (variables, bindingConds) = convert(bindings)
+      val (bodyConds, body) = maybeBody match {
+        case Some(ValBinderCont0(_, body)) => (Seq(convert(bodyOrCond)), convert(body))
+        case None => (Nil, convert(bodyOrCond))
+      }
+      val conds = bindingConds ++ bodyConds
+      symbol match {
+        case ValForallSymb(_) => Forall(variables, Nil, implies(conds, body))
+        case ValStarallSymb(_) => Starall(variables, Nil, implies(conds, body))(blame(e))
+        case ValExistsSymb(_) => Exists(variables, Nil, foldAnd(conds :+ body))
+      }
+    case ValLet(_, _, t, id, _, v, _, body, _) =>
+      Let(new Variable(convert(t))(SourceNameOrigin(convert(id), origin(id))), convert(v), convert(body))
+    case ValForPerm(_, _, bindings, _, loc, _, body, _) =>
+      ForPerm(convert(bindings), AmbiguousLocation(convert(loc))(blame(loc))(origin(loc)), convert(body))
+  }
+
+  def convert(implicit e: ValPrimaryVectorContext): Expr[G] = e match {
+    case ValSum(_, _, t, id, _, cond, _, body, _) =>
+      val binding = new Variable(convert(t))(SourceNameOrigin(convert(id), origin(id)))
+      Sum(Seq(binding), convert(cond), convert(body))
+    case ValVectorSum(_, _, rng, _, vec, _) => VectorSum(convert(rng), convert(vec))
+    case ValVectorCmp(_, _, left, _, right, _) => VectorCompare(convert(left), convert(right))
+    case ValVectorRep(_, _, inner, _) => VectorRepeat(convert(inner))
+    case ValMatrixSum(_, _, rng, _, mat, _) => MatrixSum(convert(rng), convert(mat))
+    case ValMatrixCmp(_, _, left, _, right, _) => MatrixCompare(convert(left), convert(right))
+    case ValMatrixRep(_, _, inner, _) => MatrixRepeat(convert(inner))
+  }
+
+  def convert(implicit e: ValPrimaryReducibleContext): Expr[G] = ??(e)
+
+  def convert(implicit e: ValPrimaryThreadContext): Expr[G] = e match {
+    case ValIdle(_, _, thread, _) => IdleToken(convert(thread))
+    case ValRunning(_, _, thread, _) => JoinToken(convert(thread))
+  }
+
+  def convert(implicit e: ValPrimaryContextContext): Expr[G] = e match {
+    case ValPrimaryContext0("\\result") => AmbiguousResult()
+    case ValPrimaryContext1("\\current_thread") => CurrentThreadId()
+    case ValPrimaryContext2("\\ltid") => LocalThreadId()
+    case ValPrimaryContext3("\\gtid") => GlobalThreadId()
+  }
+
+  def convert(implicit e: ValPrimaryContext): Expr[G] = e match {
+    case ValPrimary0(inner) => convert(inner)
+    case ValPrimary1(inner) => convert(inner)
+    case ValPrimary2(inner) => convert(inner)
+    case ValPrimary3(inner) => convert(inner)
+    case ValPrimary4(inner) => convert(inner)
+    case ValPrimary5(inner) => convert(inner)
+    case ValPrimary6(inner) => convert(inner)
+    case ValPrimary7(inner) => convert(inner)
+    case ValPrimary8(inner) => convert(inner)
+    case ValPrimary9(inner) => convert(inner)
+    case ValAny(_) => Any()(blame(e))
+    case ValFunctionOf(_, inner, _, names, _) => FunctionOf(new UnresolvedRef[G, Variable[G]](convert(inner)), convert(names).map(new UnresolvedRef[G, Variable[G]](_)))
+    case ValInlinePattern(open, pattern, _) =>
+      val groupText = open.filter(_.isDigit)
+      InlinePattern(convert(pattern), open.count(_ == '<'), if (groupText.isEmpty) 0 else groupText.toInt)
+    case ValUnfolding(_, predExpr, _, body) => Unfolding(convert(predExpr), convert(body))(blame(e))
+    case ValOld(_, _, expr, _) => Old(convert(expr), at = None)(blame(e))
+    case ValOldLabeled(_, _, label, _, _, expr, _) => Old(convert(expr), at = Some(new UnresolvedRef[G, LabelDecl[G]](convert(label))))(blame(e))
+    case ValTypeof(_, _, expr, _) => TypeOf(convert(expr))
+    case ValTypeValue(_, _, t, _) => TypeValue(convert(t))
+    case ValHeld(_, _, obj, _) => Held(convert(obj))
+    case ValCommitted(_, _, obj, _) => Committed(convert(obj))(blame(e))
+    case ValIdEscape(text) => local(e, text.substring(1, text.length - 1))
+    case ValSharedMemSize(_, _, ptr, _) => SharedMemSize(convert(ptr))
+    case ValNdIndex(_, _, firstIndex, _, firstDim, parsePairs, _) =>
+      val pairs = parsePairs.map(convert(_))
+      val indices = convert(firstIndex) +: pairs.map(_._1)
+      val dims = convert(firstDim) +: pairs.map(_._2)
+      NdIndex(indices, dims)
+    case ValNdLIndex(_, _, indices, _, dims, _) =>
+      val allIndices = convert(indices)
+      NdPartialIndex(allIndices.init, allIndices.last, convert(dims))
+    case ValNdLength(_, _, dims, _) => NdLength(convert(dims))
+  }
+
+  def convert(implicit e: ValExprPairContext): (Expr[G], Expr[G]) = e match {
+    case ValExprPair0(_, e1, _, e2) => (convert(e1), convert(e2))
+  }
+
+  def convert(implicit e: ValExprContext): Expr[G] = e match {
+    case ValExpr0(inner) => convert(inner)
+    case ValExpr1(inner) => convert(inner)
+  }
+
+  def convert(implicit id: ValIdentifierContext): String = id match {
+    case ValIdentifier0(inner) => convertText(inner)
+    case ValIdentifier1(ValKeywordNonExpr0(text)) => text
+    case ValIdentifier2(text) => text.substring(1, text.length - 1)
+  }
+
+  def convertText(implicit res: ValKeywordExprContext): String = res match {
+    case ValNonePerm(_) => "none"
+    case ValWrite(_) => "write"
+    case ValRead(_) => "read"
+    case ValNoneOption(_) => "None"
+    case ValEmpty(_) => "empty"
+    case ValTrue(_) => "true"
+    case ValFalse(_) => "false"
+  }
+
+  def convert(implicit res: ValKeywordExprContext): Expr[G] = res match {
+    case ValNonePerm(_) => NoPerm()
+    case ValWrite(_) => WritePerm()
+    case ValRead(_) => ReadPerm()
+    case ValNoneOption(_) => OptNone()
+    case ValEmpty(_) => EmptyProcess()
+    case ValTrue(_) => tt
+    case ValFalse(_) => ff
+  }
+
+  def convert(implicit inv: ValGenericAdtInvocationContext): Expr[G] = inv match {
+    case ValGenericAdtInvocation0(adt, _, typeArgs, _, _, func, _, args, _) =>
+      ADTFunctionInvocation(Some((new UnresolvedRef[G, AxiomaticDataType[G]](convert(adt)), convert(typeArgs))),
+        new UnresolvedRef[G, ADTFunction[G]](convert(func)), args.map(convert(_)).getOrElse(Nil))
+  }
+
+  def evalOrNop(implicit expr: Option[ExpressionContext]): Statement[G] = expr match {
+    case Some(expr) => Eval(convert(expr))(origin(expr))
+    case None =>
+      // PB: strictly speaking it would be nice if we can point to the empty range that indicates the absence of a statement here.
+      Block(Nil)(DiagnosticOrigin)
+  }
+
+}
\ No newline at end of file
diff --git a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala
index f3aa6e288b..9c1e767d3f 100644
--- a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala
+++ b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala
@@ -320,6 +320,7 @@ case class ResolveExpressionSideEffects[Pre <: Generation]() extends Rewriter[Pr
       case assn: SilverLocalAssign[Pre] => rewriteDefault(assn)
       case proof: FramedProof[Pre] => rewriteDefault(proof)
       case _: CStatement[Pre] => throw ExtraNode
+      case _: CPPStatement[Pre] => throw ExtraNode
       case _: JavaStatement[Pre] => throw ExtraNode
     }
   }
diff --git a/src/rewrite/vct/rewrite/adt/ImportADT.scala b/src/rewrite/vct/rewrite/adt/ImportADT.scala
index ed250c978f..f48fa7a41d 100644
--- a/src/rewrite/vct/rewrite/adt/ImportADT.scala
+++ b/src/rewrite/vct/rewrite/adt/ImportADT.scala
@@ -4,7 +4,7 @@ import hre.util.ScopedStack
 import vct.col.ast.RewriteHelpers.RewriteProgram
 import vct.col.ast.`type`.TFloats
 import vct.col.ast.util.Declarator
-import vct.col.ast.{CType, Declaration, GlobalDeclaration, JavaType, PVLType, Program, TAny, TArray, TAxiomatic, TBag, TBool, TBoundedInt, TChar, TClass, TEither, TFloat, TFraction, TInt, TMap, TMatrix, TModel, TNotAValue, TNothing, TNull, TOption, TPointer, TProcess, TRational, TRef, TResource, TSeq, TSet, TString, TTuple, TType, TUnion, TVar, TVoid, TZFraction, Type}
+import vct.col.ast.{CPPType, CType, Declaration, GlobalDeclaration, JavaType, PVLType, Program, TAny, TArray, TAxiomatic, TBag, TBool, TBoundedInt, TChar, TClass, TEither, TFloat, TFraction, TInt, TMap, TMatrix, TModel, TNotAValue, TNothing, TNull, TOption, TPointer, TProcess, TRational, TRef, TResource, TSeq, TSet, TString, TTuple, TType, TUnion, TVar, TVoid, TZFraction, Type}
 import vct.col.typerules.CoercingRewriter
 import vct.col.rewrite.error.ExtraNode
 import vct.col.origin.{Blame, SourceNameOrigin, UnsafeCoercion}
@@ -64,6 +64,7 @@ case object ImportADT {
     case TUnion(ts) => "union$" + ts.map(typeText).mkString("__") + "$"
     case _: JavaType[_] => throw ExtraNode
     case _: CType[_] => throw ExtraNode
+    case _: CPPType[_] => throw ExtraNode
     case _: PVLType[_] => throw ExtraNode
   }
 }
diff --git a/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala
new file mode 100644
index 0000000000..29e663d188
--- /dev/null
+++ b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala
@@ -0,0 +1,263 @@
+package vct.col.rewrite.lang
+
+import com.typesafe.scalalogging.LazyLogging
+import hre.util.ScopedStack
+import vct.col.ast._
+import vct.col.origin._
+import vct.col.ref.Ref
+import vct.col.resolve.ctx._
+import vct.col.resolve.lang.CPP
+import vct.col.rewrite.lang.LangSpecificToCol.NotAValue
+import vct.col.rewrite.{Generation, Rewritten}
+import vct.col.util.AstBuildHelpers._
+import vct.col.util.SuccessionMap
+import vct.result.VerificationError.UserError
+
+case object LangCPPToCol {
+
+  case class WrongCPPType(decl: CPPLocalDeclaration[_]) extends UserError {
+    override def code: String = "wrongCPPType"
+
+    override def text: String =
+      decl.o.messageInContext(s"This declaration has a type that is not supported.")
+  }
+
+  case class CPPDoubleContracted(decl: CPPGlobalDeclaration[_], defn: CPPFunctionDefinition[_]) extends UserError {
+    override def code: String = "multipleContracts"
+
+    override def text: String =
+      Origin.messagesInContext(Seq(
+        defn.o -> "This method has a non-empty contract at its definition, ...",
+        decl.o -> "... but its forward declaration also has a contract.",
+      ))
+  }
+}
+
+case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends LazyLogging {
+  import LangCPPToCol._
+  type Post = Rewritten[Pre]
+  implicit val implicitRewriter: AbstractRewriter[Pre, Post] = rw
+
+  val namespace: ScopedStack[CPPNamespaceDefinition[Pre]] = ScopedStack()
+  val cppFunctionSuccessor: SuccessionMap[CPPFunctionDefinition[Pre], Procedure[Post]] = SuccessionMap()
+  val cppFunctionDeclSuccessor: SuccessionMap[(CPPGlobalDeclaration[Pre], Int), Procedure[Post]] = SuccessionMap()
+  val cppNameSuccessor: SuccessionMap[CPPNameTarget[Pre], Variable[Post]] = SuccessionMap()
+  val cppGlobalNameSuccessor: SuccessionMap[CPPNameTarget[Pre], HeapVariable[Post]] = SuccessionMap()
+  val cppCurrentDefinitionParamSubstitutions: ScopedStack[Map[CPPParam[Pre], CPPParam[Pre]]] = ScopedStack()
+
+  def rewriteUnit(cppUnit: CPPTranslationUnit[Pre]): Unit = {
+    cppUnit.declarations.foreach(rw.dispatch)
+  }
+
+  def rewriteParam(cppParam: CPPParam[Pre]): Unit = {
+    cppParam.drop()
+    val varO = InterpretedOriginVariable(CPP.getDeclaratorInfo(cppParam.declarator).name, cppParam.o)
+
+    val v = new Variable[Post](cppParam.specifiers.collectFirst
+      { case t: CPPSpecificationType[Pre] => rw.dispatch(t.t) }.get)(varO)
+    cppNameSuccessor(RefCPPParam(cppParam)) = v
+    rw.variables.declare(v)
+  }
+
+  def rewriteFunctionDef(func: CPPFunctionDefinition[Pre]): Unit = {
+    func.drop()
+    val info = CPP.getDeclaratorInfo(func.declarator)
+    val returnType = func.specs.collectFirst { case t: CPPSpecificationType[Pre] => rw.dispatch(t.t) }.get
+
+    val (contract, subs: Map[CPPParam[Pre], CPPParam[Pre]]) = func.ref match {
+      case Some(RefCPPGlobalDeclaration(decl, idx)) if decl.decl.contract.nonEmpty =>
+        if (func.contract.nonEmpty) throw CPPDoubleContracted(decl, func)
+
+        val declParams = CPP.getDeclaratorInfo(decl.decl.inits(idx).decl).params.get
+        val defnParams = info.params.get
+
+        (decl.decl.contract, declParams.zip(defnParams).toMap)
+      case _ =>
+        (func.contract, Map.empty)
+    }
+
+    val namedO = InterpretedOriginVariable(CPP.getDeclaratorInfo(func.declarator).name, func.o)
+    val proc =
+      cppCurrentDefinitionParamSubstitutions.having(subs) {
+        rw.globalDeclarations.declare(
+          {
+            val params = rw.variables.collect {
+              info.params.get.foreach(rw.dispatch)
+            }._1
+            rw.labelDecls.scope {
+              new Procedure[Post](
+                returnType = returnType,
+                args = params,
+                outArgs = Nil,
+                typeArgs = Nil,
+                body = Some(rw.dispatch(func.body)),
+                contract = rw.dispatch(contract),
+              )(func.blame)(namedO)
+            }
+          }
+        )
+      }
+
+    cppFunctionSuccessor(func) = proc
+
+    func.ref match {
+      case Some(RefCPPGlobalDeclaration(decl, idx)) =>
+        cppFunctionDeclSuccessor((decl, idx)) = proc
+      case None => // ok
+    }
+  }
+
+  def rewriteGlobalDecl(decl: CPPGlobalDeclaration[Pre]): Unit = {
+    val t = decl.decl.specs.collectFirst { case t: CPPSpecificationType[Pre] => rw.dispatch(t.t) }.get
+    for ((init, idx) <- decl.decl.inits.zipWithIndex if init.ref.isEmpty) {
+      // If the reference is empty, skip the declaration: the definition is used instead.
+      val info = CPP.getDeclaratorInfo(init.decl)
+      info.params match {
+        case Some(params) =>
+          cppFunctionDeclSuccessor((decl, idx)) = rw.globalDeclarations.declare(
+            new Procedure[Post](
+              returnType = t,
+              args = rw.variables.collect {
+                params.foreach(rw.dispatch)
+              }._1,
+              outArgs = Nil,
+              typeArgs = Nil,
+              body = None,
+              contract = rw.dispatch(decl.decl.contract),
+            )(AbstractApplicable)(init.o)
+          )
+        case None =>
+          cppGlobalNameSuccessor(RefCPPGlobalDeclaration(decl, idx)) =
+            rw.globalDeclarations.declare(new HeapVariable(t)(init.o))
+      }
+    }
+  }
+
+  def rewriteLocal(decl: CPPLocalDeclaration[Pre]): Statement[Post] = {
+    decl.drop()
+    val t = decl.decl.specs.collectFirst { case t: CPPSpecificationType[Pre] => rw.dispatch(t.t) }.get
+    decl.decl.specs.foreach {
+      case _: CPPSpecificationType[Pre] =>
+      case _ => throw WrongCPPType(decl)
+    }
+
+    // LangTypesToCol makes it so that each declaration only has one init
+    val init = decl.decl.inits.head
+
+    val info = CPP.getDeclaratorInfo(init.decl)
+    val varO: Origin = InterpretedOriginVariable(info.name, init.o)
+    t match {
+      case cta @ CPPTArray(Some(size), t) =>
+        if (init.init.isDefined) throw WrongCPPType(decl)
+        implicit val o: Origin = init.o
+        val v = new Variable[Post](TArray(t))(varO)
+        cppNameSuccessor(RefCPPLocalDeclaration(decl, 0)) = v
+        val newArr = NewArray[Post](t, Seq(size), 0)(cta.blame)
+        Block(Seq(LocalDecl(v), assignLocal(v.get, newArr)))
+      case _ =>
+        val v = new Variable[Post](t)(varO)
+        cppNameSuccessor(RefCPPLocalDeclaration(decl, 0)) = v
+        implicit val o: Origin = init.o
+        init.init
+          .map(value => Block(Seq(LocalDecl(v), assignLocal(v.get, rw.dispatch(value)))))
+          .getOrElse(LocalDecl(v))
+    }
+  }
+
+  def rewriteNamespaceDef(ns: CPPNamespaceDefinition[Pre]): Unit = {
+    ns.drop()
+    namespace.having(ns) {
+      // Do not enter a scope, so methods of the namespace are declared globally to the program.
+      ns.declarations.foreach(rw.dispatch)
+    }
+  }
+
+  def result(ref: RefCPPFunctionDefinition[Pre])(implicit o: Origin): Expr[Post] =
+    Result[Post](cppFunctionSuccessor.ref(ref.decl))
+
+  def result(ref: RefCPPGlobalDeclaration[Pre])(implicit o: Origin): Expr[Post] = {
+    val maybeDefinition = ref.decls.decl.inits(ref.initIdx).ref
+    maybeDefinition match {
+      case Some(defn) => Result[Post](cppFunctionSuccessor.ref(defn.decl))
+      case None => Result[Post](cppFunctionDeclSuccessor.ref((ref.decls, ref.initIdx)))
+    }
+  }
+
+  def local(local: CPPLocal[Pre]): Expr[Post] = {
+    implicit val o: Origin = local.o
+    local.ref.get match {
+      case RefAxiomaticDataType(_) => throw NotAValue(local)
+      case RefVariable(decl) => Local(rw.succ(decl))
+      case RefModelField(decl) => ModelDeref[Post](rw.currentThis.top, rw.succ(decl))(local.blame)
+      case ref: RefCPPParam[Pre] =>
+        if (cppCurrentDefinitionParamSubstitutions.nonEmpty)
+          Local(cppNameSuccessor.ref(RefCPPParam(cppCurrentDefinitionParamSubstitutions.top.getOrElse(ref.decl, ref.decl))))
+        else
+          Local(cppNameSuccessor.ref(ref))
+      case RefCPPFunctionDefinition(_) => throw NotAValue(local)
+      case ref @ RefCPPGlobalDeclaration(decl, initIdx) =>
+        CPP.getDeclaratorInfo(decl.decl.inits(initIdx).decl).params match {
+          case None => DerefHeapVariable[Post](cppGlobalNameSuccessor.ref(ref))(local.blame)
+          case Some(_) => throw NotAValue(local)
+        }
+      case ref: RefCPPLocalDeclaration[Pre] => Local(cppNameSuccessor.ref(ref))
+    }
+  }
+
+  def invocation(inv: CPPInvocation[Pre]): Expr[Post] = {
+    val CPPInvocation(applicable, args, givenMap, yields) = inv
+    implicit val o: Origin = inv.o
+    inv.ref.get match {
+      case RefFunction(decl) =>
+        FunctionInvocation[Post](rw.succ(decl), args.map(rw.dispatch), Nil,
+          givenMap.map { case (Ref(v), e) => (rw.succ(v), rw.dispatch(e)) },
+          yields.map { case (e, Ref(v)) => (rw.dispatch(e), rw.succ(v)) })(inv.blame)
+      case RefProcedure(decl) =>
+        ProcedureInvocation[Post](rw.succ(decl), args.map(rw.dispatch), Nil, Nil,
+          givenMap.map { case (Ref(v), e) => (rw.succ(v), rw.dispatch(e)) },
+          yields.map { case (e, Ref(v)) => (rw.dispatch(e), rw.succ(v)) })(inv.blame)
+      case RefPredicate(decl) =>
+        PredicateApply[Post](rw.succ(decl), args.map(rw.dispatch), WritePerm())
+      case RefInstanceFunction(decl) => ???
+      case RefInstanceMethod(decl) => ???
+      case RefInstancePredicate(decl) => ???
+      case RefADTFunction(decl) =>
+        ADTFunctionInvocation[Post](None, rw.succ(decl), args.map(rw.dispatch))
+      case RefModelProcess(decl) =>
+        ProcessApply[Post](rw.succ(decl), args.map(rw.dispatch))
+      case RefModelAction(decl) =>
+        ActionApply[Post](rw.succ(decl), args.map(rw.dispatch))
+      case BuiltinInstanceMethod(f) => ???
+      case ref: RefCPPFunctionDefinition[Pre] =>
+        ProcedureInvocation[Post](cppFunctionSuccessor.ref(ref.decl), args.map(rw.dispatch), Nil, Nil,
+          givenMap.map { case (Ref(v), e) => (rw.succ(v), rw.dispatch(e)) },
+          yields.map { case (e, Ref(v)) => (rw.dispatch(e), rw.succ(v)) })(inv.blame)
+      case e: RefCPPGlobalDeclaration[Pre] => globalInvocation(e, inv)
+      case RefProverFunction(decl) => ProverFunctionInvocation(rw.succ(decl), args.map(rw.dispatch))
+    }
+  }
+
+  def globalInvocation(e: RefCPPGlobalDeclaration[Pre], inv: CPPInvocation[Pre]): Expr[Post] = {
+    val CPPInvocation(_, args, givenMap, yields) = inv
+    val RefCPPGlobalDeclaration(decls, initIdx) = e
+    implicit val o: Origin = inv.o
+
+    val arg = if (args.size == 1) {
+      args.head match {
+        case IntegerValue(i) if i >= 0 && i < 3 => Some(i.toInt)
+        case _ => None
+      }
+    } else None
+    (e.name, arg) match {
+      case _ => ProcedureInvocation[Post](cppFunctionDeclSuccessor.ref((decls, initIdx)), args.map(rw.dispatch), Nil, Nil,
+        givenMap.map { case (Ref(v), e) => (rw.succ(v), rw.dispatch(e)) },
+        yields.map { case (e, Ref(v)) => (rw.dispatch(e), rw.succ(v)) })(inv.blame)
+    }
+  }
+
+  def arrayType(t: CPPTArray[Pre]): Type[Post] = {
+    // TODO: we should not use pointer here
+    TPointer(rw.dispatch(t.innerType))
+  }
+
+}
\ No newline at end of file
diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala
index e62cf0bcfe..396fcb6e15 100644
--- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala
@@ -9,10 +9,7 @@ import vct.col.origin._
 import vct.col.resolve.ctx._
 import vct.col.resolve.lang.Java
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
-import vct.col.resolve._
-import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, RewriterBuilderArg}
 import vct.result.VerificationError.UserError
-import vct.col.util.SuccessionMap
 
 case object LangSpecificToCol extends RewriterBuilder {
   override def key: String = "langSpecific"
@@ -35,6 +32,7 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
   val java: LangJavaToCol[Pre] = LangJavaToCol(this)
   val bip: LangBipToCol[Pre] = LangBipToCol(this)
   val c: LangCToCol[Pre] = LangCToCol(this)
+  val cpp: LangCPPToCol[Pre] = LangCPPToCol(this)
   val pvl: LangPVLToCol[Pre] = LangPVLToCol(this)
   val silver: LangSilverToCol[Pre] = LangSilverToCol(this)
   val llvm: LangLLVMToCol[Pre] = LangLLVMToCol(this)
@@ -67,6 +65,14 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
     case func: CFunctionDefinition[Pre] => c.rewriteFunctionDef(func)
     case decl: CGlobalDeclaration[Pre] => c.rewriteGlobalDecl(decl)
     case decl: CLocalDeclaration[Pre] => ???
+
+    case unit: CPPTranslationUnit[Pre] => cpp.rewriteUnit(unit)
+    case cppParam: CPPParam[Pre] => cpp.rewriteParam(cppParam)
+    case func: CPPFunctionDefinition[Pre] => cpp.rewriteFunctionDef(func)
+    case ns: CPPNamespaceDefinition[Pre] => cpp.rewriteNamespaceDef(ns)
+    case decl: CPPGlobalDeclaration[Pre] => cpp.rewriteGlobalDecl(decl)
+    case decl: CPPLocalDeclaration[Pre] => ???
+
     case func: LlvmFunctionDefinition[Pre] => llvm.rewriteFunctionDef(func)
 
     case cls: Class[Pre] =>
@@ -103,6 +109,7 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
     case JavaLocalDeclarationStatement(locals: JavaLocalDeclaration[Pre]) => java.initLocal(locals)
 
     case CDeclarationStatement(decl) => c.rewriteLocal(decl)
+    case CPPDeclarationStatement(decl) => cpp.rewriteLocal(decl)
     case goto: CGoto[Pre] => c.rewriteGoto(goto)
     case barrier: GpgpuBarrier[Pre] => c.gpuBarrier(barrier)
 
@@ -115,6 +122,8 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
       result.ref.get match {
         case ref: RefCFunctionDefinition[Pre] => c.result(ref)
         case ref: RefCGlobalDeclaration[Pre] => c.result(ref)
+        case ref: RefCPPFunctionDefinition[Pre] => cpp.result(ref)
+        case ref: RefCPPGlobalDeclaration[Pre] => cpp.result(ref)
         case ref: RefLlvmFunctionDefinition[Pre] => llvm.result(ref)
         case RefFunction(decl) => Result[Post](anySucc(decl))
         case RefProcedure(decl) => Result[Post](anySucc(decl))
@@ -155,6 +164,9 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
     case global: GlobalThreadId[Pre] => c.cudaGlobalThreadId(global)
     case cast: CCast[Pre] => c.cast(cast)
 
+    case local: CPPLocal[Pre] => cpp.local(local)
+    case inv: CPPInvocation[Pre] => cpp.invocation(inv)
+
     case inv: SilverPartialADTFunctionInvocation[Pre] => silver.adtInvocation(inv)
     case map: SilverUntypedNonemptyLiteralMap[Pre] => silver.nonemptyMap(map)
 
@@ -169,6 +181,7 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
     case t: JavaTClass[Pre] => java.classType(t)
     case t: CTPointer[Pre] => c.pointerType(t)
     case t: CTArray[Pre] => c.arrayType(t)
+    case t: CPPTArray[Pre] => cpp.arrayType(t)
     case other => rewriteDefault(other)
   }
 }
diff --git a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala
index ae5ffe4588..2c9f5e6da6 100644
--- a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala
@@ -1,13 +1,13 @@
 package vct.col.rewrite.lang
 
+import vct.col.ast.RewriteHelpers._
 import vct.col.ast._
 import vct.col.origin.Origin
-import vct.col.resolve.ctx.{RefAxiomaticDataType, RefClass, RefEnum, RefJavaClass, RefModel, RefVariable, SpecTypeNameTarget, RefProverType}
-import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten}
-import vct.col.ast.RewriteHelpers._
-import vct.col.rewrite.lang.LangTypesToCol.IncompleteTypeArgs
 import vct.col.ref.{Ref, UnresolvedRef}
-import vct.col.resolve.lang.C
+import vct.col.resolve.ctx._
+import vct.col.resolve.lang.{C, CPP}
+import vct.col.rewrite.lang.LangTypesToCol.IncompleteTypeArgs
+import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten}
 import vct.result.VerificationError.UserError
 
 import scala.reflect.ClassTag
@@ -62,6 +62,8 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] {
         }
       case t @ CPrimitiveType(specs) =>
         dispatch(C.getPrimitiveType(specs, context = Some(t)))
+      case t@CPPPrimitiveType(specs) =>
+        dispatch(CPP.getPrimitiveType(specs, context = Some(t)))
       case t @ SilverPartialTAxiomatic(Ref(adt), partialTypeArgs) =>
         if(partialTypeArgs.map(_._1.decl).toSet != adt.typeArgs.toSet)
           throw IncompleteTypeArgs(t)
@@ -94,6 +96,29 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] {
     (newSpecifiers, newDeclarator)
   }
 
+  def normalizeCPPDeclaration(specifiers: Seq[CPPDeclarationSpecifier[Pre]],
+                            declarator: CPPDeclarator[Pre],
+                            context: Option[Node[Pre]] = None)
+                           (implicit o: Origin): (Seq[CPPDeclarationSpecifier[Post]], CPPDeclarator[Post]) = {
+    val info = CPP.getDeclaratorInfo(declarator)
+    val baseType = CPP.getPrimitiveType(specifiers, context)
+    val otherSpecifiers = specifiers.filter(!_.isInstanceOf[CPPTypeSpecifier[Pre]]).map(dispatch)
+    val newSpecifiers = CPPSpecificationType[Post](dispatch(info.typeOrReturnType(baseType))) +: otherSpecifiers
+    val newDeclarator = info.params match {
+      case Some(params) =>
+        // PB TODO: varargs is discarded here.
+        CPPTypedFunctionDeclarator[Post](
+          cPPParams.dispatch(params),
+          varargs = false,
+          CPPName(info.name)
+        )
+      case None =>
+        CPPName[Post](info.name)
+    }
+
+    (newSpecifiers, newDeclarator)
+  }
+
   override def dispatch(decl: Declaration[Pre]): Unit = decl match {
     case param: CParam[Pre] =>
       val (specs, decl) = normalizeCDeclaration(param.specifiers, param.declarator, context = Some(param))(param.o)
@@ -128,6 +153,39 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] {
       implicit val o: Origin = declaration.o
       val (specs, decl) = normalizeCDeclaration(declaration.specs, declaration.declarator, context = Some(declaration))
       globalDeclarations.declare(declaration.rewrite(specs = specs, declarator = decl))
+    case param: CPPParam[Pre] =>
+      val (specs, decl) = normalizeCPPDeclaration(param.specifiers, param.declarator, context = Some(param))(param.o)
+      cPPParams.declare(new CPPParam(specs, decl)(param.o))
+    case declaration: CPPLocalDeclaration[Pre] =>
+      declaration.decl.inits.foreach(init => {
+        implicit val o: Origin = init.o
+        val (specs, decl) = normalizeCPPDeclaration(declaration.decl.specs, init.decl, context = Some(declaration))
+        cPPLocalDeclarations.declare(declaration.rewrite(
+          decl = declaration.decl.rewrite(
+            specs = specs,
+            inits = Seq(
+              CPPInit(decl, init.init.map(dispatch)),
+            ),
+          ),
+        ))
+      })
+    case declaration: CPPGlobalDeclaration[Pre] =>
+      declaration.decl.inits.foreach(init => {
+        implicit val o: Origin = init.o
+        val (specs, decl) = normalizeCPPDeclaration(declaration.decl.specs, init.decl, context = Some(declaration))
+        globalDeclarations.declare(declaration.rewrite(
+          decl = declaration.decl.rewrite(
+            specs = specs,
+            inits = Seq(
+              CPPInit(decl, init.init.map(dispatch)),
+            ),
+          ),
+        ))
+      })
+    case declaration: CPPFunctionDefinition[Pre] =>
+      implicit val o: Origin = declaration.o
+      val (specs, decl) = normalizeCPPDeclaration(declaration.specs, declaration.declarator, context = Some(declaration))
+      globalDeclarations.declare(declaration.rewrite(specs = specs, declarator = decl))
     case cls: JavaClass[Pre] =>
       rewriteDefault(cls)
     case other => rewriteDefault(other)
@@ -137,6 +195,9 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] {
     case CDeclarationStatement(local) =>
       val (locals, _) = cLocalDeclarations.collect { dispatch(local) }
       Block(locals.map(CDeclarationStatement(_)(stat.o)))(stat.o)
+    case CPPDeclarationStatement(local) =>
+      val (locals, _) = cPPLocalDeclarations.collect { dispatch(local) }
+      Block(locals.map(CPPDeclarationStatement(_)(stat.o)))(stat.o)
 
     case other => rewriteDefault(other)
   }
diff --git a/src/viper/viper/api/transform/ColToSilver.scala b/src/viper/viper/api/transform/ColToSilver.scala
index d44cf30354..928de29efd 100644
--- a/src/viper/viper/api/transform/ColToSilver.scala
+++ b/src/viper/viper/api/transform/ColToSilver.scala
@@ -1,7 +1,7 @@
 package viper.api.transform
 
 import hre.util.ScopedStack
-import vct.col.ast.{AmbiguousLocation, ArrayLocation, FieldLocation, InstancePredicateLocation, ModelLocation, PointerLocation, PredicateLocation, SilverFieldLocation}
+import vct.col.ast.{PredicateLocation, SilverFieldLocation}
 import vct.col.origin.{AccountedDirection, FailLeft, FailRight}
 import vct.col.ref.Ref
 import vct.col.util.AstBuildHelpers.unfoldStar
@@ -253,6 +253,7 @@ case class ColToSilver(program: col.Program[_]) {
 
   def typ(t: col.Type[_]): silver.Type = t match {
     case col.TBool() => silver.Bool
+    case col.TSYCLQueue() => silver.Ref
     case col.TInt() => silver.Int
     case col.TRational() => silver.Perm
     case col.TRef() => silver.Ref
diff --git a/test/main/vct/test/integration/examples/CPPSpec.scala b/test/main/vct/test/integration/examples/CPPSpec.scala
new file mode 100644
index 0000000000..c51275bf4a
--- /dev/null
+++ b/test/main/vct/test/integration/examples/CPPSpec.scala
@@ -0,0 +1,25 @@
+package vct.test.integration.examples
+
+import vct.test.integration.helper.VercorsSpec
+
+class CPPSpec extends VercorsSpec {
+  vercors should verify using silicon example "concepts/cpp/Arrays.cpp"
+  vercors should verify using silicon example "concepts/cpp/Conditionals.cpp"
+  vercors should verify using silicon example "concepts/cpp/Loops.cpp"
+  vercors should verify using silicon example "concepts/cpp/Namespaces.cpp"
+  vercors should error withCode "noSuchName" example "concepts/cpp/NamespacesDoNotFindWithoutNamespacePrefix.cpp"
+  vercors should verify using silicon example "concepts/cpp/Operators.cpp"
+  vercors should verify using silicon example "concepts/cpp/Pointers.cpp"
+  vercors should verify using silicon example "concepts/cpp/Scoping.cpp"
+  vercors should verify using silicon example "concepts/cpp/Types.cpp"
+
+  vercors should verify using silicon example "concepts/cpp/methods/AbstractMethod.cpp"
+  vercors should verify using silicon example "concepts/cpp/methods/ContextAndContextEverywhere.cpp"
+  vercors should verify using silicon example "concepts/cpp/methods/Decreases.cpp"
+  vercors should verify using silicon example "concepts/cpp/methods/GhostMethodsAndVariables.cpp"
+  vercors should verify using silicon example "concepts/cpp/methods/GhostParamsAndResults.cpp"
+  vercors should verify using silicon example "concepts/cpp/methods/InlineFunction.cpp"
+  vercors should verify using silicon example "concepts/cpp/methods/Permissions.cpp"
+  vercors should verify using silicon example "concepts/cpp/methods/Predicates.cpp"
+  vercors should verify using silicon example "concepts/cpp/methods/PureGhostMethod.cpp"
+}
\ No newline at end of file
diff --git a/test/main/vct/test/integration/examples/SYCLSpec.scala b/test/main/vct/test/integration/examples/SYCLSpec.scala
new file mode 100644
index 0000000000..00c66b076a
--- /dev/null
+++ b/test/main/vct/test/integration/examples/SYCLSpec.scala
@@ -0,0 +1,7 @@
+package vct.test.integration.examples
+
+import vct.test.integration.helper.VercorsSpec
+
+class SYCLSpec extends VercorsSpec {
+  vercors should verify using silicon example "concepts/sycl/MethodResolving.cpp"
+}
\ No newline at end of file
diff --git a/test/main/vct/test/integration/meta/ExampleCoverage.scala b/test/main/vct/test/integration/meta/ExampleCoverage.scala
index a0de490ab5..816df554d6 100644
--- a/test/main/vct/test/integration/meta/ExampleCoverage.scala
+++ b/test/main/vct/test/integration/meta/ExampleCoverage.scala
@@ -14,6 +14,7 @@ class ExampleCoverage extends AnyFlatSpec {
       new CIncludeSpec(),
       new ClassesSpec(),
       new CounterSpec(),
+      new CPPSpec(),
       new DemoSpec(),
       new FinalConstExprSpec(),
       new ExtractSpec(),
@@ -38,6 +39,7 @@ class ExampleCoverage extends AnyFlatSpec {
       new SilverDomainSpec(),
       new SmtSpec(),
       new SummationSpec(),
+      new SYCLSpec(),
       new TechnicalAbruptSpec(),
       new TechnicalEnumSpec(),
       new TechnicalFloatSpec(),