search

utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
52 stars 30 forks source link

solving --help crash for pins2lts-mc #144

Closed yanntm closed 6 years ago

yanntm commented 6 years ago

see comment on issue : https://github.com/utwente-fmt/ltsmin/issues/120

sorry to reopen, but it's not solved really

looking at the code, I believe the issue is that the help print is not protected against main proc only printing :

this is correct : https://github.com/utwente-fmt/ltsmin/blob/next/src/pins-lib/pins.c#L1220

this seems unprotected (though similar in nature) : https://github.com/utwente-fmt/ltsmin/blob/next/src/hre/hre_popt.c#L83

(same thing for printUsage just below, same function)

this behavior is still buggy, see test runs here : https://travis-ci.org/yanntm/DockerMemoryTest

Relevant part of trace 

$ lts_install_dir/bin/pins2lts-mc --help

Usage: pins2lts-mc [OPTIONS] <model> [lts]

Perform model checking on <model>

Options

      --strategy=<bfs|sbfs|dfs|cndfs|lndfs|endfs|endfs|renault|ufscc|ndfs>     select the search strategy (default: auto)

*** segmentation fault ***

Please send information on how to reproduce this problem to: 

         ltsmin-support@lists.utwente.nl

along with all output preceding this message.

In addition, include the following information:

Package: ltsmin 3.0.0

Stack trace:

pins2lts-mc: malloc.c:2374: sysmalloc: Assertion `(old_top == (((mbinptr) (((char *) &((av)->bins[((1) - 1) * 2])) - __builtin_offsetof (struct malloc_chunk, fd)))) && old_size == 0) || ((unsigned long) (old_size) >= (unsigned long)((((__builtin_offsetof (struct malloc_chunk, fd_nextsize))+((2 *(sizeof(size_t))) - 1)) & ~((2 *(sizeof(size_t))) - 1))) && ((old_top)->size & 0x1) && ((unsigned long) old_end & pagemask) == 0)' failed.

                                                                               /home/travis/.travis/job_stages: line 57:  7343 Aborted                 (core dumped) lts_install_dir/bin/pins2lts-mc --help

The command "lts_install_dir/bin/pins2lts-mc --help" exited with 134.
yanntm commented 6 years ago

note that endfs is present twice in that list of options 

      --strategy=<bfs|sbfs|dfs|cndfs|lndfs|endfs|endfs|renault|ufscc|ndfs>     select the search strategy (default: auto)
Meijuh commented 6 years ago

I improved it with @yanntm suggestions, so I am closing this for now.