Linux Driver Verification

It should help to fix this false positive:
ldv-git(-fdepth 7):68_1:drivers/mtd/nand/alauda.ko:linux-2.6.39-rc7
where usb_free_urb() is cut off by -fdepth logic that works incorrectly without ldv_ prefix.

How will it work with recursive functions containing the label?

Recursive calls are ignored in BLAST regardless of call stack depth constraints.

Or, do I miss something?

Your example does not finish on my machine due to insufficient resources. Do you have more of these?

Meanwhile, I realized that it's not the best solution possible. The thing is that we want to actually "mark" certain functions as "important", and this marking includes but is not limited by error labels.

Using labels for marking is not the best option. The thing is that we should insert a goto to a function body for the label to be spotted by backends of various C transforming tools. We could mark it with an impossible if operator, like this:

void ldv_spin_lock(void)
{
  if (0) LABEL: goto LABEL;
  /* actual code */
}

However, this if operator will be seen in the error trace.
We could place the goto after the return statement, so that it will definitely be not shown in the trace. However, BLAST asks CIL to remove such unreachable code (and, I suppose, other C transformation tools, such as Aspectator, may discard such gotos as well), and can't find the label entirely.

A more natural way to "mark" functions is to use GCC function attributes. They are non-portable, however, but our toolchain, and the primary domain, linux device drivers, supports and uses them.

So, tomorrow, I'll retool my fixes to function attributes. Embedding them into models will be straightforward.

Hm. When I got to aspectator-powered models, it stopped working, because Aspectator does not preserve these attributes, and the files generated do contain neither ldv_model nor ldv_model_inline. I guess, C backend just can't print attributes unrecognized by GCC, which the attributes I added are.

So, if we want to use the attributes, we should teach our GCC to preserve them as if they're its native ones. Not that hard, I guess... but are there any other solutions?

Yes... Unfortunately at the moment C backend doesn't touch GCC attributes at all. And I also guess that their support can be added rather simply (especially in case of some specific kind of attributes, like for functions).