A user raised some confusion with the wording about Contracts in your documentation which was not answered and is still there. I think it should be fixed since there are lots of people who are confused about contracts and how it differs from error handling. Add to this people's confusion about asserts at runtime and how the optimizer may mess it up and you have a veritable rat's nest of confused thoughts/opinions.
Is your approach to static analysis/verification something like what Frama-C does? I had always wished somebody would wrap C/C++ with a full blown static analysis/verification plus runtime framework and make everything into a single integrated whole like for example the Dafny language. Everything should be doable in a single implementation language with annotations as needed.
A user raised some confusion with the wording about Contracts in your documentation which was not answered and is still there. I think it should be fixed since there are lots of people who are confused about contracts and how it differs from error handling. Add to this people's confusion about asserts at runtime and how the optimizer may mess it up and you have a veritable rat's nest of confused thoughts/opinions.
Is your approach to static analysis/verification something like what Frama-C does? I had always wished somebody would wrap C/C++ with a full blown static analysis/verification plus runtime framework and make everything into a single integrated whole like for example the Dafny language. Everything should be doable in a single implementation language with annotations as needed.