-
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...
-
InfluxDB
InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.
-
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.
-
-
tis-interpreter
Discontinued An interpreter for finding subtle bugs in programs written in standard C [GET https://api.github.com/repos/TrustInSoft/tis-interpreter: 404 - Not Found // See: https://docs.github.com/rest/repos/repos#get-a-repository]
-
This is also the backend for Kani - Amazon's formal verification tool for Rust.
https://github.com/model-checking/kani
-
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
