Skip to content
This repository was archived by the owner on Apr 12, 2023. It is now read-only.
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

@LinoTelschow

Description

@LinoTelschow

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions