This repository was archived by the owner on Jun 17, 2022. It is now read-only.
Repository navigation
This repository was archived by the owner on Jun 17, 2022. It is now read-only.
cast of function pointer should not be allowed #139
Description
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:
using <stdio.h>::{printf};
fn output(int *x) {
printf("%d\n", *x);
}
fn function() {}
export fn main() -> int {
output(function);
}Of course, clang halted compilation with an error. Either way, it would help to clarify in the documentation about typechecking.
Activity
aep commentedon Oct 13, 2020
so there's multiple answers to this.
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..
[-]Clarify state of typechecker[/-][+]cast of function pointer should not be allowed[/+]