esbmc
Installation Generally (And FreeBSD specifically)...
The installation process isn't made very clear.
Your github page for FreeBSD makes the process quite unclear, to quote from it, it states:
"pkg install git cmake python3 z3 bison flex boost-all wget https://github.com/llvm/llvm-project/releases/download/llvmorg-16.0.0/clang+llvm-16.0.0-amd64-unknown-freebsd13.tar.xz && mv clang16 mkdir build && cd build cmake .. -DLLVM_DIR=../clang16 -DClang_DIR=../clang16 make -j4"
But, it doesn't make sense:
- the first line suggests particular packages that might need to be installed, of which python3 is likely already installed. It suggests installing a regular z3 package, but not a dev version of the package that would allow interprocess communication -- there is a dev-version of that package for GNU/Linux platforms, but checking for my FreeBSD, no such package (or pre-built binary exists).
1.1) When you actually build via cmake (that's the time when the user gets to pick which solver (if any) they want (I'll explain that point a bit later down in this issue)
- The immediate next line is wget (but that's a GNU/Linux standard binary that's available in userland, but it's not standard on FreeBSD), True, one can install it to meet the requirement, but then the initial list should list wget (but you can do the same via curl, etc).
2.1) The second line is broken just in terms of regular syntax -- from what you want the user to have achieved -- and from will actually be achieved.
2.11) So, the line really says download the clang llvm build 16.0 (but for a highly specific version of FreeBSD) but the next command assumes the user has already unpacked the downloaded archive, but the mv command isn't fully populated in terms of the parameters to the command, so of course, running mv clang16 won't do anything but generate an error (but it's clear what's meant)
-
The first parameter to cmake (here "..") is unused and ignored, so not entirely helpful.
-
When you configure the install-scripts via cmake, one runs into a problem that the installer allows the user to configure the system without any solvers built-in. If one tries to add solvers in, then, if one wants say z3, one has to manually search down the path by searching for it via its own github page.
4.1) If one searches in this way, one of the solvers (boolector) would seem to be deprecated and replaced by bitwuzla
4.2) If you try and run the test programmes via:
https://ssvlab.github.io/esbmc/documentation.html
You'll find that in my setup (ESBMC version 7.8.1 64 bit x86_64 freebsd, w/ solvers smtlib, z3, bitwuzla, smtlib) you can't actually run a lot of the examples properly.
(smtlib gives you 2 version, 1 that's unstable, 1 that doesn't do anything obvious, since it's about piping output to a different programme).
4.3) Worse, the first illustrative example, I can't run in C++ mode, only as C, even though it could (by the code) be either. (Even though I have to add the header assert). Nevertheless, in my setup, I can't get a good response out of ESBMC (since with my solvers, even in C, it runs forever).
4.3.1) If I'm trying to call that initial programme as if it's in C++ mode, I run into these type checker problems [1], so, the argument --floatbv doesn't work (it wants me to specify isnanf (the type specific version of isnan) -- and the type-mismatch that can't be so easily fixed -- is based on a path that doesn't exist)
4.3.2) When I was compiling I saw errors about the C++ coding style -- including problems that my clang compiler is version 18 something and that certain features are to be deprecated. (The deprecated feature is char_traits (which will be removed in LLVM 19, I'm on an 18 version of LLVM (clang))
4.3.3) If you look at how the esbmc programme works behind the scenes, it appears to use the char_traits function to be able to do the symbolic algebraic manipulation of the programme (the char traits deprecation relates to the fact that as from version 19, you can only use it for certain limited types in the language not for a wider range as is currently temporarily allowed).
4.3.4) see output (attached) -- I couldn't attach -- so see [2]
4.3.5) After installing, I can get proper output on some of my old ANSI C programmes that don't do anything useful (just a simple macro system I wrote in the past for typesetting) -- but for the more advanced examples it depends that you have the right solver installed -- and that's not obvious the first time you install esbmc
[1] ESBMC version 7.8.1 64-bit x86_64 freebsd Target: 64-bit little-endian x86_64-unknown-freebsd with esbmclibc Parsing clipboard.cpp In file included from clipboard.cpp:1: In file included from /tmp/esbmc-cpp-headers-75fe-3fab-3453/math.h:13: In file included from /usr/include/c++/v1/math.h:301: In file included from /usr/include/math.h:20: /usr/include/sys/_types.h:95:26: error: cannot combine with previous 'type-name' declaration specifier typedef __uint_least16_t __char16_t; ^ /usr/include/sys/_types.h:96:26: error: cannot combine with previous 'type-name' declaration specifier typedef __uint_least32_t __char32_t; ^ clipboard.cpp:6:16: error: use of undeclared identifier 'isnan'; did you mean 'isnanf'? if(x <= 0 || isnan(x)) ^~~~~ isnanf /usr/include/math.h:320:5: note: 'isnanf' declared here int isnanf(float) __pure2; ^ ERROR: PARSING ERROR
[2] ESBMC version 7.8.1 64-bit x86_64 freebsd Target: 64-bit little-endian x86_64-unknown-freebsd with esbmclibc Parsing /home/russ/bitmaplarge/test.cpp Converting Generating GOTO Program GOTO program creation time: 0.235s GOTO program processing time: 0.001s Starting Bounded Model Checking Symex completed in: 0.000s (18 assignments) Slicing time: 0.000s (removed 9 assignments) Generated 1 VCC(s), 1 remaining after simplification (9 assignments) ERROR: No solver backends built into ESBMC; please either build some in, or explicitly configure the smtlib backend
Signal 6, backtrace: 0x1ca3821 <_ZL16segfault_handleri+0x31> at /usr/local/bin/esbmc 0x80c9a82d0 <pthread_sigmask+0x540> at /lib/libthr.so.3 0x80c9a788b <pthread_setschedparam+0x84b> at /lib/libthr.so.3 0x7ffffffff2d3 <_fini+0x7ffffc5303b7> at ??? 0x81022a54a <__sys_thr_kill+0xa> at /lib/libc.so.7 0x8101a4414 <__raise+0x34> at /lib/libc.so.7 0x8102542d9 <abort+0x49> at /lib/libc.so.7 0x1f6368d <_Z13create_solverNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEERK10namespacetRK8optionst+0x5bd> at /usr/local/bin/esbmc 0x1cc09fb <_ZN4bmct10run_threadERNSt3__110shared_ptrI22symex_target_equationtEE+0x96b> at /usr/local/bin/esbmc 0x1cbfc19 <_ZN4bmct3runERNSt3__110shared_ptrI22symex_target_equationtEE+0x289> at /usr/local/bin/esbmc 0x1cbf89f <_ZN4bmct9start_bmcEv+0x1f> at /usr/local/bin/esbmc 0x1ca776f <_ZN19esbmc_parseoptionst6do_bmcER4bmct+0x4f> at /usr/local/bin/esbmc 0x1ca3f3e <_ZN19esbmc_parseoptionst4doitEv+0x64e> at /usr/local/bin/esbmc
