Changes to loop contracts init values for structs

src/col/vct/col/ast/Node.scala

@@ -906,7 +906,7 @@ final case class CSpecificationType[G](t: Type[G])(implicit val o: Origin) exten
 
 final case class CStructDeclaration[G](name: Option[String], decl: Seq[CStructMemberDeclarator[G]])(implicit val o: Origin) extends CTypeSpecifier[G] with CStructDeclarationImpl[G]
 final case class CStructSpecifier[G](name: String)(implicit val o: Origin) extends CTypeSpecifier[G] with CStructSpecifierImpl[G] {
-  var ref: Option[CStructTarget[G]] = None
+  var ref: Option[RefCStruct[G]] = None
 }
 final case class CStructMemberDeclarator[G](specs: Seq[CDeclarationSpecifier[G]], decls: Seq[CDeclarator[G]])(implicit val o: Origin) extends Declaration[G] with CStructMemberDeclaratorImpl[G]
 

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

@@ -75,7 +75,7 @@ case object C {
       case Seq(CBool()) => TBool()
       case Seq(defn @ CTypedefName(_)) => Types.notAValue(defn.ref.get)
       case Seq(CSpecificationType(typ)) => typ
-      case Seq(defn @ CStructSpecifier(_)) => Types.notAValue(defn.ref.get)
+      case Seq(defn @ CStructSpecifier(_)) => CTStruct(defn.ref.get.decl.ref)
       case spec +: _ => throw CTypeNotSupported(context.orElse(Some(spec)))
       case _ => throw CTypeNotSupported(context)
     }
@@ -94,9 +94,9 @@ case object C {
       case target: CTypeNameTarget[G] if target.name == name => target
     }
 
-  def findCStruct[G](name: String, ctx: TypeResolutionContext[G]): Option[CStructTarget[G]] =
+  def findCStruct[G](name: String, ctx: TypeResolutionContext[G]): Option[RefCStruct[G]] =
     ctx.stack.flatten.collectFirst {
-      case target: CStructTarget[G] if target.name == name => target
+      case target: RefCStruct[G] if target.name == name => target
     }
 
   def findCName[G](name: String, ctx: ReferenceResolutionContext[G]): Option[CNameTarget[G]] =

src/rewrite/vct/rewrite/CollectLocalDeclarations.scala

@@ -27,13 +27,6 @@ case class CollectLocalDeclarations[Pre <: Generation]() extends Rewriter[Pre] {
         dispatch(impl)
       }
       Scope[Post](newVars, newImpl)(stat.o)
-    case Loop(_, _, _, _, _: Scope[Pre]) => rewriteDefault(stat)
-    case loop@Loop(_, _, _, _, body) =>
-      val (newVars, newBody) = variables.collect {
-        dispatch(body)
-      }
-      val bodyScope = Scope[Post](newVars, newBody)(body.o)
-      loop.rewrite(body = bodyScope)
     case other => rewriteDefault(other)
   }
 }

src/rewrite/vct/rewrite/IterationContractToParBlock.scala

@@ -50,6 +50,11 @@ case class IterationContractToParBlock[Pre <: Generation]() extends Rewriter[Pre
 
       implicit val o: Origin = loop.o
       currentIterationVariables.having(v) {
+        val (newVars, newBody) = variables.collect {
+          dispatch(body)
+        }
+        val bodyScope = Scope[Post](newVars, newBody)(body.o)
+
         sendDecls.scope {
           ParStatement(
             ParBlock(
@@ -58,7 +63,8 @@ case class IterationContractToParBlock[Pre <: Generation]() extends Rewriter[Pre
               requires = dispatch(requires),
               ensures = dispatch(ensures),
               context_everywhere = dispatch(context_everywhere),
-              content = dispatch(body),
+              content =
+                bodyScope,
             )(contract.blame)
           )
         }

src/rewrite/vct/rewrite/PrettifyBlocks.scala

@@ -39,8 +39,8 @@ case class PrettifyBlocks[Pre <: Generation]() extends Rewriter[Pre] {
         collectVariables(body, extra = locals)
       }
 
-    case loop: Loop[Pre] =>
-      loop.rewrite(body = collectVariables(loop.body))
+    case loop @ Loop(_, _, _, _: IterationContract[Pre], body) =>
+      loop.rewrite(body = collectVariables(body))
 
     case vec: VecBlock[Pre] =>
       vec.rewrite(content = collectVariables(vec.content))

src/rewrite/vct/rewrite/lang/LangCToCol.scala

@@ -788,16 +788,20 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz
       case _ => throw WrongStructType(decl)
     }
 
-    val target = ref.decl
     implicit val o: Origin = init.o
-    val targetClass: Class[Post] = cStructSuccessor(target)
+    val targetClass: Class[Post] = cStructSuccessor(ref.decl)
     val t = TClass[Post](targetClass.ref)
 
     val v = new Variable[Post](t)(o.sourceName(info.name))
     cNameSuccessor(RefCLocalDeclaration(decl, 0)) = v
 
-    Block(Seq(LocalDecl(v), assignLocal(v.get, NewObject[Post](targetClass.ref))))
+    val copy = init.init.map( v =>
+      Eval(createStructCopy(rw.dispatch(v), ref.decl, (f: InstanceField[_]) => PanicBlame("Cannot fail due to insufficient perm")))
+    )
 
+    val stats = Seq(LocalDecl(v), assignLocal(v.get, NewObject[Post](targetClass.ref))) ++
+      copy.toSeq
+    Block(stats)
   }
 
   def rewriteLocal(decl: CLocalDeclaration[Pre]): Statement[Post] = {

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

@@ -75,15 +75,7 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] {
       case t @ SilverPartialTAxiomatic(Ref(adt), partialTypeArgs) =>
         if(partialTypeArgs.map(_._1.decl).toSet != adt.typeArgs.toSet)
           throw IncompleteTypeArgs(t)
-
         TAxiomatic(succ(adt), adt.typeArgs.map(arg => dispatch(t.partialTypeArgs.find(_._1.decl == arg).get._2)))
-      case TNotAValue(decl) =>
-        decl match {
-          case RefCStruct(decl) =>
-            CTStruct(succ(decl))
-          case RefAxiomaticDataType(decl) => TAxiomatic[Post](succ(decl), Nil)
-          case _ => rewriteDefault(t)
-        }
       case other => rewriteDefault(other)
     }
   }

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

@@ -273,7 +273,7 @@ class CSpec extends VercorsSpec {
     }
     """
 
-  vercors should error withCode "type" in "struct type is no value" c
+  vercors should error withCode "typeUsedAsValue" in "struct type is no value" c
     """
     struct d {
         int x;
@@ -343,4 +343,30 @@ class CSpec extends VercorsSpec {
         s = t;
     }
     """
+
+    vercors should verify using silicon in "Parallel omp loop with declarations inside" c
+    """
+    #include <omp.h>
+    #include <assert.h>
+
+    int main(){
+        int sum[3] = {0, 0, 0};
+
+        #pragma omp parallel for
+        for(int i=0;i<3;i++)
+        /*@
+            context 0 <= i && i <3;
+            context Perm(&sum[i], write);
+            requires sum[i] == 0;
+            ensures sum[i] == i;
+        @*/
+        {
+            int xs[1] = {i};
+            sum[i] += xs[0];
+        }
+        assert(sum[0] == 0);
+        assert(sum[1] == 1);
+        assert(sum[2] == 2);
+    }
+    """
 }