diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala
index 72d31fd124..492f351984 100644
--- a/src/col/vct/col/ast/Node.scala
+++ b/src/col/vct/col/ast/Node.scala
@@ -1278,14 +1278,21 @@ final case class LLVMFunctionInvocation[G](ref: Ref[G, LLVMFunctionDefinition[G]
 
 final case class LLVMLoop[G](cond:Expr[G], contract:LLVMLoopContract[G], body:Statement[G])
                        (implicit val o: Origin) extends CompositeStatement[G] with LLVMLoopImpl[G]
+
 @family sealed trait LLVMLoopContract[G] extends NodeFamily[G] with LLVMLoopContractImpl[G]
+
 final case class LLVMLoopInvariant[G](value:String, references:Seq[(String, Ref[G, Declaration[G]])])
                                      (val blame: Blame[LoopInvariantFailure])
                                      (implicit val o: Origin) extends LLVMLoopContract[G] with LLVMLoopInvariantImpl[G]
+
+sealed trait LLVMStatement[G] extends Statement[G] with LLVMStatementImpl[G]
+
 sealed trait LLVMExpr[G] extends Expr[G] with LLVMExprImpl[G]
+
 final case class LLVMLocal[G](name: String)(val blame: Blame[DerefInsufficientPermission])(implicit val o: Origin) extends LLVMExpr[G] with LLVMLocalImpl[G] {
   var ref: Option[Ref[G, Variable[G]]] = None
 }
+
 final case class LLVMAmbiguousFunctionInvocation[G](name: String,
                                                     args: Seq[Expr[G]],
                                                     givenMap: Seq[(Ref[G, Variable[G]], Expr[G])],
@@ -1301,7 +1308,7 @@ final case class LLVMLoad[G](loadType: Type[G], pointer: Expr[G], ordering: LLVM
                             (implicit val o: Origin) extends LLVMExpr[G] with LLVMLoadImpl[G]
 
 final case class LLVMStore[G](value: Expr[G], pointer: Expr[G], ordering: LLVMMemoryOrdering[G])
-                             (implicit val o: Origin) extends Statement[G] with LLVMStoreImpl[G]
+                             (implicit val o: Origin) extends LLVMStatement[G] with LLVMStoreImpl[G]
 
 final case class LLVMGetElementPointer[G](structureType: Type[G], resultType: Type[G], pointer: Expr[G], indices: Seq[Expr[G]])
                                          (implicit val o: Origin) extends LLVMExpr[G] with LLVMGetElementPointerImpl[G]
@@ -1331,7 +1338,7 @@ final case class LLVMMemorySequentiallyConsistent[G]()(implicit val o:Origin) ex
 
 
 final case class LLVMIntegerValue[G](value: BigInt, integerType: Type[G])(implicit val o: Origin) extends ConstantInt[G] with LLVMExpr[G] with LLVMIntegerValueImpl[G]
-final case class LLVMPointerValue[G](value: Ref[G, LLVMGlobalVariable[G]])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMPointerValueImpl[G]
+final case class LLVMPointerValue[G](value: Ref[G, Declaration[G]])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMPointerValueImpl[G]
 // TODO: The LLVMFunctionPointerValue references a GlobalDeclaration instead of an LLVMFunctionDefinition because there is no other COL node we can use as a function pointer literal
 final case class LLVMFunctionPointerValue[G](value: Ref[G, GlobalDeclaration[G]])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMFunctionPointerValueImpl[G]
 final case class LLVMStructValue[G](value: Seq[Expr[G]], structType: Type[G])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMStructValueImpl[G]
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMAllocAImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMAllocAImpl.scala
index 760533ca67..0b7ca28484 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMAllocAImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMAllocAImpl.scala
@@ -1,8 +1,8 @@
 package vct.col.ast.lang.llvm
 
 import vct.col.ast.ops.LLVMAllocAOps
-import vct.col.ast.{LLVMAllocA, Type}
+import vct.col.ast.{LLVMAllocA, Type, LLVMTPointer}
 
 trait LLVMAllocAImpl[G] extends LLVMAllocAOps[G] { this: LLVMAllocA[G] =>
-  override val t: Type[G] = this.allocationType
+  override val t: Type[G] = LLVMTPointer(Some(this.allocationType))
 }
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMArrayValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMArrayValueImpl.scala
index 045e874eae..594a73df49 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMArrayValueImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMArrayValueImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.{Type, LLVMArrayValue}
 import vct.col.ast.ops.LLVMArrayValueOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMGetElementPointerImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMGetElementPointerImpl.scala
index db235c727a..6442aa3654 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMGetElementPointerImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMGetElementPointerImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.{LLVMGetElementPointer, LLVMTPointer, Type}
 import vct.col.ast.ops.LLVMGetElementPointerOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMGlobalVariableImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMGlobalVariableImpl.scala
index 30b77a7302..dc5dfd6275 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMGlobalVariableImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMGlobalVariableImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMGlobalVariable
 import vct.col.ast.ops.LLVMGlobalVariableOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMIntegerValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMIntegerValueImpl.scala
index de19524d71..8713ca04a0 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMIntegerValueImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMIntegerValueImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.{Type, LLVMIntegerValue}
 import vct.col.ast.ops.LLVMIntegerValueOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMLoadImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMLoadImpl.scala
index 18fc1f5b76..f82e50112a 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMLoadImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMLoadImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.{LLVMLoad, Type}
 import vct.col.ast.ops.LLVMLoadOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireImpl.scala
index df738623a8..aec8f004f3 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMMemoryAcquire
 import vct.col.ast.ops.LLVMMemoryAcquireOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireReleaseImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireReleaseImpl.scala
index 786e2b442c..6080f98594 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireReleaseImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireReleaseImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMMemoryAcquireRelease
 import vct.col.ast.ops.LLVMMemoryAcquireReleaseOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryMonotonicImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryMonotonicImpl.scala
index 51414e62e4..88a93ec4d6 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryMonotonicImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryMonotonicImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMMemoryMonotonic
 import vct.col.ast.ops.LLVMMemoryMonotonicOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryNotAtomicImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryNotAtomicImpl.scala
index 1038b551ef..7ac6a77eb4 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryNotAtomicImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryNotAtomicImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMMemoryNotAtomic
 import vct.col.ast.ops.LLVMMemoryNotAtomicOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryOrderingImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryOrderingImpl.scala
index 8730936c44..515f9be83f 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryOrderingImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryOrderingImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMMemoryOrdering
 import vct.col.ast.ops.LLVMMemoryOrderingFamilyOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryReleaseImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryReleaseImpl.scala
index db4f5a44e4..6baf5533f7 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryReleaseImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryReleaseImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMMemoryRelease
 import vct.col.ast.ops.LLVMMemoryReleaseOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemorySequentiallyConsistentImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemorySequentiallyConsistentImpl.scala
index 12c7e4c655..22381c5262 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMMemorySequentiallyConsistentImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMMemorySequentiallyConsistentImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMMemorySequentiallyConsistent
 import vct.col.ast.ops.LLVMMemorySequentiallyConsistentOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryUnorderedImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryUnorderedImpl.scala
index 855d3c9ee5..b778c4295c 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryUnorderedImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryUnorderedImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMMemoryUnordered
 import vct.col.ast.ops.LLVMMemoryUnorderedOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMPointerValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMPointerValueImpl.scala
index 8d1dc6f168..415d58f05b 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMPointerValueImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMPointerValueImpl.scala
@@ -1,10 +1,15 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
-import vct.col.ast.{Type, LLVMPointerValue, LLVMTPointer}
+import vct.col.ast.{LLVMGlobalVariable, LLVMPointerValue, LLVMTPointer, Type, HeapVariable}
 import vct.col.ast.ops.LLVMPointerValueOps
 import vct.col.print._
 
 trait LLVMPointerValueImpl[G] extends LLVMPointerValueOps[G] { this: LLVMPointerValue[G] =>
-  override lazy val t: Type[G] = LLVMTPointer(Some(value.decl.variableType))
+  override lazy val t: Type[G] = {
+    value.decl match {
+      case LLVMGlobalVariable(variableType, _, _) => LLVMTPointer(Some(variableType))
+      case v: HeapVariable[G] => LLVMTPointer(Some(v.t))
+    }
+  }
   // override def layout(implicit ctx: Ctx): Doc = ???
 }
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMRawArrayValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMRawArrayValueImpl.scala
index e1bf1c9306..b310ce588c 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMRawArrayValueImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMRawArrayValueImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.{Type, LLVMRawArrayValue}
 import vct.col.ast.ops.LLVMRawArrayValueOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMRawVectorValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMRawVectorValueImpl.scala
index c12d66a013..72a82ad346 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMRawVectorValueImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMRawVectorValueImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.{Type, LLVMRawVectorValue}
 import vct.col.ast.ops.LLVMRawVectorValueOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMSignExtendImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMSignExtendImpl.scala
index 016f44d6d9..9294bb2466 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMSignExtendImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMSignExtendImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.{LLVMSignExtend, Type}
 import vct.col.ast.ops.LLVMSignExtendOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMStatementImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMStatementImpl.scala
new file mode 100644
index 0000000000..5f8d9a1d4c
--- /dev/null
+++ b/src/col/vct/col/ast/lang/llvm/LLVMStatementImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.lang.llvm
+
+
+import vct.col.ast.LLVMStatement
+trait LLVMStatementImpl[G] { this: LLVMStatement[G] =>
+
+}
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMStoreImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMStoreImpl.scala
index c661ed452a..3e803bdcfa 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMStoreImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMStoreImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMStore
 import vct.col.ast.ops.LLVMStoreOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMStructValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMStructValueImpl.scala
index 5d19914140..77d18d9135 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMStructValueImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMStructValueImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.{LLVMStructValue, Type}
 import vct.col.ast.ops.LLVMStructValueOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMTArrayImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMTArrayImpl.scala
index db50ecd024..471b355f84 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMTArrayImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMTArrayImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMTArray
 import vct.col.ast.ops.LLVMTArrayOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMTFunctionImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMTFunctionImpl.scala
index 85b5951f9f..2776838c27 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMTFunctionImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMTFunctionImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMTFunction
 import vct.col.ast.ops.LLVMTFunctionOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMTIntImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMTIntImpl.scala
index 580c5c414d..4f13f92ade 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMTIntImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMTIntImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMTInt
 import vct.col.ast.ops.LLVMTIntOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMTStructImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMTStructImpl.scala
index b5634ecc98..d782fdd91b 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMTStructImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMTStructImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMTStruct
 import vct.col.ast.ops.LLVMTStructOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMTVectorImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMTVectorImpl.scala
index 5c0617be93..2a1a85b661 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMTVectorImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMTVectorImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.LLVMTVector
 import vct.col.ast.ops.LLVMTVectorOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMTruncateImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMTruncateImpl.scala
index 610e9780b9..0eef4cff6b 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMTruncateImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMTruncateImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.{LLVMTruncate, Type}
 import vct.col.ast.ops.LLVMTruncateOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMVectorValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMVectorValueImpl.scala
index 8012c0ded0..a9db55c0b9 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMVectorValueImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMVectorValueImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.{Type, LLVMVectorValue}
 import vct.col.print._
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMZeroExtendImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMZeroExtendImpl.scala
index 9bcdc0fc55..686f7fc7e1 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMZeroExtendImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMZeroExtendImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.{LLVMZeroExtend, Type}
 import vct.col.ast.ops.LLVMZeroExtendOps
diff --git a/src/col/vct/col/ast/lang/llvm/LLVMZeroedAggregateValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMZeroedAggregateValueImpl.scala
index 8161633046..053cf691ed 100644
--- a/src/col/vct/col/ast/lang/llvm/LLVMZeroedAggregateValueImpl.scala
+++ b/src/col/vct/col/ast/lang/llvm/LLVMZeroedAggregateValueImpl.scala
@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.{Type, LLVMZeroedAggregateValue}
 import vct.col.ast.ops.LLVMZeroedAggregateValueOps
diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala
index 83316253d6..0a88d521f7 100644
--- a/src/col/vct/col/typerules/CoercingRewriter.scala
+++ b/src/col/vct/col/typerules/CoercingRewriter.scala
@@ -1463,8 +1463,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite
       case glue: JavaBipGlue[Pre] => glue
       case LLVMLocal(name) => e
       case LLVMAllocA(allocationType, numElements) => e
-      case LLVMLoad(loadType, p, ordering) => LLVMLoad(loadType, p, ordering)
-      case LLVMGetElementPointer(structureType, resultType, pointer, indices) => e
+      case LLVMLoad(loadType, p, ordering) => LLVMLoad(loadType, llvmPointer(p, loadType)._1, ordering)
+      case LLVMGetElementPointer(structureType, resultType, pointer, indices) => LLVMGetElementPointer(structureType, resultType, llvmPointer(pointer, structureType)._1, indices)
       case LLVMSignExtend(inputType, outputType, value) => e
       case LLVMZeroExtend(inputType, outputType, value) => e
       case LLVMTruncate(inputType, outputType, value) => e
@@ -1528,7 +1528,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite
       case l @ Lock(obj) => Lock(cls(obj))(l.blame)
       case Loop(init, cond, update, contract, body) => Loop(init, bool(cond), update, contract, body)
       case LLVMLoop(cond, contract, body) => LLVMLoop(bool(cond), contract, body)
-      case LLVMStore(value, p, ordering) => LLVMStore(value, p, ordering)
+      case LLVMStore(value, p, ordering) => LLVMStore(value, llvmPointer(p, value.t)._1, ordering)
       case ModelDo(model, perm, after, action, impl) => ModelDo(model, rat(perm), after, action, impl)
       case n @ Notify(obj) => Notify(cls(obj))(n.blame)
       case at @ ParAtomic(inv, content) => ParAtomic(inv, content)(at.blame)
diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala
index 7d17879d19..3b3e4d22d2 100644
--- a/src/col/vct/col/typerules/CoercionUtils.scala
+++ b/src/col/vct/col/typerules/CoercionUtils.scala
@@ -6,6 +6,8 @@ import vct.col.origin.{DiagnosticOrigin, Origin}
 import vct.col.resolve.lang.{C, CPP}
 import vct.col.resolve.lang.CPP.getBaseTypeFromSpecs
 
+import scala.annotation.tailrec
+
 case object CoercionUtils {
   private implicit val o: Origin = DiagnosticOrigin
 
@@ -200,6 +202,8 @@ case object CoercionUtils {
       case (LLVMTPointer(Some(leftInner)), LLVMTPointer(Some(rightInner))) =>
         getAnyCoercion(leftInner, rightInner).getOrElse(return None)
 
+
+
       // Something with TVar?
 
       // Unsafe coercions
@@ -299,11 +303,20 @@ case object CoercionUtils {
     case _ => None
   }
 
+  @tailrec
+  def firstElementIsType[G](aggregate: Type[G], innerType: Type[G]): Boolean = aggregate match {
+    case aggregate if getAnyCoercion(aggregate, innerType).isDefined => true
+    case LLVMTStruct(_, _, elements) => firstElementIsType(elements.head, innerType)
+    case LLVMTArray(numElements, elementType) => numElements > 0 && firstElementIsType(elementType, innerType)
+    case LLVMTVector(_, _) => false // TODO: Should this be possible?
+    case _ => false
+  }
+
   def getAnyLLVMPointerCoercion[G](source: Type[G], innerType: Type[G]): Option[(Coercion[G], LLVMTPointer[G])] = source match {
       case LLVMTPointer(None) =>
         Some((CoerceLLVMPointer(None, Some(innerType)), LLVMTPointer[G](Some(innerType))))
-      case LLVMTPointer(Some(t)) if t == innerType =>
-        Some((CoerceLLVMPointer(Some(t), Some(innerType)), LLVMTPointer[G](Some(innerType))))
+      case LLVMTPointer(Some(t)) if firstElementIsType(t, innerType) =>
+        Some(CoerceLLVMPointer(Some(t), Some(innerType)), LLVMTPointer[G](Some(innerType)))
       case _: TNull[G] =>
         Some((CoerceLLVMPointer(None, Some(innerType)), LLVMTPointer[G](Some(innerType))))
       case _ => None
diff --git a/src/llvm/include/Passes/Function/FunctionBodyTransformer.h b/src/llvm/include/Passes/Function/FunctionBodyTransformer.h
index 4c300bb368..83120722b7 100644
--- a/src/llvm/include/Passes/Function/FunctionBodyTransformer.h
+++ b/src/llvm/include/Passes/Function/FunctionBodyTransformer.h
@@ -70,7 +70,8 @@ class FunctionCursor {
      * @param llvmInstruction
      * @return the created variable declaration
      */
-    col::Variable &declareVariable(Instruction &llvmInstruction);
+    col::Variable &declareVariable(Instruction &llvmInstruction,
+                                   Type *llvmPointerType = nullptr);
 
     /**
      * Functionality is twofold:
@@ -82,8 +83,10 @@ class FunctionCursor {
      * @param colBlock
      * @return The created col assignment
      */
-    col::Assign &createAssignmentAndDeclaration(Instruction &llvmInstruction,
-                                                col::Block &colBlock);
+    col::Assign &
+    createAssignmentAndDeclaration(Instruction &llvmInstruction,
+                                   col::Block &colBlock,
+                                   Type *llvmPointerType = nullptr);
 
     /**
      * Creates an assignment in the provided colBlock referencing the provided
diff --git a/src/llvm/include/Transform/Transform.h b/src/llvm/include/Transform/Transform.h
index ea10017d36..4506aa4a97 100644
--- a/src/llvm/include/Transform/Transform.h
+++ b/src/llvm/include/Transform/Transform.h
@@ -12,6 +12,8 @@ namespace llvm2col {
 namespace col = vct::col::ast;
 
 // type transformers
+void transformAndSetPointerType(llvm::Type &llvmType, col::Type &colType);
+
 void transformAndSetType(llvm::Type &llvmType, col::Type &colType);
 
 /**
diff --git a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp
index 506687ef8d..215d9ae74e 100644
--- a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp
+++ b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp
@@ -103,13 +103,19 @@ FDResult &FunctionCursor::getFDResult(Function &otherLLVMFunction) {
     return FAM.getResult<FunctionDeclarer>(otherLLVMFunction);
 }
 
-col::Variable &FunctionCursor::declareVariable(Instruction &llvmInstruction) {
+col::Variable &FunctionCursor::declareVariable(Instruction &llvmInstruction,
+                                               Type *llvmPointerType) {
     // create declaration in buffer
     col::Variable *varDecl = functionScope.add_locals();
     // set type of declaration
     try {
-        llvm2col::transformAndSetType(*llvmInstruction.getType(),
-                                      *varDecl->mutable_t());
+        if (llvmPointerType == nullptr) {
+            llvm2col::transformAndSetType(*llvmInstruction.getType(),
+                                          *varDecl->mutable_t());
+        } else {
+            llvm2col::transformAndSetPointerType(*llvmPointerType,
+                                                 *varDecl->mutable_t());
+        }
     } catch (pallas::UnsupportedTypeException &e) {
         std::stringstream errorStream;
         errorStream << e.what() << " in variable declaration.";
@@ -125,10 +131,9 @@ col::Variable &FunctionCursor::declareVariable(Instruction &llvmInstruction) {
     return *varDecl;
 }
 
-col::Assign &
-FunctionCursor::createAssignmentAndDeclaration(Instruction &llvmInstruction,
-                                               col::Block &colBlock) {
-    col::Variable &varDecl = declareVariable(llvmInstruction);
+col::Assign &FunctionCursor::createAssignmentAndDeclaration(
+    Instruction &llvmInstruction, col::Block &colBlock, Type *llvmPointerType) {
+    col::Variable &varDecl = declareVariable(llvmInstruction, llvmPointerType);
     return createAssignment(llvmInstruction, colBlock, varDecl);
 }
 
diff --git a/src/llvm/lib/Transform/Instruction/MemoryOpTransform.cpp b/src/llvm/lib/Transform/Instruction/MemoryOpTransform.cpp
index 005f3b143f..a1f4916574 100644
--- a/src/llvm/lib/Transform/Instruction/MemoryOpTransform.cpp
+++ b/src/llvm/lib/Transform/Instruction/MemoryOpTransform.cpp
@@ -36,13 +36,14 @@ void llvm2col::transformMemoryOp(llvm::Instruction &llvmInstruction,
 void llvm2col::transformAllocA(llvm::AllocaInst &allocAInstruction,
                                col::Block &colBlock,
                                pallas::FunctionCursor &funcCursor) {
-    col::Assign &assignment =
-        funcCursor.createAssignmentAndDeclaration(allocAInstruction, colBlock);
+    col::Assign &assignment = funcCursor.createAssignmentAndDeclaration(
+        allocAInstruction, colBlock,
+        /* pointer type*/ allocAInstruction.getAllocatedType());
     col::Expr *allocAExpr = assignment.mutable_value();
     col::LlvmAllocA *allocA = allocAExpr->mutable_llvm_alloc_a();
     allocA->set_allocated_origin(
         llvm2col::generateSingleStatementOrigin(allocAInstruction));
-    llvm2col::transformAndSetType(*allocAInstruction.getType(),
+    llvm2col::transformAndSetType(*allocAInstruction.getAllocatedType(),
                                   *allocA->mutable_allocation_type());
     llvm2col::transformAndSetExpr(funcCursor, allocAInstruction,
                                   *allocAInstruction.getArraySize(),
diff --git a/src/llvm/lib/Transform/Transform.cpp b/src/llvm/lib/Transform/Transform.cpp
index 27329d87e4..06b95c9861 100644
--- a/src/llvm/lib/Transform/Transform.cpp
+++ b/src/llvm/lib/Transform/Transform.cpp
@@ -15,6 +15,13 @@ const std::string SOURCE_LOC = "Transform::Transform";
 
 namespace col = vct::col::ast;
 
+void llvm2col::transformAndSetPointerType(llvm::Type &llvmType,
+                                          col::Type &colType) {
+    col::LlvmtPointer *pointerType = colType.mutable_llvmt_pointer();
+    pointerType->set_allocated_origin(generateTypeOrigin(llvmType));
+    llvm2col::transformAndSetType(llvmType, *pointerType->mutable_inner_type());
+}
+
 void llvm2col::transformAndSetType(llvm::Type &llvmType, col::Type &colType) {
     switch (llvmType.getTypeID()) {
     case llvm::Type::IntegerTyID:
diff --git a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala
index 7b2b0441df..a59198e0a9 100644
--- a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala
+++ b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala
@@ -353,6 +353,7 @@ case class ResolveExpressionSideEffects[Pre <: Generation]() extends Rewriter[Pr
       case _: CStatement[Pre] => throw ExtraNode
       case _: CPPStatement[Pre] => throw ExtraNode
       case _: JavaStatement[Pre] => throw ExtraNode
+      case _: LLVMStatement[Pre] => throw ExtraNode
     }
   }
 
diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala
index ba44d21ecd..e20274dc4f 100644
--- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala
@@ -3,12 +3,12 @@ package vct.rewrite.lang
 import com.typesafe.scalalogging.LazyLogging
 import vct.col.ast._
 import vct.col.origin.Origin
-import vct.col.ref.{LazyRef, Ref}
+import vct.col.ref.{DirectRef, LazyRef, Ref}
 import vct.col.resolve.ctx.RefLLVMFunctionDefinition
 import vct.col.rewrite.{Generation, Rewritten}
+import vct.col.util.AstBuildHelpers.tt
 import vct.col.util.{CurrentProgramContext, SuccessionMap}
-import vct.result.VerificationError.SystemError
-import vct.rewrite.lang.LangLLVMToCol.UnexpectedLLVMNode
+import vct.result.VerificationError.{SystemError, UserError}
 
 case object LangLLVMToCol {
   case class UnexpectedLLVMNode(node: Node[_]) extends SystemError {
@@ -18,14 +18,25 @@ case object LangLLVMToCol {
         .getOrElse(node.o)
         .messageInContext("VerCors assumes this node does not occur here in llvm input.")
   }
+
+  case class NonConstantStructIndex(origin: Origin) extends UserError {
+    override def code: String = "nonConstantStructIndex"
+
+    override def text: String =
+      origin.messageInContext(s"This struct indexing operation (getelementptr) uses a non-constant struct index which we do not support.")
+  }
 }
 
 case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends LazyLogging {
+  import LangLLVMToCol._
   type Post = Rewritten[Pre]
   implicit val implicitRewriter: AbstractRewriter[Pre, Post] = rw
 
   private val llvmFunctionMap: SuccessionMap[LLVMFunctionDefinition[Pre], Procedure[Post]] = SuccessionMap()
   private val specFunctionMap: SuccessionMap[LLVMSpecFunction[Pre], Function[Post]] = SuccessionMap()
+  private val globalVariableMap: SuccessionMap[LLVMGlobalVariable[Pre], HeapVariable[Post]] = SuccessionMap()
+  private val structMap: SuccessionMap[LLVMTStruct[Pre], Class[Post]] = SuccessionMap()
+  private val structFieldMap: SuccessionMap[(LLVMTStruct[Pre], Int), InstanceField[Post]] = SuccessionMap()
 
 
   def rewriteLocal(local: LLVMLocal[Pre]): Expr[Post] = {
@@ -122,6 +133,82 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends
     )
   }
 
+  def rewriteStruct(t: LLVMTStruct[Pre]): Unit = {
+    val LLVMTStruct(name, packed, elements) = t
+    val newStruct = new Class[Post](rw.classDeclarations.collect {
+      elements.zipWithIndex.foreach { case (fieldType, idx) =>
+        structFieldMap((t, idx)) =
+          new InstanceField(rw.dispatch(fieldType), flags = Nil)(fieldType.o)
+        rw.classDeclarations.declare(structFieldMap((t, idx)))
+      }
+    }._1, Seq(), tt[Post])(t.o)
+
+    rw.globalDeclarations.declare(newStruct)
+    structMap(t) = newStruct
+  }
+
+  def rewriteGlobalVariable(decl: LLVMGlobalVariable[Pre]): Unit = {
+    // TODO: Handle the initializer
+    // TODO: Include array and vector bounds somehow
+    decl.variableType match {
+      case struct: LLVMTStruct[Pre] => {
+        rewriteStruct(struct)
+        globalVariableMap.update(decl, rw.globalDeclarations.declare(new HeapVariable[Post](new TClass[Post](new DirectRef[Post, Class[Post]](structMap(struct)))(struct.o))(decl.o)))
+      }
+      case array: LLVMTArray[Pre] => {
+        globalVariableMap.update(decl, rw.globalDeclarations.declare(new HeapVariable[Post](new TArray[Post](rw.dispatch(array.elementType))(array.o))(decl.o)))
+      }
+      case vector: LLVMTVector[Pre] => {
+        globalVariableMap.update(decl, rw.globalDeclarations.declare(new HeapVariable[Post](new TArray[Post](rw.dispatch(vector.elementType))(vector.o))(decl.o)))
+      }
+      case _ => {
+        ???
+      }
+    }
+  }
+
+  def rewritePointerChain(pointer: Expr[Post], t: Type[Pre], indices: Seq[Expr[Pre]])(implicit o: Origin): Expr[Post] = {
+    if (indices.isEmpty) {
+      return pointer
+    }
+    t match {
+      case struct: LLVMTStruct[Pre] => {
+        indices.head match {
+          // TODO: This doesn't quite work because struct types are not uniqued
+          case value: LLVMIntegerValue[Pre] =>
+            rewritePointerChain(Deref[Post](pointer, structFieldMap.ref((struct, value.value.intValue)))(o), struct.elements(value.value.intValue), indices.tail)
+          case _ => throw NonConstantStructIndex(o)
+        }
+      }
+      case array: LLVMTArray[Pre] => ???
+      case vector: LLVMTVector[Pre] => ???
+    }
+  }
+
+  def rewriteGetElementPointer(gep: LLVMGetElementPointer[Pre]): Expr[Post] = {
+    implicit val o: Origin = gep.o
+    val t = gep.structureType
+    t match {
+      case struct: LLVMTStruct[Pre] => {
+        // TODO: We don't support variables in GEP yet and this just assumes all the indices are integer constants
+        // TODO: Use an actual Blame
+
+        // Acquire the actual struct through a PointerAdd
+        // TODO: Can we somehow wrap the rw.dispatch(gep.pointer) to add the known type structureType?
+        val structPointer = DerefPointer(PointerAdd(rw.dispatch(gep.pointer), rw.dispatch(gep.indices.head))(o))(o)
+
+        rewritePointerChain(structPointer, struct, gep.indices.tail)
+      }
+      case array: LLVMTArray[Pre] => ???
+      case vector: LLVMTVector[Pre] => ???
+    }
+    // Deref might not be the correct thing to use here since technically the pointer is only dereferenced in the load or store instruction
+  }
+
+  def rewritePointerValue(pointer: LLVMPointerValue[Pre]): Expr[Post] = {
+    new LLVMPointerValue[Post](globalVariableMap.ref(pointer.value.decl.asInstanceOf[LLVMGlobalVariable[Pre]]))(pointer.o)
+  }
+
   def result(ref: RefLLVMFunctionDefinition[Pre])(implicit o: Origin): Expr[Post] =
     Result[Post](llvmFunctionMap.ref(ref.decl))
 
diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala
index 3746d2800d..44cdf4c158 100644
--- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala
@@ -123,6 +123,7 @@ case class LangSpecificToCol[Pre <: Generation](veymontGeneratePermissions: Bool
 
     case func: LLVMFunctionDefinition[Pre] => llvm.rewriteFunctionDef(func)
     case global: LLVMGlobalSpecification[Pre] => llvm.rewriteGlobal(global)
+    case global: LLVMGlobalVariable[Pre] => llvm.rewriteGlobalVariable(global)
 
     case cls: Class[Pre] =>
       currentClass.having(cls) {
@@ -267,6 +268,8 @@ case class LangSpecificToCol[Pre <: Generation](veymontGeneratePermissions: Bool
     case inv: LLVMAmbiguousFunctionInvocation[Pre] => llvm.rewriteAmbiguousFunctionInvocation(inv)
     case local: LLVMLocal[Pre] => llvm.rewriteLocal(local)
     case pointer: LLVMFunctionPointerValue[Pre] => llvm.rewriteFunctionPointer(pointer)
+    case pointer: LLVMPointerValue[Pre] => llvm.rewritePointerValue(pointer)
+    case gep: LLVMGetElementPointer[Pre] => llvm.rewriteGetElementPointer(gep)
 
     case other => rewriteDefault(other)
   }