gradual-verification / gvc0

Gradually Verified C0
6 stars 5 forks source link

Precedence of ++/-- and pointer dereference (*) #3

Closed conradz closed 3 years ago

conradz commented 3 years ago

Increment/decrement (++/--) operators are defined to have a higher precedence than the pointer dereference, but currently do not. This is because ++ and -- are statements, not expressions in C0 and all expression parsing is done before statement parsing in our parser. This causes *x++; to be parsed successfully and interpreted as dereferencing first and incrementing, but it should be parsed as *(x++); and cause an error.

See the fp-basic/starplusplus1.c0 and fp-basic/starplusplus4.c0 test cases.

A possible fix for this is to parse ++/-- as expressions but add a pass to make sure they are only used directly in expression statements, not as part of a larger expression.