The C Bounded Model Checker: Criminally Underused

• dmd

  146 2,888 9.9 D

  dmd D Programming Language compiler

  

Thank you for the explanation.

I agree that if one isn't going to enhance C, one is going to have to resort to these tools.

C gets new features now and then. Why not add something incredibly useful, like the slice proposal? Instead, C23 got enhanced with the crazy Unicode identifiers. Richard Cattermole has been adding them to D's C support, requiring 6000 lines of code!!

https://github.com/dlang/dmd/pull/15307

The entire C parser is 6000 lines of code:

https://github.com/dlang/dmd/blob/master/compiler/src/dmd/cp...

• coreHTTP

  1 68 5.4 C

  Client implementation of a subset of HTTP 1.1 protocol designed for embedded devices.

  

One of the examples they gave was an HTTP client, which would be a surprisingly non-toy example, so I looked at what they actually did in the code (https://github.com/FreeRTOS/coreHTTP/tree/main/test/cbmc).

Not that I'm an expert in processing what exactly is being tested, but it basically looks only able to prove that an individual function doesn't overrun buffers. If you tell it to assume that overflows can't happen (!). So I'm not impressed.

• WorkOS

  workos.com sponsored

  The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

  

• c-semantics

  4 301 1.8 C

  Semantics of C in K

  

• tis-interpreter

  2 561 10.0 OCaml

  An interpreter for finding subtle bugs in programs written in standard C

  

• kani

  47 1,900 9.5 Rust

  Kani Rust Verifier

  

This is also the backend for Kani - Amazon's formal verification tool for Rust.

https://github.com/model-checking/kani

• cbmc

  5 752 9.9 C++

  C Bounded Model Checker

  

https://github.com/diffblue/cbmc/issues/7732 I'll note that some form of undefined behavior checking / documentation is on the roadmap for the next major version

Suggest a related project