alt Hacker Newsas someone building an analyzer for zig, if you sent something like this through the system im building, it would get handled by Zig's optional type tagging; but lets say you did "free" (so your result is half freed, half not freed): it would get rejected because both branches produce inconsistent type refinements, you don't have to solve the halting problem, just analyze all possible branches and seek convergence.
Replies
> just analyze all possible branches and seek convergence.
This sounds like a very simple form of abstract interpretation, how do you handle the issues it generally brings?
For example if after one branch you don't converge, but after two you do, do you accept that? What if this requires remembering the relationship between variables? How do you represent these relationships?
Historically this has been a tradeoff between representing the state space with high or perfect precision, which however can require an exponential amount of memory/calculations, or approximate them with an abstract domain, which however tend to lose precision after performing certain operations.
Add dynamically sized values (e.g. arrays) and loops/recursion and now you also need to simulate a possibly unbounded number of iterations.
Rust is the poster child for these complaints, but this is a great example of "the language rejects a valid program". Not all things that can be expressed in C are good ideas!
This is "valid" C, but I wholly support checking tools that reject it.