search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
850 stars 265 forks source link

Make C++ support more visible #8272

Open intrigus-lgtm opened 7 months ago

intrigus-lgtm commented 7 months ago

Hey, I almost missed that cbmc also supports C++.

I think it might make sense to update the documentation: https://diffblue.github.io/cbmc/

CBMC is a model checker for C and C++.

and also the "About" text on GitHub:

C and C++ Bounded Model Checker

martin-cs commented 6 months ago

Maybe?

You are correct that CBMC has had a C++ front-end for ... more than half of it's two decades of existence. However there are a few problems with it which make it harder to use than we would like.

The problem is that most implementations of the standard template library ( STL ) use a lot of template meta-programming. This means that to support even the most basic code that #include with a modern, mainstream STL implementation, you have to support a very large amount of template code that is not really used anywhere but the internals of the STL and maybe Boost and is completely irrelevant for what you are trying to verify. This is a huge amount of work and so far no-one has been willing to commit either the time or the funding to do it.

So what can you do?

A. Use a different STL implementation. An older one or one designed for simpler targets might work.

B. You can write your own versions of the STL headers that you need, maybe using the modelling features in CBMC https://diffblue.github.io/cbmc/cprover-manual/index.html This will likely perform much better than using a real STL.

C. At points there have been tools that translate C++ into C.

While I am muddying the waters I might also point out that there are several other language front-ends which are significantly more useful than the C++ one. I think the rough order of utility is:

  1. ANSI C : production use
  2. Rust (via https://github.com/model-checking/kani ) : production use
  3. The subset of JVM that is generated from Java : has been used in production
  4. Verilog : has been used in production
  5. C++ : works but doesn't support modern STL
  6. A roughly SPARK-like subset of Ada ( via https://github.com/diffblue/gnat2goto ) : used to work
  7. Sieman's Statement List language : status unknown

HTH