Skip to content
This repository was archived by the owner on Apr 12, 2023. It is now read-only.

Add ghost parameter to processPkt and its dependencies #63

Open
LinoTelschow opened this issue Feb 18, 2022 · 0 comments
Open

Add ghost parameter to processPkt and its dependencies #63

LinoTelschow opened this issue Feb 18, 2022 · 0 comments

Comments

@LinoTelschow
Copy link
Collaborator

As is:

  • at the moment the processPkt method doesn't return information if the processResult contains an SCMP error packet.

To Be:

  • the processPkt method should have a postconditon like:
isSCMPError ==> !isEmptyPR(result)
ghost
ensures res == (pr.EgressID == 0 && pr.OutConn == nil && pr.OutAddr == nil && pr.OutPkt == nil && pr.AddrSrc == 0)
decreases
pure func isEmptyPR(pr processResult) (res bool) {
	return pr.EgressID == 0 && pr.OutConn == nil && pr.OutAddr == nil && pr.OutPkt == nil && pr.AddrSrc == 0
}

With this information the caller of processPkt could deduce that processResult is not empty.

@LinoTelschow LinoTelschow mentioned this issue Feb 18, 2022
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant