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

MemSafety - unset subproperty for false verdict #1285

Open versokova opened 3 years ago

versokova commented 3 years ago

There are many new benchmarks in the MemSafety category, where the subproperty for unsafe versions is not defined. For example (maybe more): c/openbsd-6.2/*.yml c/Juliet_Test/*bad.yml

There are a few tasks that may contain more than 1 error (according to the CPAchacker). Need further investigation.

CWE415_Double_Free---s01---CWE415_Double_Free__*bad.yml false(valid-memtrack), according to the filename should be false(valid-free)

CWE590_Free_Memory_Not_on_Heap---s04---CWE590_Free_Memory_Not_on_Heap__*bad.yml false(valid-deref) or false(valid-memtrack), according to the filename should be false(valid-free)

CWE401_Memory_Leak---s01---CWE401_Memory_Leak*bad.yml false(valid-free), according to the filename should be false(valid-memtrack)

And this CWE415_Double_Free---s01---CWE415_Double_Free__malloc_free_*bad.yml for sure (CBMC and CPAchecker). See valid-memsafety.MemSafety-Juliet.table.html))))