sosy-lab / sv-benchmarks

Collection of Verification Tasks (MOVED, please follow the link)
https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
184 stars 169 forks source link

Files with known overflows outside of Bitvector category #276

Open PhilippWendler opened 7 years ago

PhilippWendler commented 7 years ago

This year several tasks with unsigned overflows have been added to some categories, e.g., in #234.

In previous years, such tasks have been moved to the BitVectorsReach category and other categories have been kept mostly free of overflows.

Should this be done here as well? Otherwise, what is the reason for having a specific BitVectors category?

If we want to move the files, how do we organize them in the repository? Moving files between directories as has been done in the past is not good, because then the connection between readme, license, and source file is lost.

zvonimir commented 7 years ago

I support moving such benchmarks into the BitVectorsReach category, as you suggested. I could be wrong, but I think you could leave those files in their original folders, but just update set files.

dbeyer commented 7 years ago

Yes, not moving, but keeping the files close to their original and README and LICENSE.

Those files were added to a new .set file: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/Overflows-Other.set

dbeyer commented 7 years ago

@PhilippWendler, just to make sure I correctly understood: You mean signed overflow, right? ("This year several tasks with unsigned overflows")

PhilippWendler commented 7 years ago

No, I meant unsigned overflows.

dbeyer commented 7 years ago

@PhilippWendler: Please propose action item.

PhilippWendler commented 7 years ago

Adding these files to another category is easy, but to remove them from the current category without removing them from the current directory is not so easy. How about creating a subdirectory for such files?