Changed the signature of writtenVars s.t. it returns a Seq instead of…

… a Set

src/main/scala/semper/sil/ast/utility/ControlFlowGraph.scala

@@ -98,10 +98,14 @@ object ControlFlowGraph {
    * @param b A block whose set of written variables is to be computed.
    * @return The set of written variables.
    */
-  def writtenVars(b: Block): Set[LocalVar] = b match {
-    case lb: LoopBlock => writtenVars(lb.body)
-    case cb: ConditionalBlock => cb.stmt.writtenVars ++ writtenVars(cb.thn) ++ writtenVars(cb.els)
-    case frpb: FreshReadPermBlock => writtenVars(frpb.body) ++ frpb.vars
-    case sb: StatementBlock => sb.stmt.writtenVars
+  def writtenVars(b: Block): Seq[LocalVar] = {
+    val writtenTo = b match {
+      case lb: LoopBlock => writtenVars(lb.body)
+      case cb: ConditionalBlock => cb.stmt.writtenVars ++ writtenVars(cb.thn) ++ writtenVars(cb.els)
+      case frpb: FreshReadPermBlock => writtenVars(frpb.body) ++ frpb.vars
+      case sb: StatementBlock => sb.stmt.writtenVars
+    }
+
+    writtenTo.distinct
   }
 }

src/main/scala/semper/sil/ast/utility/Statements.scala

@@ -55,17 +55,20 @@ object Statements {
     s.reduceWithContext(Nil, addDecls, combineResults)
   }
 
-  def writtenVars(s: Stmt): Set[LocalVar] = {
-    var writtenTo = Set[LocalVar]()
+  /**
+   * Computes all local variables that are written to in the given statement and that are declared outside of
+   */
+  def writtenVars(s: Stmt): Seq[LocalVar] = {
+    var writtenTo = Seq[LocalVar]()
 
     s visit {
-      case LocalVarAssign(lhs, _) => writtenTo = writtenTo + lhs
+      case LocalVarAssign(lhs, _) => writtenTo = lhs +: writtenTo
       case MethodCall(_, _, targets) => writtenTo = writtenTo ++ targets
       case FreshReadPerm(vars, _) => writtenTo = writtenTo ++ vars
-      case NewStmt(lhs) => writtenTo = writtenTo + lhs
-      case While(_, _, locals, body) => writtenTo = writtenTo ++ (writtenVars(body) -- locals.map(_.localVar))
+      case NewStmt(lhs) => writtenTo = lhs +: writtenTo
+      case While(_, _, locals, body) => writtenTo = writtenTo ++ (writtenVars(body) intersect s.undeclLocalVars)
     }
 
-    writtenTo
+    writtenTo.distinct
   }
 }