search

GaloisInc / pate

Patches Assured up to Trace Equivalence
Other
15 stars 2 forks source link

Add packet example and integration test #417

Closed thebendavis closed 1 month ago

thebendavis commented 1 month ago

This adds a standalone example (packet.exe) and an integration test. Beyond testing basic verifier functionality, this is intended to provide an integration test of the 1) terminal user interaction, and 2) resulting equivalence condition, in ways that the other automated tests do not. The integration test is implemented as an expect script that captures a subset of the expected output including a key clause of the equivalence condition, and will alert / need to be updated if this output changes during evolution of the PATE verifier.

This integration test has been added to the docker CI job. I have not additionally added it to the build CI job because that job uses cabal build pkg:pate which breaks subsequent use of ./pate.sh, which is the interface used by the integration test. This issue is captured separately in #418 and is outside of the scope of this PR.

danmatichuk commented 1 month ago

This looks fine to me, I think including at least one example that bypasses the normal "scripting" interface makes sense as a sanity check. I think it also makes sense to test it both via docker and natively once #418 is addressed.

thebendavis commented 1 month ago

This looks fine to me, I think including at least one example that bypasses the normal "scripting" interface makes sense as a sanity check. I think it also makes sense to test it both via docker and natively once #418 is addressed.

Thanks for the review! I have flagged the appropriate items for followup in relevant issues.