From 439c0e8d9228770ae2b7361224a0f6627e47baf8 Mon Sep 17 00:00:00 2001
From: mlimbeck <mlimbeck@student.ethz.ch>
Date: Sat, 17 Aug 2024 07:54:16 +0200
Subject: [PATCH] different trigger

---
 router/dataplane.go | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/router/dataplane.go b/router/dataplane.go
index a45c3a4ed..8cd185665 100644
--- a/router/dataplane.go
+++ b/router/dataplane.go
@@ -123,7 +123,7 @@ type BatchConn interface {
 	// @ 	msgs[i].Mem()
 	// @ requires  forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
 	// @ 	msgs[i].GetFstBuffer() in msgsUBufs
-	// @ requires  forall ubuf []byte :: { ubuf } ubuf in msgsUBufs ==>
+	// @ requires  forall ubuf []byte :: { ubuf in msgsUBufs } ubuf in msgsUBufs ==>
 	// @ 	sl.Bytes(ubuf, 0, len(ubuf))
 	// @ ensures   forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
 	// @ 	(msgs[i].Mem() && msgs[i].HasActiveAddr())
@@ -136,7 +136,7 @@ type BatchConn interface {
 	// @ 	forall i int :: { &msgs[i] } 0 <= i && i < n ==> msgs[i].GetN() <= len(msgs[i].GetFstBuffer())
 	// @ ensures   forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
 	// @ 	msgs[i].GetFstBuffer() in msgsUBufs
-	// @ ensures   forall ubuf []byte :: { ubuf } ubuf in msgsUBufs ==>
+	// @ ensures   forall ubuf []byte :: { ubuf in msgsUBufs } ubuf in msgsUBufs ==>
 	// @ 	sl.Bytes(ubuf, 0, len(ubuf))
 	// @ ensures   err != nil ==> err.ErrorMem()
 	// contracts for IO-spec
@@ -835,7 +835,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 			// @ 	msgs[i].GetAddr() == nil
 			// @ ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
 			// @ 	msgs[i].GetFstBuffer() in msgsUBufs
-			// @ ensures forall ubuf []byte :: { ubuf } ubuf in msgsUBufs ==>
+			// @ ensures forall ubuf []byte :: { ubuf in msgsUBufs } ubuf in msgsUBufs ==>
 			// @ 	sl.Bytes(ubuf, 0, len(ubuf))
 			// @ decreases
 			// @ outline(
@@ -847,7 +847,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 			// @ 	msgs[i].Mem() && msgs[i].GetAddr() == nil && msgs[i].HasActiveAddr()
 			// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < i0 ==>
 			// @ 	msgs[i].GetFstBuffer() in msgsUBufs
-			// @ invariant forall ubuf []byte :: { ubuf } ubuf in msgsUBufs ==>
+			// @ invariant forall ubuf []byte :: { ubuf in msgsUBufs } ubuf in msgsUBufs ==>
 			// @ 	sl.Bytes(ubuf, 0, len(ubuf))
 			// @ decreases len(msgs) - i0
 			for i0 := 0; i0 < len(msgs); i0 += 1 {
@@ -889,7 +889,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 			// @ 	msgs[i].Mem()
 			// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
 			// @ 	msgs[i].GetFstBuffer() in msgsUBufs
-			// @ invariant forall ubuf []byte :: { ubuf } ubuf in msgsUBufs ==>
+			// @ invariant forall ubuf []byte :: { ubuf in msgsUBufs } ubuf in msgsUBufs ==>
 			// @ 	sl.Bytes(ubuf, 0, len(ubuf))
 			// @ invariant writeMsgInv(writeMsgs)
 			// @ invariant acc(dPtr, _) && *dPtr === d
@@ -964,7 +964,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 				// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem()
 				// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
 				// @ 	msgs[i].GetFstBuffer() in msgsUBufs
-				// @ invariant forall ubuf []byte :: { ubuf } ubuf in msgsUBufs ==>
+				// @ invariant forall ubuf []byte :: { ubuf in msgsUBufs } ubuf in msgsUBufs ==>
 				// @ 	sl.Bytes(ubuf, 0, len(ubuf))
 				// @ invariant writeMsgInv(writeMsgs)
 				// @ invariant acc(dPtr, _) && *dPtr === d