Verdict for ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--mtd--sm_ftl.ko.cil.i
zvonimir opened this issue · 1 comments
zvonimir commented
I am having trouble figuring out what/where the bug is in this benchmark. I tried running it with various SMACK options, and it always fails to find a bug. The only verifier that reported false for it last year was CPAchecker, but if I am reading this right in the last year's table, the witness was not confirmed (I would guess that is what blue font color indicates in the table).
I wanted to take a look at the CPAchecker error witness, but it seems those are not available for download.
Does anyone know why this benchmark contains a bug?
Any insight you might have would be appreciated. Thanks!
zvonimir commented
Ok, I think I got it. It is related to malloc(0) discussion.