esbmc and the assert methods in C

[monicamarcus]

I ltried 3 of the short examples of C code shown in your documentation. Two of them use assert() and one uses __VERIFIER_assert() for certain boolean formulas as arguments. In each case, if I try first to compile the example using gcc or clang, I get a syntax error about the undefined method, assert respectively __VERIFIER_assert. The examples using assert() compile only if I add the line #include <assert.h> but if I run esbmc on those examples, it complains about not finding the header file.

esbmc does not need to include the definitions of the methods assert() and __VERIFIER_assert() in the programs submitted for verification.

What does esbmc understand by assert() and __VERIFIER_assert() ? What is the difference between them?

Thanks and best regards,
Monica

[lucasccordeiro]

Hello Monica,

There is no difference between __VERIFIER_assert(expr) and assert(expr). In particular, __VERIFIER_assert(expr) was used by SV-COMP (https://sv-comp.sosy-lab.org/2022) for many years which is not in use anymore.

So, I would recommend using assert() and adding the respective library <assert.h> to your code.

Best,
Lucas

[monicamarcus]

Hello Dr. Cordeiro,

Thank you for the reply.

If I run esbmc on the C code example adding <assert.h> to it, I get a fatal error:

fatal error: 'assert.h' file not found
#include <assert.h>
^~~~~~~~~~

If I run esbmc on the same C code example without adding <assert.h> to it, there are no problems. That is why I asked my questions in the first place. I still need to understand how esbmc finds the definition of assert(), if it cannot find the assert.h file.

I would appreciate it very much if you can explain.

Thanks and best wishes,
Monica

[monicamarcus]

Dr. Cordeiro,

I solved my problem with assert.h: I did not specify the complete path to the include folder. Now esbmc no longer complains about not finding assert.h.

Thanks and best regards,
Monica

[lucasccordeiro]

Dear Monica,

I'm glad to hear that you managed to run ESBMC on your computer.

If there is something that we can do to improve your experience with ESBMC, please let us know.

Best,
Lucas