Currently Klever-based error traces (violation witnesses) parser supports only some versions of CPAchecker (with specific options) and fails hard (i.e., without providing any useful output) in other cases. For example, it requires "sourcecode" tag, which is not printed even in default CPAchecker configuration, and which can be obtained automatically with help of other data.
It is suggested to completely rewrite this parser, so it would satisfy the following requirements:
general format of SV-COMP violation witnesses should be supported (i.e., if this witness can be validated, it should be displayed);
in case of global errors (witness file cannot be parsed, some core elements are missing, etc.) detailed error message should be presented to the user (i.e., "line N: ERROR: details");
if some none-essential elements are missing, which are still vital for visualization, witness should be presented without them with a detailed warning message (for example, if there are only assumption edges, there should be a warning on missing function calls).
Currently Klever-based error traces (violation witnesses) parser supports only some versions of CPAchecker (with specific options) and fails hard (i.e., without providing any useful output) in other cases. For example, it requires "sourcecode" tag, which is not printed even in default CPAchecker configuration, and which can be obtained automatically with help of other data. It is suggested to completely rewrite this parser, so it would satisfy the following requirements: