XLiZHI
commented
8 months ago Closed intrigus-lgtm closed 2 months ago
XLiZHI
commented
8 months ago 
fbrausse
commented
8 months ago @intrigus-lgtm At the moment, running ESBMC with either --no-library or --no-abstracted-cpp-includes on programs that use the C or C++ standard library is not supported in a platform-independent manner, which we aim at: ESBMC runs on Linux, Windows and MacOS. May I ask for what reason you expect ESBMC to work correctly on C++ programs using those libraries while passing --no-library and/or --no-abstracted-cpp-includes?
~Note also that <string_view> is only available since C++17. You can pass --cppstd 17 or higher for that to ESBMC to enable those later additions from the system's default library implementation.~ Edit: sorry, I missed you're using this option already.
intrigus-lgtm
commented
8 months ago May I ask for what reason you expect ESBMC to work correctly on C++ programs using those libraries while passing --no-library and/or --no-abstracted-cpp-includes?
No particular reason, but I thought I don't need any of the existing models and didn't want to spend time to model them (and esbmc --help listed the options^^).
My end goal is to verify some custom asserts, I don't really care about any existing memory checks right now.
At the moment, running ESBMC with either --no-library or --no-abstracted-cpp-includes on programs that use the C or C++ standard library is not supported in a platform-independent manner
May I ask what the issue is on other platforms or is there an existing issue?
fbrausse
commented
8 months ago No particular reason, but I thought I don't need any of the existing models and didn't want to spend time to model them (and
esbmc --helplisted the options^^). My end goal is to verify some custom asserts, I don't really care about any existing memory checks right now.
Good point, thanks. Those options are primarily for debugging system compatibilty. We should move them to the "Debug" section.
If you're not interested in pointer or other checks for now, these can selectively be disabled (listed in help message under "Property checking"). Memory leak checks are opt-in.
--no-bounds-check do not do array bounds check
--no-pointer-check do not do pointer check
--no-align-check do not check pointer alignment
--memory-leak-check enable memory leak check
[...]Maybe to clarify: The models distributed with ESBMC are generally provided to cover a larger range of language and library features and to speed up verification. System library headers are too different in their implementations and also assume a specific library implementation which ESBMC doesn't have access to when running. So it should be fine to keep the models enabled.
As for C++, it's a work in progress since the library is so large. In particular supporting the system's \<iostream> is tricky because it combines lots of C++ features into a single implementation (exceptions, virtual methods, templates). For simpler C++ programs with user-defined types there should be fewer issues, but feel free to open bugs here for ones with the library as well.
At the moment, running ESBMC with either --no-library or --no-abstracted-cpp-includes on programs that use the C or C++ standard library is not supported in a platform-independent manner
May I ask what the issue is on other platforms or is there an existing issue?
Sure, there are parts of the libraries that we need to model ourselves and where it's near impossible to work with the arbitrary types the varying system libraries provide, pthreads is one such example. Another one: We'd also like to have some control over the floating point environment, so \<fenv.h> shouldn't be taken from the system because the constants for the rounding modes FE_UPWARD etc. could vary.
fbrausse
commented
2 months ago Either option is incompatible with programs that actually include library headers. I'll close this for now. Please reopen if a concrete problem can be described.
Information
ESMB version:
ESBMC version 7.5.0 64-bit x86_64 linuxKernel/OS:Linux debian 6.1.0-17-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.69-1 (2023-12-30) x86_64 GNU/LinuxGCC version:gcc (Debian 12.2.0-14) 12.2.0Clang version:Debian clang version 14.0.6 Target: x86_64-pc-linux-gnuCode
If we run
esbmc --cppstd 17 --input-file cpptest.cpp --no-abstracted-cpp-includes --no-librarywe get the following errors:If we run
esbmc --cppstd 17 --input-file cpptest.cpp --no-abstracted-cpp-includeswe get the following errors:If we run
esbmc --cppstd 17 --input-file cpptest.cpp --no-librarywe get the following errors:If we run
esbmc --cppstd 17 --input-file cpptest.cppwe get the following errors:Expected Result
ESBMC successfully compiles the file.