assertion in run

viperproject · Dec 18, 2024 · a6cd4e0 · a6cd4e0
1 parent 2aebfb2
commit a6cd4e0
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/router/dataplane.go b/router/dataplane.go
@@ -1032,6 +1032,8 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 					// @ assert sl.Bytes(tmpBuf, 0, p.N)
 					// @ assert sl.Bytes(tmpBuf, 0, len(tmpBuf))
 					result, err /*@ , addrAliasesPkt, newAbsPkt @*/ := processor.processPkt(tmpBuf, srcAddr /*@, ioLock, ioSharedArg, dp @*/)
+					// @ assert forall i int :: { &msgs[i] } i0 < i && i < pkts ==>
+					// @ 	MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]
 					// @ fold scmpErr.Mem()
 
 					switch {