Linux Driver Verification

As well as for #1633 issue we need to integrate KB scripts with error trace parser and may be write some special routines allowing simple tree traversing. The latter will allow to implement all criterion and a lot of other KB library functions in the more efficient way.

After implementation of blockers this issue becomes trivial. It's committed to b625fa5 of knowledge-base-2 branch.
From today when you'll click Create filled KB record you'll obtain a new KB record with a filled Script field:

return 1 if (call_stacks_ne($et, $kb_et));

At the Demo 18, a couple of serious issues was identified in this feature:

• call_stack should be removed to something like call_tree;
• a bug with initialization function (which always has a file-specific name) should be fixed, i.e. this function should not be considered for matching of calls.

Pavel Shved wrote:

At the Demo 18, a couple of serious issues was identified in this feature:

• call_stack should be removed to something like call_tree;
• a bug with initialization function (which always has a file-specific name) should be fixed, i.e. this function should not be considered for matching of calls.

Both issues are fixed in commit bfd7942 of master branch and will be available after QA testing. If all will be ok, I'll deploy fixes on QA reference launches and for CPAchecker DB.

BTW!!! If you have some local knowledge bases (I guess that you haven't any), please update them manually to be up-to-date:

mysql ldv_db_3 -e "update kb set script=replace(script, 'call_stacks_ne', 'call_trees_ne');" 

Fixes are deployed and show that all works. For instance, see that was automatically marked as 'False unsafe' on the basis of previously added KB records.
Note, that KB verdicts changed considerably after these fixes application. See attachments that show this. Also CPAchecker traces are matched with BLAST ones now. For instance, this leaded to KB records application to CPAchecker error traces.

Works well for me.