Linux Driver Verification

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?