Meijuh
commented
7 years ago @alaarman I have made a bit of an improvement, so that an assertion is actually triggered. This assertion shows why the segfault occurs. I do not know how to fix this though, can you look at it?
alaarman
In next branch, pins2lts-seq seems seriously broken: it's crashing in any run where por is activated.
Here are some invocation traces + a debugger run with symbols. Reproduce with attached files (simple model Eratosthenes 10) and command :
pins2lts-seq ./gal.so -p --pins-guards --when -i "EratosthenesPT010ReachabilityCardinality0==true"
Note that substituting pins2lts-mc resolves the problem. gal.zip
(gdb) r ./gal.so -p --pins-guards --when -i "EratosthenesPT010ReachabilityCardinality0==true" Starting program: /data2/ythierry/GITHOME/ITS-Tools-Dependencies/ltsmin/src/pins2lts-seq/pins2lts-seq ./gal.so -p --pins-guards --when -i "EratosthenesPT010ReachabilityCardinality0==true" [Thread debugging using libthread_db enabled] Using host libthread_db library "/lib64/libthread_db.so.1". pins2lts-seq, 0.000: Registering PINS so language module pins2lts-seq, 0.000: Loading model from ./gal.so pins2lts-seq, 0.001: library has no initializer pins2lts-seq, 0.001: loading model GAL pins2lts-seq, 0.001: completed loading model GAL pins2lts-seq, 0.001: Initializing POR dependencies: labels 14, guards 8 pins2lts-seq, 0.002: Forcing the use of a cycle proviso. For best results use --proviso=color. pins2lts-seq, 0.002: There are 14 state labels and 1 edge labels pins2lts-seq, 0.002: State length is 5, there are 8 groups pins2lts-seq, 0.002: Running dfs search strategy pins2lts-seq, 0.002: Using a tree for state storage pins2lts-seq, 0.002: Visible groups: 0 / 8, labels: 1 / 14 pins2lts-seq, 0.002: POR cycle proviso: stack
Program received signal SIGSEGV, Segmentation fault. 0x00007ffff6e0db98 in main_arena () from /lib64/libc.so.6 (gdb) bt
0 0x00007ffff6e0db98 in main_arena () from /lib64/libc.so.6
1 0x00000000004fe5f9 in por_seen (dst=0xad9b48, group=0, src_changed=false) at pins2pins-por.c:210
2 0x00000000004fe6d5 in seen_cb (context=0xac43a0, ti=0x7fffffffc360, dst=0xad9b48, cpy=0x7ffff6a5f5e0) at pins2pins-por.c:223
3 0x00007ffff685cda5 in next_state () from /data2/ythierry/GITHOME/ITS-Tools-pnmcc/INPUTS/Eratosthenes-PT-010/gal.so
4 0x00000000004a5b0e in default_all (self=0xab4060, src=0xad9a80, cb=0x4fe600, context=0xac43a0) at pins.c:286
5 0x00000000004a77df in GBgetTransitionsAll (model=0xab4060, src=0xad9a80, cb=0x4fe600, context=0xac43a0) at pins.c:885
6 0x00000000004fe7de in por_seen_groups (ctx=0xac43a0, src=0xad9a80, src_changed=0) at pins2pins-por.c:239
7 0x00000000004fe8c7 in por_init_transitions (model=0xac0bb0, ctx=0xac43a0, src=0xad9a80) at pins2pins-por.c:261
8 0x000000000050730f in beam_setup (model=0xac0bb0, ctx=0xac43a0, src=0xad9a80) at por-beam.c:669
9 0x00000000005074fd in beam_search_all (self=0xac0bb0, src=0xad9a80, cb=0x4a3a25, user_context=0x7fffffffd5c0) at por-beam.c:711
10 0x00000000004a77df in GBgetTransitionsAll (model=0xac0bb0, src=0xad9a80, cb=0x4a3a25, context=0x7fffffffd5c0) at pins.c:885
11 0x00000000004a0a09 in dfs_state_next_all (state=0x7fffffffd5c0, arg=0x0) at pins2lts-seq.c:639
12 0x00000000004a39ef in gsea_foreach_open_cb (s_open=0x7fffffffd5c0, arg=0x0) at pins2lts-seq.c:1763
13 0x00000000004a395e in gsea_foreach_open (open_cb=0x4a397c, arg=0x0) at pins2lts-seq.c:1743
14 0x00000000004a390e in gsea_search (src=0x7fffffffd630) at pins2lts-seq.c:1731
15 0x00000000004a42f7 in main (argc=7, argv=0x7fffffffd798) at pins2lts-seq.c:1870
(gdb) f 1
1 0x00000000004fe5f9 in por_seen (dst=0xad9b48, group=0, src_changed=false) at pins2pins-por.c:210
210 return loc->find_state (dst, &ti, loc->find_state_ctx); (gdb) l 205 por_seen (int dst, int group, bool src_changed) 206 { 207 transition_info_t ti = GB_TI (NULL, src_changed ? -1 : group); 208 local_t loc = get_local (); 209 HREassert (loc, "POR seen not activated (call por_set_find_state)"); 210 return loc->find_state (dst, &ti, loc->find_state_ctx); 211 } 212 213 static void 214 seen_cb (void context, transition_info_t ti, int dst, int cpy) (gdb) p loc $1 = (local_t ) 0xad9b70 (gdb) p dst $2 = (int ) 0xad9b48 (gdb) p dest No symbol "dest" in current context. (gdb) p dst $3 = 1 (gdb) p group $4 = 0 (gdb) p src_changed $5 = false (gdb) p ti $6 = {labels = 0x0, group = 0, por_proviso = 0} (gdb) p *loc $7 = {find_state = 0x7ffff6e0db98 <main_arena+88>, find_state_ctx = 0x7ffff6e0db98 <main_arena+88>}