esbmc call for support for CXXNoexceptExpr type

ESBMC version 7.8.1 64-bit x86_64 linux Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc Parsing ads_log.cpp.ipp Converting ERROR: Conversion of unsupported clang expr: "CXXNoexceptExpr" to expression CXXNoexceptExpr 0x560ca6e8bc38 </usr/lib/gcc/x86_64-linux-gnu/13/../../../../include/c++/13/bits/stl_vector.h:472:9, line:475:40> 'bool' -CallExpr 0x560ca6e8bbb0 <line:472:18, line:475:39> 'std::basic_string<char> *':'std::basic_string<char> *' |-ImplicitCastExpr 0x560ca6e8bb98 <line:472:18, col:23> 'std::basic_string<char> *(*)(std::basic_string<char> *, std::basic_string<char> *, std::basic_string<char> *, std::allocator<std::basic_string<char>> &) noexcept(noexcept(__relocate_a_1(std::__niter_base(__first), std::__niter_base(__last), std::__niter_base(__result), __alloc)))' <FunctionToPointerDecay> | -DeclRefExpr 0x560ca6e6ccf8 <col:18, col:23> 'std::basic_string *(std::basic_string *, std::basic_string *, std::basic_string *, std::allocator<std::basic_string> &) noexcept(noexcept(__relocate_a_1(std::__niter_base(__first), std::__niter_base(__last), std::__niter_base(__result), __alloc)))' lvalue Function 0x560ca6e6cb58 '__relocate_a' 'std::basic_string *(std::basic_string *, std::basic_string *, std::basic_string *, std::allocator<std::basic_string> &) noexcept(noexcept(__relocate_a_1(std::__niter_base(__first), std::__niter_base(__last), std::__niter_base(__result), __alloc)))' (FunctionTemplate 0x560ca340e838 '__relocate_a') non_odr_use_unevaluated |-ImplicitCastExpr 0x560ca6e8bbf0 <col:36, col:58> 'std::basic_string ' <LValueToRValue> | -CallExpr 0x560ca6e6af30 <col:36, col:58> 'std::basic_string<char> *' xvalue | -ImplicitCastExpr 0x560ca6e6af18 <col:36, col:56> 'auto ()() noexcept -> decltype(__declval<std::basic_string *>(0))' <FunctionToPointerDecay> | -DeclRefExpr 0x560ca6e6ae58 <col:36, col:56> 'auto () noexcept -> decltype(__declval<std::basic_string<char> *>(0))' lvalue Function 0x560ca6e6ad60 'declval' 'auto () noexcept -> decltype(__declval<std::basic_string<char> *>(0))' (FunctionTemplate 0x560ca3177fb0 'declval') non_odr_use_unevaluated |-ImplicitCastExpr 0x560ca6e8bc08 <line:473:8, col:30> 'std::basic_string<char> *' <LValueToRValue> | -CallExpr 0x560ca6e6b3f0 <col:8, col:30> 'std::basic_string *' xvalue | -ImplicitCastExpr 0x560ca6e6b3d8 <col:8, col:28> 'auto (*)() noexcept -> decltype(__declval<std::basic_string<char> *>(0))' <FunctionToPointerDecay> | -DeclRefExpr 0x560ca6e6b370 <col:8, col:28> 'auto () noexcept -> decltype(__declval<std::basic_string *>(0))' lvalue Function 0x560ca6e6ad60 'declval' 'auto () noexcept -> decltype(__declval<std::basic_string *>(0))' (FunctionTemplate 0x560ca3177fb0 'declval') non_odr_use_unevaluated |-ImplicitCastExpr 0x560ca6e8bc20 <line:474:8, col:30> 'std::basic_string ' <LValueToRValue> | -CallExpr 0x560ca6e6b8b0 <col:8, col:30> 'std::basic_string<char> *' xvalue | -ImplicitCastExpr 0x560ca6e6b898 <col:8, col:28> 'auto ()() noexcept -> decltype(__declval<std::basic_string *>(0))' <FunctionToPointerDecay> | -DeclRefExpr 0x560ca6e6b830 <col:8, col:28> 'auto () noexcept -> decltype(__declval<std::basic_string<char> *>(0))' lvalue Function 0x560ca6e6ad60 'declval' 'auto () noexcept -> decltype(__declval<std::basic_string<char> *>(0))' (FunctionTemplate 0x560ca3177fb0 'declval') non_odr_use_unevaluated -CallExpr 0x560ca6e6c780 <line:475:8, col:38> 'std::allocator<std::basic_string>' lvalue -ImplicitCastExpr 0x560ca6e6c768 <col:8, col:36> 'auto (*)() noexcept -> decltype(__declval<std::allocator<std::basic_string<char>> &>(0))' <FunctionToPointerDecay> -DeclRefExpr 0x560ca6e6c6a8 <col:8, col:36> 'auto () noexcept -> decltype(__declval<std::allocator<std::basic_string> &>(0))' lvalue Function 0x560ca6e6c5b0 'declval' 'auto () noexcept -> decltype(__declval<std::allocator<std::basic_string> &>(0))' (FunctionTemplate 0x560ca3177fb0 'declval') non_odr_use_unevaluated

ERROR: CONVERSION ERROR

Feb 27 '25 01:02 mark-071

Hi @mark-071 could you please provide a simple, reduced testcase that demonstrates the bug?

Feb 27 '25 01:02 intrigus-lgtm

Hi @mark-071 could you please provide a simple, reduced testcase that demonstrates the bug? os: ubuntu24.04, compiler: clang14 command: /usr/lib/llvm-14/bin/clang++ test.cpp -E -o test.cpp.ipp esbmc test.cpp.ipp

source code: test.cpp

#include <thread>
#include <atomic>
#include <chrono>
 
int shared_counter = 0;
 
void race_increment() {
    while (true) {
        shared_counter++;  
        std::this_thread::sleep_for(std::chrono::milliseconds(10));
    }
}
int main() {
    std::thread t1(race_increment);
    std::thread t2(race_increment);
    while (true) {
        std::this_thread::sleep_for(std::chrono::seconds(1));
    }
    t1.join(); 
    t2.join(); 
    return 0;
}

Feb 27 '25 03:02 mark-071

@intrigus-lgtm: Do you think you could take care of this issue?

Feb 27 '25 15:02 lucasccordeiro

@intrigus-lgtm: Do you think you could take care of this issue?

Yes. Should be a pretty simple fix.

Feb 27 '25 16:02 intrigus-lgtm