Restricted & to only be allowed to be combined with sycl::handler

examples/concepts/sycl/fullExamples/MatrixTransposeWithF.cpp

@@ -1,6 +1,6 @@
 #include <sycl/sycl.hpp>
 
-// Helper function which calculates a linear index out a row and column
+// Helper function which calculates a linear index out of a row and a column
 /*@
 	requires row >= 0 && row < rows && col >= 0 && col < cols;
 	ensures \result == col + (row * cols);

src/col/vct/col/resolve/lang/CPP.scala

@@ -11,7 +11,7 @@ import vct.result.VerificationError.UserError
 case object CPP {
   implicit private val o: Origin = DiagnosticOrigin
 
-  private case class CPPTypeNotSupported(node: Option[Node[_]]) extends UserError {
+  case class CPPTypeNotSupported(node: Option[Node[_]]) extends UserError {
     override def code: String = "cppTypeNotSupported"
 
     override def text: String = {
@@ -40,7 +40,7 @@ case object CPP {
     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)
+  case class DeclaratorInfo[G](params: Option[Seq[CPPParam[G]]], typeOrReturnType: Type[G] => Type[G], name: String, isReference: Boolean = false)
 
   def getDeclaratorInfo[G](decl: CPPDeclarator[G], isParam: Boolean = false): DeclaratorInfo[G] = decl match {
     case CPPAddressingDeclarator(operators, inner) =>
@@ -50,7 +50,9 @@ case object CPP {
         DeclaratorInfo(
           innerInfo.params,
           t => innerInfo.typeOrReturnType(t),
-          innerInfo.name)
+          innerInfo.name,
+          isReference = true
+        )
       } else if (operators.collectFirst({ case x: CPPReference[G] => x }).isDefined) {
         // Do not support multiple &, or & later in the sequence
         throw CPPTypeNotSupported(Some(decl))

src/rewrite/vct/rewrite/lang/LangTypesToCol.scala

@@ -1,15 +1,14 @@
 package vct.rewrite.lang
 
 import vct.col.ast.RewriteHelpers._
-import vct.col.ast.{TModel, _}
+import vct.col.ast._
 import vct.col.origin.Origin
 import vct.col.ref.{Ref, UnresolvedRef}
 import vct.col.resolve.ctx._
 import vct.col.resolve.lang.{C, CPP}
-import vct.rewrite.lang.LangTypesToCol.{EmptyInlineDecl, IncompleteTypeArgs}
-import vct.col.typerules.Types
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten}
 import vct.result.VerificationError.UserError
+import vct.rewrite.lang.LangTypesToCol.{EmptyInlineDecl, IncompleteTypeArgs}
 
 import scala.reflect.ClassTag
 
@@ -109,6 +108,10 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] {
                            (implicit o: Origin): (Seq[CPPDeclarationSpecifier[Post]], CPPDeclarator[Post]) = {
     val info = CPP.getDeclaratorInfo(declarator, context.getOrElse(false).isInstanceOf[CPPParam[Pre]])
     val baseType = CPP.getBaseTypeFromSpecs(specifiers, context)
+    if (info.isReference && !baseType.isInstanceOf[SYCLTHandler[Pre]]) {
+      // Only accept reference parameters for type sycl::handler, as we only need & support for a lambda method with that parameter
+      throw CPP.CPPTypeNotSupported(Some(declarator))
+    }
     val otherSpecifiers = specifiers.filter(!_.isInstanceOf[CPPTypeSpecifier[Pre]]).map(dispatch)
     val newSpecifiers = CPPSpecificationType[Post](dispatch(info.typeOrReturnType(baseType))) +: otherSpecifiers
     val newDeclarator = info.params match {

test/main/vct/test/integration/examples/SYCLFullProgramsSpec.scala

@@ -3,7 +3,7 @@ package vct.test.integration.examples
 import vct.test.integration.helper.VercorsSpec
 
 class SYCLFullProgramsSpec extends VercorsSpec {
-//  vercors should verify using silicon flag "--no-infer-heap-context-into-frame" example "concepts/sycl/fullExamples/VectorAdd.cpp"
+  vercors should verify using silicon flag "--no-infer-heap-context-into-frame" example "concepts/sycl/fullExamples/VectorAdd.cpp"
 
   // About 1 in 5 times this test will fail, because then VerCors fails to prove the pre-conditions of the second kernel even though they are true
   vercors should verify using silicon flag "--no-infer-heap-context-into-frame" example "concepts/sycl/fullExamples/MatrixTransposeWithF.cpp"