C only code or also c++ code?

[monicamarcus]

So far I managed to run the second example available from the web interface. What I would really need is to model-check C++ code. So please let me know whether ESBMC can verify C++ source code or only C source code?

I was also able to install ESBMC on my macOS computer. I tried to run it on the same second example from the web interface and after successfully parsing the code, it complains about not finding a symbol: __chkstk_darwin. It also says that esbmc was built for Mac OS X 11.6, but on my computer I have only version 10.13.6.

How can I fix this issue? Could I build esbmc for Mac OS X 10.13.6 ?

I tried using the following command:

esbmc doublelists.cc --unwind 12 -I /usr/lib/libSystem.B.dylib

But it does not help. In the file doublelists.cc I have the following code:

#include <assert.h>
int main() {
int i,j;
for(i=0; i<6; i++) {
j=i;
}
assert(j==i);
return j;
}

The file does compile with c++ and if I run the executable then the result is:

Assertion failed: (j==i), function main, file doublelists.cc, line 8
Abort trap: 6

Thanks and best regards,
Monica

[lucasccordeiro]

Dear @monicamarcus,

Many thanks for your interest in ESBMC++.

You can find ESBMC++, which handles C++03 programs, at https://ssvlab.github.io/esbmc/benchmarks/stvr_2021_experiments.zip.

We're currently expanding our clang C++ frontend (https://github.com/esbmc/esbmc/tree/master/src/clang-cpp-frontend) to support the most recent versions of the C++ standard. @kunjsong01 is leading this development.

Which version of the C++ standard do you want to verify?

BTW, you can find our journal paper at STVR 2022 and the video of our talk at ICST 2022 at:

Felipe R. Monteiro, Mikhail R. Gadelha, Lucas C. Cordeiro. Model checking C++ programs. In Softw. Test. Verification Reliab. 32(1), 2022. DOI, Video,

Best,
Lucas

[monicamarcus]

Dear Dr. Cordeiro @lucasccordeiro

Thank you very much for your reply. I shall check the links in your message.

Currently I am an Android programer (not a C++ programer) but in the past I learned and worked with some formal verification tools.

My interest is to prove to a friend of mine (who is a senior C++ software developer) that formal verification can be used to verify the correctness of C++ programs. The version would be C++20.

I had found the journal paper you mentioned in October 2021, but I only started to try esbmc a few days ago. I shall watch the video of the talk, thank you for suggesting them.

Thanks and best regards,
Monica

[monicamarcus]

Dear @kunjsong01

I've learned from Dr. Lucas Cordeiro that you are leading the project to develop esbmc++ to support the latest versions of C++. What version of C++ is supported at https://github.com/esbmc/esbmc/tree/master/src/clang-cpp-frontend ?

Thanks and best regards,
Monica

[kunjsong01]

Hi @monicamarcus,

The clang-cpp-frontend is not complete, still in an early development stage. I'm trying to bring it up to support C++11 before Q4 2022.

Cheers,
Kunjian

[lucasccordeiro]

@monicamarcus: we have advanced our C++ frontend quite a lot.

Would you happen to have some benchmarks that we can play with?