Bug #8362

Do not expect coverage when verifiers fail

Added by Evgeny Novikov 3 months ago. Updated about 1 month ago.

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

0%

Category:Results processingSpent 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 Closed 08/15/2017

History

#1 Updated by Evgeny Novikov 3 months ago

  • Target version set to 0.2

#2 Updated by Alexey Polushkin 2 months ago

I've implemented in branch 'failed_coverage'

#3 Updated by Evgeny Novikov 2 months ago

  • Status changed from New to Resolved

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

#4 Updated by Ilja Zakharov 2 months ago

  • Status changed from Resolved to Open

Need to update this according to the Klever version after refactoring.

#5 Updated by Evgeny Novikov 2 months ago

Please, rebase it on top of the latest master.

#6 Updated by Evgeny Novikov 2 months ago

  • Category changed from Tasks generation to Results processing

#7 Updated by Alexey Polushkin 2 months ago

The branch has been updated

#8 Updated by Evgeny Novikov about 1 month ago

Your fix doesn't look to fix everything related with this issue. I suppose to move all coverage related checks from core.vrp.RP#_process_finished_task_ to core.vrp.coverage_parser.LCOV and add information on coverage to verification reports just if your coverage parser succeeds.

#9 Updated by Alexey Polushkin about 1 month ago

  • Status changed from Open to Resolved

Resolved in 'new_report_archives' branch.

#10 Updated by Evgeny Novikov about 1 month ago

  • Status changed from Resolved to Closed

I merged the branch that has this bug fix (multicoverage) to master in commit:37f0c082.

Also available in: Atom PDF