[ryao]

Here is a sound static analyzer that can identify all memory safety bugs in C/C++ code, among other kinds of bugs:

https://www.absint.com/astree/index.htm

You can use it to produce code that is semi-formally verified to be safe, with no need for extensions. It is used in the aviation and nuclear industries. Given that it is used only by industries where reliability is so important that money is no object, I never bothered to ask them how much it costs. Few people outside of those industries knows that it exists. It is a shame that the open source alternatives only support subsets of what it supports. The computing industry is largely focused on unsound approaches that are easier to do, but do not catch all issues.

If you want extensions, here is a version of C that relies on hardware features to detect pointer dereferences to the wrong places through capabilities:

https://github.com/CTSRD-CHERI/cheri-c-programming

It requires special CHERI hardware, although the hardware does exist.

[AlotOfReading]

Astree is a pain in the butt. Even if it were free, I'd recommend it to very few people. It's not usable without someone (often a team) being responsible for it full time.

TrustInSoft is the higher quality option, polyspace is the more popular option, and IKOS is probably the best open source option. I've also had luck with tools from Galois Inc and the increasingly dated rv-match tool.

[edwcross]

Funny you mentioned TrustInSoft but not its open-source origin (which is still under development and evolving in a different direction), Frama-C. I cannot compare it to IKOS, but their usefulness depends a lot on the type of code and verification needs.

[AlotOfReading]

I want to like Frama-C, but I've never managed to actually use it successfully on real projects and the repeated experiences have soured me on it. Getting a recent version installed was a serious chore last time I tried, and no one else is willing to deal with ACSL to get the full value.

[KsassPeuk]

At some point in the past you also posted the ACSL cast badly documented. I asked you what you needed exactly, but you probably missed the message. So let me try again:

What kind of documentation would you expect in addition to ACSL by Example and the WP tutorial?

[ryao]

Tell me more.