Project

General

Profile

Bug #8967

Download files for competition does not allow to choose Unknowns

Added by Vadim Mutilin 9 months ago. Updated 6 months ago.

Status:
Closed
Priority:
Urgent
Category:
Bridge
Target version:
Start date:
06/19/2018
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Linux x64
Published in build:

Description

See picture.
The Job has 9 Unknowns, but I can not choose them.
I can download only Unsafes/Safes using "Download files for competition".

klever_unknowns.png (52 KB) klever_unknowns.png Vadim Mutilin, 06/19/2018 11:11 AM
klever_duplicates.png (155 KB) klever_duplicates.png Vadim Mutilin, 06/19/2018 11:24 AM
svcomp(1).zip (3.24 MB) svcomp(1).zip generated by Klever v1.1 Anton Vasilyev, 10/04/2018 07:27 PM

Related issues

Blocked by Klever - Feature #9035: Change the way to identify sub-jobsClosed2018-06-28

History

#1 Updated by Vadim Mutilin 9 months ago

Screenshot

#2 Updated by Vadim Mutilin 9 months ago

The archive actually contains Unknown tasks

#3 Updated by Vadim Mutilin 9 months ago

Unfortunately the archive contains duplicated files. It looks like the name for tasks before commit and after commit coincide. See screenshot

#4 Updated by Vadim Mutilin 9 months ago

Moreover now it does not saves benchmark xml

#5 Updated by Evgeny Novikov 9 months ago

  • Target version changed from 1.0 to 2.0
  • Priority changed from High to Urgent

Now it is too late to fix this dinosaur. I suggest to fix it together with #9035 since it will improve sub-jobs identification (verification tasks identification is a part of it).

#6 Updated by Evgeny Novikov 9 months ago

  • Blocked by Feature #9035: Change the way to identify sub-jobs added

#7 Updated by Evgeny Novikov 9 months ago

  • Target version changed from 2.0 to 1.1

This issue is not strictly bound with purposes of 2.0 that targets verification of C software.

#8 Updated by Evgeny Novikov 8 months ago

  • Target version changed from 1.1 to 2.0

Let's Vladimir will do this after his vacation.

#9 Updated by Vladimir Gratinskiy 6 months ago

  • Status changed from New to Feedback

Please check again if it works in current master. It might be already fixed.

#10 Updated by Vladimir Gratinskiy 6 months ago

  • Status changed from Feedback to Resolved

I've checked and it works already.

#11 Updated by Evgeny Novikov 6 months ago

  • Status changed from Resolved to Open

Vadim Mutilin wrote:

Moreover now it does not saves benchmark xml

This doesn't work still. I suggest to download an archive with archives with input files of static verifiers, but name these archives as you name CIL files now.

Also there is strange file NOFILES in an archive.

#12 Updated by Vladimir Gratinskiy 6 months ago

Evgeny Novikov wrote:

Vadim Mutilin wrote:

Moreover now it does not saves benchmark xml

This doesn't work still. I suggest to download an archive with archives with input files of static verifiers, but name these archives as you name CIL files now.

Did you try to download unknowns' files for job which has it?

Also there is strange file NOFILES in an archive.

An archive must have at least one file. As I can't check at the start of archive generation if there are any files for specified filters (safes/unsafes/unknowns/unknowns with specific problem), I add empty file NOFILES at the end if there are no files. Without verifier input archives unpacking I can check if there are files for archive and return an error if not.

#13 Updated by Evgeny Novikov 6 months ago

Vladimir Gratinskiy wrote:

Evgeny Novikov wrote:

Vadim Mutilin wrote:

Moreover now it does not saves benchmark xml

This doesn't work still. I suggest to download an archive with archives with input files of static verifiers, but name these archives as you name CIL files now.

Did you try to download unknowns' files for job which has it?

Yes, this works. But there are just CIL source files. My suggestion is to avoid any parsing of archives with verifier input files in Bridge, but pack them into subdirectories Safes/Unsafes/Unknowns within file svcomp.zip.

Also there is strange file NOFILES in an archive.

An archive must have at least one file. As I can't check at the start of archive generation if there are any files for specified filters (safes/unsafes/unknowns/unknowns with specific problem), I add empty file NOFILES at the end if there are no files. Without verifier input archives unpacking I can check if there are files for archive and return an error if not.

There may be no files in ZIP archives:

>>> from zipfile import ZipFile
>>> with ZipFile('spam.zip', 'w') as myzip:
...   pass
... 
>>> 
>>> exit()

$ file spam.zip
spam.zip: Zip archive data (empty)

#14 Updated by Evgeny Novikov 6 months ago

BTW, there is such the exception:

Traceback (most recent call last):
  File "/home/novikov/work/klever/bridge/reports/utils.py", line 854, in __reports_data
    for data in self.__cil_data(reports[r_id], r_path):
  File "/home/novikov/work/klever/bridge/reports/utils.py", line 874, in __cil_data
    for data in self.stream.compress_string(self.prp_fname, zfp.read(self.prp_fname)):
  File "/usr/lib64/python3.6/zipfile.py", line 1314, in read
    with self.open(name, "r", pwd) as fp:
  File "/usr/lib64/python3.6/zipfile.py", line 1352, in open
    zinfo = self.getinfo(name)
  File "/usr/lib64/python3.6/zipfile.py", line 1281, in getinfo
    'There is no item named %r in the archive' % name)
KeyError: "There is no item named 'unreach-call.prp' in the archive" 
"There is no item named 'unreach-call.prp' in the archive" 

#15 Updated by Vladimir Gratinskiy 6 months ago

  • Status changed from Open to Feedback

Evgeny Novikov wrote:

My suggestion is to avoid any parsing of archives with verifier input files in Bridge, but pack them into subdirectories Safes/Unsafes/Unknowns within file svcomp.zip.

If people who need this feature agree with suggestion, I'll start fixing.

#16 Updated by Vadim Mutilin 6 months ago

I think it is a good suggestion, because it will allow to support verifications tasks which differ from standard ones like having several CIL files in one task.
It is OK to have original "archives with verifier input files in Bridge", but please rename them in the same way as it was previously for the CIL files (with modules, rules etc) to tell one archive from another.

#17 Updated by Evgeny Novikov 6 months ago

  • Status changed from Feedback to Open

#18 Updated by Vladimir Gratinskiy 6 months ago

  • Status changed from Open to Resolved

Fixed in bridge-2.0.

#19 Updated by Evgeny Novikov 6 months ago

  • Status changed from Resolved to Closed

Tests passed, so, I merged the branch to master in b8bda00ac.

#20 Updated by Anton Vasilyev 6 months ago

Please check that file names at archive aren't duplicated when job contains different revisions like in Validation preset.

#21 Updated by Evgeny Novikov 6 months ago

Anton Vasilyev wrote:

Please check that file names at archive aren't duplicated when job contains different revisions like in Validation preset.

Bridge knows nothing about different "revisions", "versions", "configurations", etc. Moreover, anyway filenames can match ones obtained some time ago. So, resolve these issues outside Klever using means appropriate for you.

Moreover, it's strange that you used Klever 1.1 for generating an archive as you need to use master where several issues were fixed.

Also available in: Atom PDF