Refactor witness output interpretation

[marian-lingsch]

In order to make it easier to understand the output of the witness linter we sepparate the exception case from the case where there was no output

[PhilippWendler]

Does "witnesslint finished" not in run.output[-1] really imply an EXCEPTION result?

[marian-lingsch]

If witnesslint exited successfully, the last line will always contain "witnesslint finished".
If this line is not present something went wrong internally, which is usually due to some exception, therefore we return EXCEPTION in this case.
The same could be reasoned for an empty output. Is it preferable to return EXCEPTION (no output) in this case or Error (no output) in this case?

[PhilippWendler]

It is a decision of the tool maintainer what to do here, but I personally would find the "usually" too weak here. Nothing worse during debugging than some output that leads you in the wrong direction. In CPAchecker's tool-info module, for example, we return EXCEPTION if there is some specific output that indicates that there was an exception. So if I was responsible for the linter's tool-info module, I would return ERROR (no output) as it is suggested, maybe EXCEPTION for exit code 7 (if this is what the tool produces), potentially EXCEPTION if there is something that looks like an exception in the output, and as a fallback ERROR if none of these and the other existing cases match.

Btw.: I just noticed the UNKNOWN return value. UNKNOWN is for cases where the tool voluntarily gives up and does not attempt to provide an answer (like an incomplete verifier). It is not for cases where the tool-info module fails to find out a proper return value. In the code here it looks like the latter case, so I guess it should be changed to return ERROR.

[marian-lingsch]

Thank you very much for your comments. I tried to address both concerns with the last two commits by returning an Error per default and splitting the error that witnesslint did not finish from the case where we know there has been an exception.
Feedback is always very welcome!