News for hackers. Stuff that matters.

A comment on The C Bounded Model Checker: Criminally Underused. Parent comment

Re:The C Bounded Model Checker: Criminally Underused by jcranmer on Tuesday January 30, 2024 @03:04PM (#39194959)
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 integer overflows can't happen (!). So I'm not impressed.

[ Parent | on HN ]
Re:The C Bounded Model Checker: Criminally Underused by snnn on Wednesday January 31, 2024 @04:37AM (#39201832)
If you only test buffer overruns, VC++ static analyzer + SAL2 can do an excellent job on this. Basically if you annotate every pointer with a length, the compiler can tell you if a pointer arithmetic is safe or not.
[ Parent | on HN ]