You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Jun 17, 2022. It is now read-only.
It would be helpful to know how much typechecking is done by ZZ. I was under the impression it did full typechecking, so I was surprised to find that the following program transpiled to C without error:
First of all zetz doesn't have a type checker. Let me know what wording sounded like it does, so we can fix that.
On the issue of this being an invalid cast. Zetz is a prove assistant for C. You can cast anything into anything as long as you don't violate any smt models. Since there aren't any, this passes.
However, zetz is supposed to catch UB by default, and this is UB, so this is still a bug. The issue is a) that printf is completely unconstrained until someone writes a model for it, but also b) a function pointer is unconstrained for backwards compat with union casts, which i havent figured out yet..
aep
changed the title
Clarify state of typechecker
cast of function pointer should not be allowed
Oct 13, 2020
Sign up for freeto subscribe to this conversation on GitHub.
Already have an account?
Sign in.
It would be helpful to know how much typechecking is done by ZZ. I was under the impression it did full typechecking, so I was surprised to find that the following program transpiled to C without error:
Of course, clang halted compilation with an error. Either way, it would help to clarify in the documentation about typechecking.
The text was updated successfully, but these errors were encountered: