Command lines for witness validation are outdated
PhilippWendler opened this issue · 6 comments
With a current Ultimate version, the command line given in the documentation in this repository does not work anymore. The usage of Ultimate is now as follows:
usage: Ultimate.py [-h] [--version] [--config <dir>] [--data <dir>]
[--full-output] [--validate <file>] --spec <file>
--architecture {32bit,64bit} --file <file>
[--witness-dir <dir>] [--witness-name WITNESS_NAME]
As long as old and new versions of Ultimate are relevant, the documentation should probably give examples for both and explain how to choose between them.
For CPAchecker, the documentation says to use -spec witness-to-validate.graphml, but I thought this is deprecated in favor of -witness? (Although it still seems to work.)
We have issue #135 for that over at Ultimate, but we will only explain the latest version of Ultimate in our docs. I will update the instructions here as soon as I get around to fixing our issue.
We have issue #135 for that over at Ultimate, but we will only explain the latest version of Ultimate in our docs. I will update the instructions here as soon as I get around to fixing our issue.
@danieldietsch Could you please double check whether this was done and then let's close the issue.
Its on the list ;)
If CPAchecker is current we can finally close this issue.
@MartinSpiessl Could you check the command line for CPAchecker, please?
Yeah, this section seems to be quite outdated. I also don't think this repo is the right place for describing how to do a (violation) witness validation with an arbitrary analysis in CPAchecker. We should just provide means of how to call the -witnessValidation config. The more detailed description I would rather move to https://sosy-lab.gitlab.io/research/tutorials/CPAchecker/Witnesses.html, I created an issue in the repo from which that page is generated such that that information is not lost. I also prepared a pull request #50 that simplifies the instructions for CPAchecker, such that we can close this issue in a timely manner.
Apart from that I tried to run CPAcheckers validation on the example program+witness in this repo and the validation if this (violation) witness is actually not successful. I tried to run it with an older CPAchecker version (1.7-svn 29852-unix from SV-COMP 2019) and even with that one I was not able to validate the witness. Unfortunately we also did not document against which tool version this README was executed when written.
This is related to issue #41. I think it would be best to rather generate the example witness anew with CPAchecker and then note the actual version against which the commands were executed/tested. Actually if we generate the witness again the we have the producer field which gives a good clue about which tool version was used (at least for generating the witness). But of course documenting which tool versions we used to check the witness should also be documented somewhere.
The current command lines refer to some test.c, which is not in the repo. But of course anyone who reads this README and is new to the matter will try it with the example files in the repo first. So it might be worthwhile to change/extend the instructions to refer to these example files in some way.