Linux Driver Verification

Examples (ldv-git on Kernel-59365d136d205cc20fe666ca7f89b1c5001b0d5a)

1. bttv-vbi.ko ldv_main0_plain_sorted_withcheck blast
   

   lock without unlock at the end
   actions of spin_unlock is out of the depth
   ldv_spin_unlock_irqrestore_1(blast_must_tmp__11639, blast_must_tmp__11640) { /* The function body is undefined. */ };
   

1. cm.ko ldv_main0_plain_sorted_withcheck blast
   

   depth
   

1. cs5535-mfgpt.ko ldv_main0_plain_sorted_withcheck blast
   

   depth
   

My idea is that we should ignore fdepth option for model functions at all.

For now, we can consider a function is model if it starts from ldv_.

...and does the __blast_assert start with ldv_? ;-)

Yes, enforcing depth inside the model functions is nonsense. We should fix it asap.

Would an option -ignore-depth-for ldv_, with an additional fix to ignore depth for BLAST's internal pseudo-functions, suffice?

Pavel Shved wrote:

Would an option -ignore-depth-for ldv_, with an additional fix to ignore depth for BLAST's internal pseudo-functions, suffice?

Yes, that would be great.

Why is it not closed? Because of blast_assert that doesn't begin with _ldv is ignored?