Past-the-end string parsing in extract_lexeme

[futile]

The first loop in extract_lexeme (link) will continue past the end of the given string if the last character before the terminating 0 is a backslash (e.g., ./jtc -w '[\\' Bookmarks).

This is because the presence of the backslash will cause the iterator to be increased twice, thus skipping the terminating null-byte.

This bug was found using Symbolic Execution techniques developed in the course of the SYMBIOSYS research project at COMSYS, RWTH Aachen University. This research is supported by the European Research Council (ERC) under the EU's Horizon 2020 Research and Innovation Programme grant agreement n. 647295 (SYMBIOSYS).

[ldn-softdev]

Hi Futile,
thank you for catching this one, indeed, overlooked issue, luckily the fix is trivial.

btw, is SYMBIOSYS publicly available?

[ldn-softdev]

I have posted the quick fixes for both issues, thanks again for reporting those!

[futile]

Thanks for the quick confirmation! We are using a version of the KLEE symbolic execution engine (https://klee.github.io) with our implementation for C++ support, which is available from the existing PR: klee/klee#966.

Thanks for the quick fixes! :)