why3replay fails when used on an .mlw file
why3 replay works on session directories but fails when given an .mlw file:
====== tikki:~/prj/why3 (master)> bin/why3 replay --merging-only examples/maximum_subarray.mlw Usage: why3 replay [options] ...
This happens because Server_util.get_session_dir returns the source file into the file queue (server_utils.ml:40), and why3replay fails if the queue is not empty after the get_session_dir call (why3replay.ml:383).
I would suggest to split get_session_dir into two functions: one to take a single file name (session directory or session .xml file or source file) and return a directory name (without mkdir). This function should be named "get_session_dir" and used in why3replay. The other function would implement the queue management logic and use the first one to retrieve the directory names.
That said, I do not quite understand the logic of the current get_session_dir.
- Why it only accepts a source file name when it is the only name in the queue (server_utils.ml:33) — why aren't source files handled the same way as session directories or why3session.xml files?
- Why does it return the source file name into the queue?