Linux Driver Verification

During fixing of #347 issue and making correct instrumentation for extern functions I found that some models have incorrect aspects. For example, 08_1 (comes from local testing) and 37_1 (comes from small regression test). The 37_1 model contains:

before: call(unsigned long probe_irq_on(void))
{
ldv_probe_irq_on()
}

what leads after instrumentation to:

long unsigned int ldv_probe_irq_on_1 (void)
{
  typedef long unsigned int ldv_func_ret_type;
  typedef void ldv_func_arg_type1;

ldv_probe_irq_on()

  return probe_irq_on();
}

But we must write correct C code inside advice bodies!