ltscombine has stack-use-after-scope issues, as reported by address sanitizer #1898
Description
Report by address sanitizer
"Failed" (exit code: 255)
------- Stderr: -------
=================================================================
==2636560==ERROR: AddressSanitizer: stack-use-after-scope on address 0x7f6d49715f90 at pc 0x5fd85d6c0cf1 bp 0x7f6d47dfe250 sp 0x7f6d47dfe248
READ of size 8 at 0x7f6d49715f90 thread T1
#0 0x5fd85d6c0cf0 in state_thread::compute_state(mcrl2::lts::lts_builder*, std::queue<unsigned long, std::__debug::deque<unsigned long, std::allocator<unsigned long>>>&, mcrl2::lts::detail::progress_monitor&, mcrl2::utilities::indexed_set<std::__debug::vector<unsigned long, std::allocator<unsigned long>>, false, std::hash<std::__debug::vector<unsigned long, std::allocator<unsigned long>>>, std::equal_to<std::__debug::vector<unsigned long, std::allocator<unsigned long>>>, std::allocator<std::__debug::vector<unsigned long, std::allocator<unsigned long>>>, std::__debug::deque<std::__debug::vector<unsigned long, std::allocator<unsigned long>>, std::allocator<std::__debug::vector<unsigned long, std::allocator<unsigned long>>>>>&, unsigned long const&, std::mutex&, std::unique_lock<std::mutex>&, std::mutex&, std::mutex&) /scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tools/experimental/ltscombine/lts_combine.cpp:341:24
#1 0x5fd85d6b8060 in state_thread::operator()(mcrl2::lts::lts_builder*, std::queue<unsigned long, std::__debug::deque<unsigned long, std::allocator<unsigned long>>>&, mcrl2::lts::detail::progress_monitor&, mcrl2::utilities::indexed_set<std::__debug::vector<unsigned long, std::allocator<unsigned long>>, false, std::hash<std::__debug::vector<unsigned long, std::allocator<unsigned long>>>, std::equal_to<std::__debug::vector<unsigned long, std::allocator<unsigned long>>>, std::allocator<std::__debug::vector<unsigned long, std::allocator<unsigned long>>>, std::__debug::deque<std::__debug::vector<unsigned long, std::allocator<unsigned long>>, std::allocator<std::__debug::vector<unsigned long, std::allocator<unsigned long>>>>>&, unsigned long, std::mutex&, std::mutex&, std::mutex&, std::mutex&, std::condition_variable&, unsigned long&) /scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tools/experimental/ltscombine/lts_combine.cpp:285:7
#2 0x5fd85d646071 in mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0::operator()() const /scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tools/experimental/ltscombine/lts_combine.cpp:576:11
#3 0x5fd85d646071 in void std::__invoke_impl<void, mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0>(std::__invoke_other, mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0&&) /usr/bin/../lib/gcc/x86_64-linux-gnu/13/../../../../include/c++/13/bits/invoke.h:61:14
#4 0x5fd85d646071 in std::__invoke_result<mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0>::type std::__invoke<mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0>(mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0&&) /usr/bin/../lib/gcc/x86_64-linux-gnu/13/../../../../include/c++/13/bits/invoke.h:96:14
#5 0x5fd85d646071 in void std::thread::_Invoker<std::tuple<mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0>>::_M_invoke<0ul>(std::_Index_tuple<0ul>) /usr/bin/../lib/gcc/x86_64-linux-gnu/13/../../../../include/c++/13/bits/std_thread.h:292:13
#6 0x5fd85d646071 in std::thread::_Invoker<std::tuple<mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0>>::operator()() /usr/bin/../lib/gcc/x86_64-linux-gnu/13/../../../../include/c++/13/bits/std_thread.h:299:11
#7 0x5fd85d646071 in std::thread::_State_impl<std::thread::_Invoker<std::tuple<mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0>>>::_M_run() /usr/bin/../lib/gcc/x86_64-linux-gnu/13/../../../../include/c++/13/bits/std_thread.h:244:13
#8 0x7f6d4b4ecdb3 (/lib/x86_64-linux-gnu/libstdc++.so.6+0xecdb3) (BuildId: ca77dae775ec87540acd7218fa990c40d1c94ab1)
#9 0x5fd85d5208cc in asan_thread_start(void*) asan_interceptors.cpp.o
#10 0x7f6d4b09caa3 in start_thread nptl/pthread_create.c:447:8
#11 0x7f6d4b129c6b in clone3 misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:78
Address 0x7f6d49715f90 is located in stack of thread T0 at offset 3984 in frame
#0 0x5fd85d643ae7 in mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long) /scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tools/experimental/ltscombine/lts_combine.cpp:513
This frame has 25 object(s):
[32, 40) 'nr_of_threads.addr'
[64, 120) 'outgoing_transitions' (line 515)
[160, 200) '__begin1' (line 516)
[240, 280) '__end1' (line 516)
[320, 568) 'states' (line 522)
[640, 696) 'initial_states' (line 523)
[736, 744) 'action_decls' (line 524)
[768, 1688) 'data_spec' (line 525)
[1824, 1832) 'proc_params' (line 526)
[1856, 1896) '__begin168' (line 527)
[1936, 1976) '__end171' (line 527)
[2016, 2024) 'ref.tmp105' (line 530)
[2048, 2968) 'ref.tmp124' (line 531)
[3104, 3112) 'ref.tmp143' (line 532)
[3136, 3240) 'queue' (line 537)
[3280, 3344) 'progress_monitor' (line 541)
[3376, 3384) 'lts_builder' (line 544)
[3408, 3448) 'builder_mutex' (line 559)
[3488, 3528) 'queue_mutex' (line 560)
[3568, 3608) 'progress_mutex' (line 561)
[3648, 3688) 'states_mutex' (line 562)
[3728, 3776) 'queue_cond' (line 565)
[3808, 3816) 'busy' (line 566)
[3840, 3896) 'threads' (line 568)
[3936, 3992) 'thread' (line 572) <== Memory access at offset 3984 is inside this variable
HINT: this may be a false positive if your program uses some custom stack unwind mechanism, swapcontext or vfork
(longjmp and C++ exceptions *are* supported)
SUMMARY: AddressSanitizer: stack-use-after-scope /scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tools/experimental/ltscombine/lts_combine.cpp:341:24 in state_thread::compute_state(mcrl2::lts::lts_builder*, std::queue<unsigned long, std::__debug::deque<unsigned long, std::allocator<unsigned long>>>&, mcrl2::lts::detail::progress_monitor&, mcrl2::utilities::indexed_set<std::__debug::vector<unsigned long, std::allocator<unsigned long>>, false, std::hash<std::__debug::vector<unsigned long, std::allocator<unsigned long>>>, std::equal_to<std::__debug::vector<unsigned long, std::allocator<unsigned long>>>, std::allocator<std::__debug::vector<unsigned long, std::allocator<unsigned long>>>, std::__debug::deque<std::__debug::vector<unsigned long, std::allocator<unsigned long>>, std::allocator<std::__debug::vector<unsigned long, std::allocator<unsigned long>>>>>&, unsigned long const&, std::mutex&, std::unique_lock<std::mutex>&, std::mutex&, std::mutex&)
Shadow bytes around the buggy address:
0x7f6d49715d00: 00 00 f2 f2 f2 f2 00 f2 f2 f2 00 00 00 00 00 f2
0x7f6d49715d80: f2 f2 f2 f2 00 00 00 00 00 f2 f2 f2 f2 f2 00 00
0x7f6d49715e00: 00 00 00 f2 f2 f2 f2 f2 00 00 00 00 00 f2 f2 f2
0x7f6d49715e80: f2 f2 00 00 00 00 00 00 f2 f2 f2 f2 00 f2 f2 f2
0x7f6d49715f00: 00 00 00 00 00 00 00 f2 f2 f2 f2 f2 f8 f8 f8 f8
=>0x7f6d49715f80: f8 f8[f8]f3 f3 f3 f3 f3 00 00 00 00 00 00 00 00
0x7f6d49716000: f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5
0x7f6d49716080: f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5
0x7f6d49716100: f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5
0x7f6d49716180: f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5
0x7f6d49716200: f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5 f5
Shadow byte legend (one shadow byte represents 8 application bytes):
Addressable: 00
Partially addressable: 01 02 03 04 05 06 07
Heap left redzone: fa
Freed heap region: fd
Stack left redzone: f1
Stack mid redzone: f2
Stack right redzone: f3
Stack after return: f5
Stack use after scope: f8
Global redzone: f9
Global init order: f6
Poisoned by user: f7
Container overflow: fc
Array cookie: ac
Intra object redzone: bb
ASan internal: fe
Left alloca redzone: ca
Right alloca redzone: cb
Thread T1 created by T0 here:
#0 0x5fd85d508755 in pthread_create (/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/build/stage/bin/ltscombine+0x189755) (BuildId: 56a5002262107244e298e381b495e21f89d2fb44)
#1 0x7f6d4b4eceb0 in std::thread::_M_start_thread(std::unique_ptr<std::thread::_State, std::default_delete<std::thread::_State>>, void (*)()) (/lib/x86_64-linux-gnu/libstdc++.so.6+0xeceb0) (BuildId: ca77dae775ec87540acd7218fa990c40d1c94ab1)
#2 0x5fd85d645bdd in std::thread::thread<mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0, void>(mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0&&) /usr/bin/../lib/gcc/x86_64-linux-gnu/13/../../../../include/c++/13/bits/std_thread.h:164:2
#3 0x5fd85d645bdd in decltype(::new((void*)(0)) std::thread(std::declval<mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0>())) std::construct_at<std::thread, mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0>(std::thread*, mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0&&) /usr/bin/../lib/gcc/x86_64-linux-gnu/13/../../../../include/c++/13/bits/stl_construct.h:97:39
#4 0x5fd85d644cd5 in void std::allocator_traits<std::allocator<std::thread>>::construct<std::thread, mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0>(std::allocator<std::thread>&, std::thread*, mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0&&) /usr/bin/../lib/gcc/x86_64-linux-gnu/13/../../../../include/c++/13/bits/alloc_traits.h:540:4
#5 0x5fd85d644cd5 in void std::__cxx1998::vector<std::thread, std::allocator<std::thread>>::_M_realloc_insert<mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0>(__gnu_cxx::__normal_iterator<std::thread*, std::__cxx1998::vector<std::thread, std::allocator<std::thread>>>, mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0&&) /usr/bin/../lib/gcc/x86_64-linux-gnu/13/../../../../include/c++/13/bits/vector.tcc:468:4
#6 0x5fd85d644cd5 in std::thread& std::__cxx1998::vector<std::thread, std::allocator<std::thread>>::emplace_back<mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0>(mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0&&) /usr/bin/../lib/gcc/x86_64-linux-gnu/13/../../../../include/c++/13/bits/vector.tcc:123:4
#7 0x5fd85d644cd5 in std::thread& std::__debug::vector<std::thread, std::allocator<std::thread>>::emplace_back<mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0>(mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long)::$_0&&) /usr/bin/../lib/gcc/x86_64-linux-gnu/13/../../../../include/c++/13/debug/vector:519:11
#8 0x5fd85d644cd5 in mcrl2::combine_lts(std::__debug::vector<mcrl2::lts::lts_lts_t, std::allocator<mcrl2::lts::lts_lts_t>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::aterm_string, std::allocator<atermpp::aterm_string>>&, std::__debug::vector<atermpp::term_list<atermpp::aterm_string>, std::allocator<atermpp::term_list<atermpp::aterm_string>>>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>, bool, unsigned long) /scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tools/experimental/ltscombine/lts_combine.cpp:573:13
#9 0x5fd85d5dc86c in mcrl2::ltscombine_tool::run() /scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tools/experimental/ltscombine/ltscombine.cpp:57:5
#10 0x5fd85d565216 in mcrl2::utilities::tools::tool::execute(int, char**) /scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/libraries/utilities/include/mcrl2/utilities/tool.h:212:22
#11 0x5fd85d5638c5 in main /scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tools/experimental/ltscombine/ltscombine.cpp:311:35
#12 0x7f6d4b02a1c9 in __libc_start_call_main csu/../sysdeps/nptl/libc_start_call_main.h:58:16
#13 0x7f6d4b02a28a in __libc_start_main csu/../csu/libc-start.c:360:3
#14 0x5fd85d487f94 in _start (/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/build/stage/bin/ltscombine+0x108f94) (BuildId: 56a5002262107244e298e381b495e21f89d2fb44)
==2636560==ABORTING
Traceback (most recent call last):
File "/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tests/random/random_testing.py", line 695, in main
test.execute_in_sandbox()
File "/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tests/random/../../tests/utility/testing.py", line 383, in execute_in_sandbox
self.execute()
File "/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tests/random/random_testing.py", line 51, in execute
super().execute()
File "/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tests/random/../../tests/utility/testing.py", line 368, in execute
result = self._run()
^^^^^^^^^^^
File "/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tests/random/../../tests/utility/testing.py", line 305, in _run
raise e
File "/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tests/random/../../tests/utility/testing.py", line 278, in _run
returncode = tool.execute(
^^^^^^^^^^^^^
File "/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tests/random/../../tests/utility/tools.py", line 175, in execute
process = RunProcess(name, args + self.args, memlimit, timeout)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tests/random/../../tests/utility/run_process.py", line 156, in __init__
raise ToolRuntimeError(
tests.utility.run_process.ToolRuntimeError: 'Tool /scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/build/stage/bin/ltscombine [\'/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/build/tests/workspace/ltscombine_0/l5.lts\', \'/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/build/tests/workspace/ltscombine_0/l6.lts\', \'/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/build/tests/workspace/ltscombine_0/l7.lts\', \'--hide=a\', \'--allow=a,b\', \'--comm="a|b->c"\'] ended with return code 1'
Contents of file l1.mcrl2:
act
a,c,b,d;
proc
P = a;
Q = (((true) -> (a)) + (sum b1: Bool. ((delta) . (((delta) . (a | b)) . (a))))) . (d);
R = a;
init
((R) || (Q)) || (P);
Contents of file l2.mcrl2:
act
a,c,b,d;
proc
P = ((sum b1: Bool. ((true) -> (c))) + (a)) + (d);
Q = d;
R = (delta) . (a);
init
block({d}, ((R) || (P)) || (Q));
Contents of file l10.mcrl2:
act Terminate,a,c,b,d;
proc P(x: Pos) =
(x == 1) ->
a .
P(x = 2)
+ (x == 1) ->
a .
P(x = 3)
+ (x == 1) ->
a|a .
P(x = 4)
+ (x == 1) ->
a .
P(x = 5)
+ (x == 1) ->
a|a .
P(x = 6)
+ (x == 1) ->
a|a .
P(x = 7)
+ (x == 1) ->
a|a|a .
P(x = 8)
+ (x == 2) ->
a .
P(x = 4)
+ (x == 2) ->
a .
P(x = 6)
+ (x == 2) ->
a|a .
P(x = 8)
+ (x == 3) ->
a .
P(x = 4)
+ (x == 3) ->
d .
P(x = 9)
+ (x == 3) ->
a|d .
P(x = 10)
+ (x == 3) ->
a .
P(x = 7)
+ (x == 3) ->
a|a .
P(x = 8)
+ (x == 3) ->
a|d .
P(x = 11)
+ (x == 3) ->
a|a|d .
P(x = 12)
+ (x == 4) ->
d .
P(x = 10)
+ (x == 4) ->
a .
P(x = 8)
+ (x == 4) ->
a|d .
P(x = 12)
+ (x == 5) ->
a .
P(x = 6)
+ (x == 5) ->
a .
P(x = 7)
+ (x == 5) ->
a|a .
P(x = 8)
+ (x == 6) ->
a .
P(x = 8)
+ (x == 7) ->
a .
P(x = 8)
+ (x == 7) ->
d .
P(x = 11)
+ (x == 7) ->
a|d .
P(x = 12)
+ (x == 8) ->
d .
P(x = 12)
+ (x == 9) ->
a .
P(x = 10)
+ (x == 9) ->
a .
P(x = 11)
+ (x == 9) ->
a|a .
P(x = 12)
+ (x == 10) ->
a .
P(x = 12)
+ (x == 11) ->
a .
P(x = 12)
+ (x == 12) ->
Terminate .
P(x = 13)
+ delta;
init P(1);
Contents of file l11.mcrl2:
act a,c,b,d;
proc P(x: Pos) =
(x == 1) ->
c .
P(x = 2)
+ (x == 1) ->
c .
P(x = 2)
+ (x == 1) ->
a .
P(x = 2)
+ delta;
init P(1);
#--- commands ---#
mcrl22lps l1.mcrl2 l3.lps -n
mcrl22lps l2.mcrl2 l4.lps -n
lps2lts l3.lps l5.lts
lps2lts l4.lps l6.lts
lts2lps l5.lts -l l3.lps l8.lps
lpspp l8.lps l10.mcrl2
lts2lps l6.lts -l l3.lps l9.lps
lpspp l9.lps l11.mcrl2
ltscombine l5.lts l6.lts l7.lts --hide=a --allow=a,b --comm="a|b->c"
/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/src/tests/utility/../scripts/ltscombine_naive.py l10.mcrl2 l11.mcrl2 l12.mcrl2 --hide=a --allow=a,b --comm=a|b->c
mcrl22lps l12.mcrl2 l13.lps
lps2lts l13.lps l14.lts
ltscompare l7.lts l14.lts -ebisim
An exception occurred: <class 'tests.utility.run_process.ToolRuntimeError'> 'Tool /scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/build/stage/bin/ltscombine [\'/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/build/tests/workspace/ltscombine_0/l5.lts\', \'/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/build/tests/workspace/ltscombine_0/l6.lts\', \'/scratch/teamcity/BuildAgent/work/c1149d302b50fc7c/build/tests/workspace/ltscombine_0/l7.lts\', \'--hide=a\', \'--allow=a,b\', \'--comm="a|b->c"\'] ended with return code 1'