diff --git a/src/main/scala/analysis/BasicIRConstProp.scala b/src/main/scala/analysis/BasicIRConstProp.scala
index d87458c21..ae3f70a7d 100644
--- a/src/main/scala/analysis/BasicIRConstProp.scala
+++ b/src/main/scala/analysis/BasicIRConstProp.scala
@@ -61,6 +61,7 @@ trait ILValueAnalysisMisc:
 
       case _ => valuelattice.top
 
+  val calleePreservedRegisters = Set("R0", "R1", "R2", "R3", "R4", "R5", "R6", "R7", "R8", "R9", "R10", "R11")
 
   /** Transfer function for state lattice elements.
     */
@@ -68,6 +69,7 @@ trait ILValueAnalysisMisc:
     n match
       case la: LocalAssign =>
         s + (la.lhs -> eval(la.rhs, s))
+      case c: Call => s ++ calleePreservedRegisters.filter(reg => s.keys.exists(_.name == reg)).map(n => Register(n, BitVecType(64)) -> statelattice.sublattice.top).toMap
       case _ => s
 
 
diff --git a/src/main/scala/ir/IRCursor.scala b/src/main/scala/ir/IRCursor.scala
index f8e1acffc..f0352dbd5 100644
--- a/src/main/scala/ir/IRCursor.scala
+++ b/src/main/scala/ir/IRCursor.scala
@@ -3,34 +3,56 @@ import cfg_visualiser.DotElement
 import cfg_visualiser.{DotArrow, DotGraph, DotInlineArrow, DotInterArrow, DotIntraArrow, DotNode, DotRegularArrow}
 
 import collection.mutable
+import scala.annotation.tailrec
 
 /*
  * Defines a position in the IL / CFG; this becomes the lhs of the state map lattice in a static analysis.
  */
-type CFGPosition = Procedure | Block | Command | ProcedureUnknownJump  | ProcedureExit
+type CFGPosition = Procedure | Block | Command
 
 
 // Interprocedural
 //  position = (call string) + Position
 
 
+
 /*
-    An additional CFG node which implicitly follows the node at `pos`
-    A call to an unknown procedure without a return to here
+    Closed trace-perspective beginning of a composite IL structure.
  */
-case class ProcedureUnknownJump(fromProcedure: Procedure, pos: CFGPosition)
+def begin(c: CFGPosition): CFGPosition = {
+  c match {
+    case p:Procedure => p
+    case b:Block => b
+    case s:Statement => s.parent.statements.head()
+    case s:Jump => s
+  }
+}
 
 /*
- *  An additional CFG node which implicitly follows the node at `pos`
- *  The exit from a procedure from pos (the last command/jump in the procedure).
+    Closed trace-perspective end of a composite IL structure.
  */
-case class ProcedureExit(fromProcedure: Procedure, pos: CFGPosition)
+@tailrec
+def end(c: CFGPosition): CFGPosition = {
+  c match {
+    case p:Procedure => end(p.returnBlock)
+    case b:Block => b.jump
+    case s:Statement => s.parent.statements.back()
+    case s:Jump => s
+  }
+}
+
 
 object IntraProcIRCursor {
   type Node = CFGPosition
 
   def succ(pos: CFGPosition): Set[CFGPosition] = {
     pos match {
+      case proc: Procedure =>
+        if proc.entryBlock.isEmpty then Set(proc.returnBlock) else Set(proc.entryBlock.get)
+      case b: Block =>
+        if b.statements.isEmpty
+        then Set.from(b.jumpSet)
+        else Set[CFGPosition](b.statements.head())
       case s: Statement =>
         if (s.parent.statements.hasNext(s)) {
           Set(s.parent.statements.getNext(s))
@@ -51,14 +73,6 @@ object IntraProcIRCursor {
               case None => Set()
           }
       }
-      case b: Block =>
-        if b.statements.isEmpty
-          then Set.from(b.jumpSet)
-        else Set[CFGPosition](b.statements.head())
-      case proc: Procedure =>
-        if proc.entryBlock.isEmpty then Set(proc.returnBlock) else Set(proc.entryBlock.get)
-      case j: ProcedureUnknownJump => Set(ProcedureExit(j.fromProcedure, j))
-      case e: ProcedureExit => Set()
     }
   }
 
@@ -71,14 +85,30 @@ object IntraProcIRCursor {
           Set(s.parent) // predecessor blocks
         }
       case j: Jump => if j.parent.statements.isEmpty then Set(j.parent) else Set(j.parent.statements.last)
-      case b: Block => b.predecessors.asInstanceOf[Set[CFGPosition]]
+      case b: Block => b.predecessors.map(end)
       case proc: Procedure => Set() // intraproc
-      case r: ProcedureUnknownJump => Set(r.pos)
-      case r: ProcedureExit => Set(r.pos)
     }
   }
 }
 
