Let WitnessLint output the type of the witness

[dbeyer]

I would like to request the following feature:

The witness linter should show the type of the witness in the status.

This requires changes in the witness linter (log the content of the key witness-type in GramphML to stdout)
and in the tool-info module (instead of return result.RESULT_DONE change to return result.RESULT_DONE + f" ({witness_type})" where witness_type` is matched from the log output.

Optional (but this is neither urgent nor currently necessary):
The log output of WitnessLint could also include some more information that might be interesing for the users,
for example:

    "architecture": "32bit",
    "creationtime": "2021-12-06T14:44:55+01:00",
    "inputwitnesshash": "b74b9a4b98de1e383e38d91e28c3cfeed8d8428c9b166772b4a6f5288a75207f",
    "producer": "CPAchecker 2.1 / witnessValidation",
    "program-sha256": "77d80771821c1cd45088b62d9d16474928a377618be5caefce4c7c3ebfdda084",
    "programfile": "../../sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.2.ufo.BOUNDED-10.pals.c",
    "programhash": "77d80771821c1cd45088b62d9d16474928a377618be5caefce4c7c3ebfdda084",
    "sourcecodelang": "C",
    "specification": "CHECK( init(main()), LTL(G ! call(reach_error())) )",
    "witness-file": "fileByHash/0a526b3e99025c41428566c92586c3c0c4c2e3dfc875bf9fa96cfc2bcfa29995.graphml",
    "witness-sha256": "0a526b3e99025c41428566c92586c3c0c4c2e3dfc875bf9fa96cfc2bcfa29995",
    "witness-size": 213910,
    "witness-type": "violation_witness"

[PhilippWendler]

From BenchExec's point of view a result like DONE(foo) would currently be counted as error result (and printed in pink instead of blue). That is not problematic per se and it could even be changed, but maybe it is better to not overload the status column with this anyway?

How about extending the tool-info module such that it becomes possible to extract the witness type into a separate column? (Like we do it with CPAchecker statistics, for example?)

[PhilippWendler]

The tool-info module could even provide the possibility to extract other metadata from the witness, even a generic feature such that you can ask for any key that is present at top level in the witness would be easy to implement, I guess (if the linter outputs this information - but we could add a --verbose flag to do so, for example).

[dbeyer]

First part implemented in #56.

[SvenUmbricht]

Closing this since there doesn't seem to be anything left to do. The requested summary is printed since #56 was merged, and while the original request of adding the witness type to the status column has not been realized, the proposal from #55 (comment) was implemented in sosy-lab/benchexec#803 and in particular allows the extraction of the witness type into its own column.