search

gradual-verification / gvc0

Gradually Verified C0
6 stars 5 forks source link

Old assertions #6

Closed conradz closed 3 years ago

conradz commented 3 years ago

C0 defines a \old(param) that allows the initial value of an argument to be used in a postcondition even if the parameter is reassigned. Currently the parser does not parse this.

conradz commented 3 years ago

These were actually removed from the C0 standard, so we shouldn't implement them.