Skip to content

Commit fab87f7

Browse files
authored
remove unnecessary function (#406)
1 parent b5bc28c commit fab87f7

File tree

1 file changed

+0
-7
lines changed

1 file changed

+0
-7
lines changed

router/dataplane_spec.gobra

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -413,13 +413,6 @@ func (d *DataPlane) getInternal() {
413413
unfold acc(d.Mem(), _)
414414
}
415415

416-
requires acc(d.Mem(), _)
417-
ensures acc(&d.macFactory, _)
418-
decreases
419-
func (d *DataPlane) getMacFactoryMem() {
420-
unfold acc(d.Mem(), _)
421-
}
422-
423416
ghost
424417
requires acc(d.Mem(), _) && d.getMacFactory() != nil
425418
ensures acc(&d.macFactory, _) && acc(&d.key, _) && acc(d.key, _)

0 commit comments

Comments
 (0)