Project

General

Profile

Actions

Bug #1313

open

Infinite sequence models are flawed

Added by Pavel Shved over 13 years ago. Updated about 12 years ago.

Status:
New
Priority:
Normal
Assignee:
Category:
Environment Generation
Start date:
06/02/2011
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

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?


Related issues 1 (1 open0 closed)

Related to Linux Driver Verification - Bug #3351: Handling error cases of callbacks in envgen for more than two structuresOpenVadim Mutilin08/21/2012

Actions
Actions #1

Updated by Pavel Shved over 13 years ago

If you're lucky, you may observe this error on my machine.

Actions #2

Updated by Vadim Mutilin over 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.

Actions #3

Updated by Vadim Mutilin over 13 years ago

Module

linux-2.6.31.6    32_1    drivers/xen/xenfs/xenfs.ko    ldv_main1_sequence_infinite_withcheck_stateful

Actions

Also available in: Atom PDF