Klever

The archive actually contains Unknown tasks

Moreover now it does not saves benchmark xml

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.

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)

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" 

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.

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.