I am implementing flow-sensitive bounds in the Checked C compiler. Hopefully this can be complete for v1.0. If it is too much work, we should move it out of the specification.
I have already decided to make one change. The specification says that all flow-sensitive bounds declarations should agree at all points in a function and that the compiler should issue an error if they don't agree. We should make the inferred bounds be Unknown instead. If a programmer tries to access memory, the compiler will generate an error in that case. This will be much less burdensome on the programmer.
I am implementing flow-sensitive bounds in the Checked C compiler. Hopefully this can be complete for v1.0. If it is too much work, we should move it out of the specification.
I have already decided to make one change. The specification says that all flow-sensitive bounds declarations should agree at all points in a function and that the compiler should issue an error if they don't agree. We should make the inferred bounds be
Unknowninstead. If a programmer tries to access memory, the compiler will generate an error in that case. This will be much less burdensome on the programmer.