+object InterProcIRCursor {
+  type Node = CFGPosition
+
+  def succ(pos: CFGPosition): Set[CFGPosition] = {
+    IntraProcIRCursor.succ(pos) ++ (pos match
+      case c: DirectCall => Set(c.target)
+      case _ => Set()
+      )
+  }
+    def pred(pos: CFGPosition): Set[CFGPosition] = {
+      IntraProcIRCursor.pred(pos) ++ (pos match
+        case c: Procedure => c.callers().map(end)
+        case b: Block => if b.isReturn then b.parent.callers().map(end) else Set()
+        case _ => Set()
+        )
+    }
+}
+
 
 def computeDomain(prog: Program): mutable.Set[CFGPosition] = {
   val domain : mutable.Set[CFGPosition] = mutable.Set.from(prog.procedures)
diff --git a/src/main/scala/translating/BAPToIR.scala b/src/main/scala/translating/BAPToIR.scala
index 4793040bd..ff25e2ec3 100644
--- a/src/main/scala/translating/BAPToIR.scala
+++ b/src/main/scala/translating/BAPToIR.scala
@@ -19,11 +19,7 @@ class BAPToIR(var program: BAPProgram, mainAddress: Int) {
     var mainProcedure: Option[Procedure] = None
     val procedures: ArrayBuffer[Procedure] = ArrayBuffer()
     for (s <- program.subroutines) {
-      //val blocks: mutable.HashSet[Block] = mutable.HashSet[Block]()
-      //val in: ArrayBuffer[Parameter] = ArrayBuffer()
-      //val out: ArrayBuffer[Parameter] = ArrayBuffer()
-      val procedure = Procedure(s.name, Some(s.address), Seq(), Seq(), Seq())
-
+      val procedure = Procedure(s.name, Some(s.address))
 
       for (b <- s.blocks) {
         val block = Block(b.label, b.address, ArrayBuffer())
@@ -48,7 +44,7 @@ class BAPToIR(var program: BAPProgram, mainAddress: Int) {
       for (b <- s.blocks) {
         val block = labelToBlock(b.label)
         for (st <- b.statements) {
-          block.statements.append(translate(st, block))
+          block.statements.append(translate(st))
         }
         val (jump, newBlocks) = translate(b.jumps, block)
         procedure.addBlocks(newBlocks)
@@ -65,7 +61,7 @@ class BAPToIR(var program: BAPProgram, mainAddress: Int) {
     Program(procedures, mainProcedure.get, memorySections, ArrayBuffer())
   }
 
-  private def translate(s: BAPStatement, parent: Block) = s match {
+  private def translate(s: BAPStatement) = s match {
     case b: BAPMemAssign   => MemoryAssign(b.lhs.toIR, b.rhs.toIR, Some(b.line))
     case b: BAPLocalAssign => LocalAssign(b.lhs.toIR, b.rhs.toIR, Some(b.line))
   }
diff --git a/src/main/scala/translating/ILtoIL.scala b/src/main/scala/translating/ILtoIL.scala
index 8af2b1505..bdbc10a81 100644
--- a/src/main/scala/translating/ILtoIL.scala
+++ b/src/main/scala/translating/ILtoIL.scala
@@ -62,10 +62,9 @@ private class ILSerialiser extends ReadOnlyVisitor {
 
 
   override def visitGoTo(node: GoTo): GoTo = {
-    program ++= "NonDetGoTo({"
-    // TODO
+    program ++= "GoTo("
     program ++= node.targets.map(blockIdentifier).mkString(", ")
-    program ++= "})" // GoTo
+    program ++= ")" // GoTo
     node
   }
 
diff --git a/src/main/scala/util/IntrusiveList.scala b/src/main/scala/util/IntrusiveList.scala
index 3a5f2f6e0..8afb59075 100644
--- a/src/main/scala/util/IntrusiveList.scala
+++ b/src/main/scala/util/IntrusiveList.scala
@@ -80,6 +80,9 @@ final class IntrusiveList[T <: IntrusiveListElement] private (var numElems: Int,
 
   override def head(): T = firstElem.get
 
+  override def headOption(): Option[T] = firstElem
+
+
   def begin(): T = firstElem.get
 
   private def containsRef(elem: T): Boolean = {