Klever

At the moment I got the following exception:

2017-08-16 11:27:41 (components.py:123) RSB ERROR> Raise exception:
Traceback (most recent call last):
  File "/home/debian/klever/core/core/components.py", line 116, in run
    self.main()
  File "/home/debian/klever/core/core/utils.py", line 56, in callbacks_caller
    ret = attr(*args, **kwargs)
  File "/home/debian/klever/core/core/vtg/rsb.py", line 61, in generate_verification_tasks
    self.decide_verification_task()
  File "/home/debian/klever/core/core/utils.py", line 56, in callbacks_caller
    ret = attr(*args, **kwargs)
  File "/home/debian/klever/core/core/vtg/rsb.py", line 379, in decide_verification_task
    self.create_verification_report(verification_report_id, decision_results)
  File "/home/debian/klever/core/core/utils.py", line 56, in callbacks_caller
    ret = attr(*args, **kwargs)
  File "/home/debian/klever/core/core/vtg/rsb.py", line 420, in create_verification_report
    self.conf['VTG strategy']['collect coverage'])
  File "/home/debian/klever/core/core/vtg/coverage_parser.py", line 26, in __init__
    self.parse()
  File "/home/debian/klever/core/core/vtg/coverage_parser.py", line 70, in parse
    with open(self.coverage_file, encoding='utf-8') as fp:
FileNotFoundError: [Errno 2] No such file or directory: 'output/coverage.info'

when, say, verifier failed:

Error: org.sosy_lab.cpachecker.cpa.bam.BAMCPA is not a valid CPA: wrapped CPA does not support BAM: org.sosy_lab.cpachecker.cpa.predicate.PredicateCPA (CPABuilder.buildCPAs, SEVERE)

The reason is that coverage is expected unconditionally on BenchExec statuses.

Indeed the best solution is likely to add some more information to BenchExec statuses to notify whether coverage was successfully printed or not. For instance, a verifier can print coverage but then a timeout happens - in this case we still can visualize coverage although a final verdict is unknown. But most likely you will understand that coverage wasn't successfully printed by catching exception when parsing a coverage file.

The issue isn't very-very important since there will be unknowns anyway.