Direct visualization of witnesses

[PavelAndrianov]

It is a bit separate issue from previous ones. As a origin Klever is not in favor to support direct visualization of witnesses, we may think if it is possible to implement this feature firstly in our lightweight version. The benefit is related only to sv-comp community. We have already an option to upload an archive and a corresponding functionality, which prepares the archive. Is it possible to extract it and simplify for the particular task? An ideal case is, when a klever itself is not required, someone may just get a simple conversion script and test the visualization on our test server. I did not set a project, as the issue is not related to cv verification.

[vmordan]

As I understand, there are 2 sub-tasks here:

1. Allow to save html representation of error trace from Klever, so it can be shown somewhere separately.
2. Allow to transform witness to such html representation, so it can be used outside of Klever (i.e. verifier produces witness and this new function makes it human-readable without Klever).

[PavelAndrianov]

I did not think in a such direction, but it is a good idea. My idea is to provide some stand-alone script, which can prepare an upload archive without the whole Klever. But this archive should be uploaded to some external Klever station. However, your idea is much helpful for CV-Klever project, as if it implemented, we may add an html-trace without link to Klever-machine, which may be unavailable.

So, we may think in both directions. Seems, to prepare a script is a bit simpler (but I am not sure), and html representation may be useful not only for sv-comp community.

[vmordan]

First subtask is implemented in commit 78ba48c3

[vmordan]

Second subtask is implemented in commit b355e50