Juliet memsafety tasks do not specify violated subproperty, and might violate more than one subproperty
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