You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
Hey, I almost missed that cbmc also supports C++.
I think it might make sense to update the documentation:
https://diffblue.github.io/cbmc/
and also the "About" text on GitHub:
The text was updated successfully, but these errors were encountered: