Skip to content

Commit

Permalink
adding missing comment
Browse files Browse the repository at this point in the history
  • Loading branch information
mlimbeck committed Nov 14, 2023
1 parent 4c87477 commit 193add2
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions verification/io/dataplane_abstract.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,7 @@ pure func (dp DataPlaneSpec) GetNeighborIA(ifs IO_ifs) IO_as {
return dp.neighborIAs[ifs]
}

// This function corresponds to function 'asid' in the IO spec
ghost
decreases
pure func (dp DataPlaneSpec) GetLocalIA() IO_as {
Expand Down

0 comments on commit 193add2

Please sign in to comment.