Permutation generator does not support treating missing `requires` and `ensures` specifications as `true`

gradual-verification / gvc0

Gradually Verified C0

6 stars 5 forks source link

Permutation generator does not support treating missing `requires` and `ensures` specifications as `true` #53

Open icmccorm opened 1 year ago

icmccorm commented 1 year ago

Currently, if a precondition or postcondition is left out, the verifier will assume @requires true or @ensures true. However, several test cases involving the permutation generator will fail for specs like this.