gradual-verification / gvc0

Gradually Verified C0
6 stars 5 forks source link

Run-time checks with char comparison should use char val not int val #56

Open jennalwise opened 1 year ago

jennalwise commented 1 year ago

In my cparser case study, I ran into a compiler issue in cc0 for a run-time check generated by the frontend containing 'c1->val == 0', which did not compile with cc0 because the type on the left is a char and the type on the right is an int. The original c0 program contains 'c1->val == '\0'', so the comparison produced is correct, because the backend is using the numeric value of 0 for '\0', which is the correct value. It is just unfortunate that c0 won't treat 0 implicitly as '\0' in this context.

So, we need to fix the frontend to translate numerics like this back into their ASCII char variant.