Bug #8967
closedDownload files for competition does not allow to choose Unknowns
Added by Vadim Mutilin almost 6 years ago. Updated over 5 years ago.
0%
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".
Files
| 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 |
Updated by Vadim Mutilin almost 6 years ago
- File klever_unknowns.png klever_unknowns.png added
Screenshot
Updated by Vadim Mutilin almost 6 years ago
The archive actually contains Unknown tasks
Updated by Vadim Mutilin almost 6 years ago
- File klever_duplicates.png klever_duplicates.png added
Unfortunately the archive contains duplicated files. It looks like the name for tasks before commit and after commit coincide. See screenshot
Updated by Vadim Mutilin almost 6 years ago
Moreover now it does not saves benchmark xml
Updated by Evgeny Novikov almost 6 years ago
- Priority changed from High to Urgent
- Target version changed from 1.0 to 2.0
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).
Updated by Evgeny Novikov almost 6 years ago
- Blocked by Feature #9035: Change the way to identify sub-jobs added
Updated by Evgeny Novikov almost 6 years 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.
Updated by Evgeny Novikov almost 6 years ago
- Target version changed from 1.1 to 2.0
Let's Vladimir will do this after his vacation.
Updated by Vladimir Gratinskiy over 5 years ago
- Status changed from New to Feedback
Please check again if it works in current master. It might be already fixed.
Updated by Vladimir Gratinskiy over 5 years ago
- Status changed from Feedback to Resolved
I've checked and it works already.
Updated by Evgeny Novikov over 5 years 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.
Updated by Vladimir Gratinskiy over 5 years 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.
Updated by Evgeny Novikov over 5 years 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)
Updated by Evgeny Novikov over 5 years 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"
Updated by Vladimir Gratinskiy over 5 years 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.
Updated by Vadim Mutilin over 5 years 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.
Updated by Evgeny Novikov over 5 years ago
- Status changed from Feedback to Open
Updated by Vladimir Gratinskiy over 5 years ago
- Status changed from Open to Resolved
Fixed in bridge-2.0.
Updated by Evgeny Novikov over 5 years ago
- Status changed from Resolved to Closed
Tests passed, so, I merged the branch to master in b8bda00ac.
Updated by Anton Vasilyev over 5 years ago
- File svcomp(1).zip svcomp(1).zip added
Please check that file names at archive aren't duplicated when job contains different revisions like in Validation preset.
Updated by Evgeny Novikov over 5 years 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.