Linux Driver Verification

By the analogy with #562 an another interesting and rather complex task is a comparison of unsafes coming from different techniques and models and with time. It seems that we may simplify a bit the given task. For example we may build some error trace "signature" and compare them aromatically (both traditional error trace analysis and manual examining of such "signatures" should also be presented). For my mind such a "signature" may be just a full function call stack like following:

entry_point;
{
 ldv_initialize;
 sm_lm78_init;
 {
  lm78_isa_found;
  {
   __request_region;
   printk;
  }
  i2c_add_driver;
  {
   i2c_register_driver;
  }
 }
 nondet_int;
 nondet_int;
 lm78_i2c_detect;
 {
  dev_get_drvdata;
  {
  }
  i2c_check_functionality;
  {
   i2c_get_functionality;
   {
    (mem_4 ); //Hmm...
   }
  }
  mutex_lock;
  {
  }
  i2c_smbus_read_byte_data;
  lm78_alias_detect;
  {
   dev_get_drvdata;
   {
   }
   lm78_read_value;
   {
    mutex_lock;
    {
     ldv_blast_assert;
     {
     }
    }
   }
  }
 }
}

More intellectual "signatures" may be developed. I think that this the task for error trace visualizer and then for stats server.