Strange problems encountered with uppaal 5.0.0

[Lqs66]

I'm using UPPAAL's external function feature in my model.

When I run . /verifyta ~/Desktop/uppllvm/python/rtl.xml, I encounter a Segmentation fault (core dumped), which suggests that I need to debug it.

But when I debugged it (using gdb --args ./verifyta ~/Desktop/uppllvm/python/rtl.xml) using gdb, everything worked fine.

Here is my model:
rtl.zip

[mikucionisaau]

Non-deterministic behavior like this is usually caused by undefined behavior, most often triggered by incorrect use of memory.

The library depends on many other libraries I don't have:

$ ldd libbase.so 
	linux-vdso.so.1 (0x00007fffde3b3000)
	libyaml-cpp.so.0.8 => /lib/x86_64-linux-gnu/libyaml-cpp.so.0.8 (0x000072b1f89ca000)
	libllvmloader.so => not found
	libmodel.so => not found
	libsupport.so => not found
	libstdc++.so.6 => /lib/x86_64-linux-gnu/libstdc++.so.6 (0x000072b1f8600000)
	libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x000072b1f88df000)
	libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x000072b1f88b2000)
	libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x000072b1f8200000)
	/lib64/ld-linux-x86-64.so.2 (0x000072b1f8bc5000)

Anyway, I cannot help you to debug your library without sources.

I strongly suggest creating a test executable for your library which mimics the calls from your model and debug from there. In such setup, you can enable undefined behavior and address sanitizers (see man gcc for -fsanitize=undefined and -fsanitize=address, or man clang if you are using llvm), which can easily find the offending code.

[Lqs66]

Thanks for the reply, I will keep trying it.

[mikucionisaau]

Alternatively, you can try running within valgrind -- that's equivalent to address sanitizer, except it has ~100x of execution overhead, but it should be fast enough when the program fails early.