search

gradual-verification / gvc0

Gradually Verified C0
6 stars 5 forks source link

Result assertions #5

Closed conradz closed 3 years ago

conradz commented 3 years ago

C0 defines a \result expression that can be used in postconditions. Currently this is not being parsed.