Skip to content
This repository has been archived by the owner on Oct 3, 2021. It is now read-only.

MemSafety - unset subproperty for false verdict #1285

Open
versokova opened this issue Dec 20, 2020 · 0 comments
Open

MemSafety - unset subproperty for false verdict #1285

versokova opened this issue Dec 20, 2020 · 0 comments
Labels
C Task in language C issue with benchmark

Comments

@versokova
Copy link
Contributor

versokova commented Dec 20, 2020

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

@versokova versokova added C Task in language C issue with benchmark labels Dec 20, 2020
mchalupa added a commit to staticafi/sv-benchmarks that referenced this issue Dec 20, 2020
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
C Task in language C issue with benchmark
Development

No branches or pull requests

1 participant