Bug #1313
openInfinite sequence models are flawed
0%
Description
I was analyzing a driver from 'linux-2.6.39' with '32_7', Module = 'drivers/usb/class/cdc-wdm.k'. LDV shows a false positive. The sequence of functions called from main is (excerpt):
1707 - wdm_pre_reset(var_group4 /* intf */);
1349 - res_wdm_open_10 = wdm_open(var_group2 /* inode */, var_group1 /* file */);
1350 ldv_check_return_value(res_wdm_open_10) { /* The function body is undefined. */ };
1351 assert(res_wdm_open_10 != 0);
1827 + wdm_exit();
1830 + ldv_check_final_state_FOREACH();
pre_reset and post_reset handlers are invoked in a sound, but not in a complete manner! This scenario shows that between pre- and post- reset handlers there could be a call to open, which would make the module terminate. Does it happen like this?
Updated by Pavel Shved almost 13 years ago
If you're lucky, you may observe this error on my machine.
Updated by Vadim Mutilin almost 13 years ago
That is true.
The post_reset should always be called after pre_reset, but now DEG does not enfore it to be called.
Current way of specifying sequence conditions does not allow to do it, because stateful sequence model only enforces successful calls. In the example we have two structures and the calls are mixed, currently there is no way to define sequence conditions on several structures at all. For each single function we define preconditions which say that something should not be called, and do not say that something should be called.
Updated by Vadim Mutilin almost 13 years ago
Module
linux-2.6.31.6 32_1 drivers/xen/xenfs/xenfs.ko ldv_main1_sequence_infinite_withcheck_stateful