sosy-lab/sv-benchmarks

MemSafety - unset subproperty for false verdict

versokova opened this issue · 0 comments

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