Bug #8362

Do not expect coverage when verifiers fail

Added by Evgeny Novikov about 1 month ago. Updated 7 days ago.

Status:ResolvedStart date:08/16/2017
Priority:UrgentDue date:
Assignee:Alexey Polushkin% Done:

0%

Category:Tasks generationSpent time:-
Target version:0.2
Detected in build:svn Published in build:
Platform:

Description

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.


Related issues

Blocks Klever - Feature #8353: Calculate total code coverage New 08/15/2017

History

#1 Updated by Evgeny Novikov 25 days ago

  • Target version set to 0.2

#2 Updated by Alexey Polushkin 8 days ago

I've implemented in branch 'failed_coverage'

#3 Updated by Evgeny Novikov 7 days ago

  • Status changed from New to Resolved

Ilja would like to examine code and the fix itself before merging to master.

Also available in: Atom PDF