Online Linux Driver Verification Service (alpha)

Rule violation
Driver: tests-model-08_1--test-doubleget.tar.bz2
Kernel: linux-2.6.32.12
Verification architecture: x86_64
Rule: Module get/put
Error trace
Function bodies
Blocks
  • Others...
    Entry point
    Entry point body
    Function calls
    Initialization function calls
    Function without body calls
    Function stack overflows
    Initialization function bodies
    Returns
    Return values
    Asserts
    Assert conditions
    Identation
    Driver environment initialization
    Driver environment function calls
    Driver environment function bodies
    Model asserts
    Model state changes
    Model returns
    Model function calls
    Model function bodies
    Model function function calls
    Model function function bodies
    Model others
    Function bodies without model function calls
Hide Entry point Hide Entry point body Hide Function calls Show Initialization function calls Hide Function without body calls Hide Function stack overflows Hide Function bodies Show Initialization function bodies Hide Blocks Hide Returns Hide Return values Hide Asserts Hide Assert conditions Hide Identation Show Driver environment initialization Hide Driver environment function calls Hide Driver environment function bodies Hide Model asserts Hide Model state changes Hide Model returns Hide Model function calls Show Model function bodies Hide Model function function calls Hide Model function function bodies Hide Model others Show Function bodies without model function calls
-entry_point();
{
128 -ldv_s_misc_fops_file_operations = 0;
LDV_IN_INTERRUPT = 1;
120 ldv_initialize() { /* The function body is undefined. */ };
126 +tmp = my_init();
126 assert(tmp == 0);
131 tmp___1 = nondet_int() { /* The function body is undefined. */ };
131 assert(tmp___1 != 0);
135 tmp___0 = nondet_int() { /* The function body is undefined. */ };
137 assert(tmp___0 == 0);
140 assert(ldv_s_misc_fops_file_operations == 0);
145 -res_misc_open_0 = misc_open(var_group1 /* inode */, var_group2 /* file */);
{
30 +tmp = ldv_try_module_get_1(&(&(mydev))->mod /* module */);
30 assert(tmp != 0);
31 +ldv_try_module_get_2(&(&(mydev))->mod /* module */);
32 +ldv_module_put_3(&(&(mydev))->mod /* ldv_func_arg1 */);
34 __retres4 = 0;
28 return __retres4;
}
146 ldv_check_return_value(res_misc_open_0) { /* The function body is undefined. */ };
147 assert(res_misc_open_0 == 0);
149 ldv_s_misc_fops_file_operations = 0;
131 tmp___1 = nondet_int() { /* The function body is undefined. */ };
131 assert(tmp___1 == 0);
131 assert(ldv_s_misc_fops_file_operations == 0);
168 +my_exit();
171 +ldv_check_final_state();
}
Source code
1 2 #include <linux/module.h> 3 extern int ldv_try_module_get(struct module*); 4 extern void ldv_module_get(struct module*); 5 extern void ldv_module_put(struct module*); 6 extern unsigned int ldv_module_refcount(void); 7 extern void ldv_module_put_and_exit(); 8 9 /** 10 */ 11 #include <linux/kernel.h> 12 #include <linux/module.h> 13 #include <linux/major.h> 14 #include <linux/fs.h> 15 16 struct my_device { 17 struct module mod; 18 } mydev; 19 20 static int misc_open(struct inode * inode, struct file * file); 21 22 static const struct file_operations misc_fops = { 23 .owner = THIS_MODULE, 24 .open = misc_open, 25 }; 26 27 28 static int misc_open(struct inode * inode, struct file * file) 29 { 30 if (try_module_get(&mydev.mod)) { 31 try_module_get(&mydev.mod); 32 module_put(&mydev.mod); 33 } 34 return 0; 35 } 36 37 static int __init my_init(void) 38 { 39 if (register_chrdev(MISC_MAJOR,"misc",&misc_fops)) 40 goto fail_register; 41 return 0; 42 43 fail_register: 44 return -1; 45 } 46 47 static void __exit my_exit(void) 48 { 49 } 50 51 module_init(my_init); 52 module_exit(my_exit); 53 54 MODULE_LICENSE("Apache 2.0"); 55 MODULE_AUTHOR("LDV Project, Vadim Mutilin <mutilin@ispras.ru>"); 56 57 58 59 60 61 62 /* LDV_COMMENT_BEGIN_MAIN */ 63 #ifdef LDV_MAIN0_sequence_infinite_withcheck_stateful 64 65 /*###########################################################################*/ 66 67 /*############## Driver Environment Generator 0.2 output ####################*/ 68 69 /*###########################################################################*/ 70 71 72 73 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Test if all kernel resources are correctly released by driver before driver will be unloaded. */ 74 void ldv_check_final_state(void); 75 76 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Test correct return result. */ 77 void ldv_check_return_value(int res); 78 79 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Initializes the model. */ 80 void ldv_initialize(void); 81 82 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Returns arbitrary interger value. */ 83 int nondet_int(void); 84 85 /* LDV_COMMENT_VAR_DECLARE_LDV Special variable for LDV verifier. */ 86 int LDV_IN_INTERRUPT; 87 88 /* LDV_COMMENT_FUNCTION_MAIN Main function for LDV verifier. */ 89 void ldv_main0_sequence_infinite_withcheck_stateful(void) { 90 91 92 93 /* LDV_COMMENT_BEGIN_VARIABLE_DECLARATION_PART */ 94 /*============================= VARIABLE DECLARATION PART =============================*/ 95 /** STRUCT: struct type: file_operations, struct name: misc_fops **/ 96 /* content: static int misc_open(struct inode * inode, struct file * file)*/ 97 /* LDV_COMMENT_END_PREP */ 98 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "misc_open" */ 99 struct inode * var_group1; 100 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "misc_open" */ 101 struct file * var_group2; 102 /* LDV_COMMENT_VAR_DECLARE Variable declaration for test return result from function call "misc_open" */ 103 static int res_misc_open_0; 104 105 106 107 108 /* LDV_COMMENT_END_VARIABLE_DECLARATION_PART */ 109 /* LDV_COMMENT_BEGIN_VARIABLE_INITIALIZING_PART */ 110 /*============================= VARIABLE INITIALIZING PART =============================*/ 111 LDV_IN_INTERRUPT=1; 112 113 114 115 116 /* LDV_COMMENT_END_VARIABLE_INITIALIZING_PART */ 117 /* LDV_COMMENT_BEGIN_FUNCTION_CALL_SECTION */ 118 /*============================= FUNCTION CALL SECTION =============================*/ 119 /* LDV_COMMENT_FUNCTION_CALL Initialize LDV model. */ 120 ldv_initialize(); 121 122 /** INIT: init_type: ST_MODULE_INIT **/ 123 /* content: static int __init my_init(void)*/ 124 /* LDV_COMMENT_END_PREP */ 125 /* LDV_COMMENT_FUNCTION_CALL Kernel calls driver init function after driver loading to kernel. This function declared as "MODULE_INIT(function name)". */ 126 if(my_init()) 127 goto ldv_final; 128 int ldv_s_misc_fops_file_operations = 0; 129 130 131 while( nondet_int() 132 || !(ldv_s_misc_fops_file_operations == 0) 133 ) { 134 135 switch(nondet_int()) { 136 137 case 0: { 138 139 /** STRUCT: struct type: file_operations, struct name: misc_fops **/ 140 if(ldv_s_misc_fops_file_operations==0) { 141 142 /* content: static int misc_open(struct inode * inode, struct file * file)*/ 143 /* LDV_COMMENT_END_PREP */ 144 /* LDV_COMMENT_FUNCTION_CALL Function from field "open" from driver structure with callbacks "misc_fops". Standart function test for correct return result. */ 145 res_misc_open_0 = misc_open( var_group1, var_group2); 146 ldv_check_return_value(res_misc_open_0); 147 if(res_misc_open_0) 148 goto ldv_module_exit; 149 ldv_s_misc_fops_file_operations=0; 150 151 } 152 153 } 154 155 break; 156 default: break; 157 158 } 159 160 } 161 162 ldv_module_exit: 163 164 /** INIT: init_type: ST_MODULE_EXIT **/ 165 /* content: static void __exit my_exit(void)*/ 166 /* LDV_COMMENT_END_PREP */ 167 /* LDV_COMMENT_FUNCTION_CALL Kernel calls driver release function before driver will be uploaded from kernel. This function declared as "MODULE_EXIT(function name)". */ 168 my_exit(); 169 170 /* LDV_COMMENT_FUNCTION_CALL Checks that all resources and locks are correctly released before the driver will be unloaded. */ 171 ldv_final: ldv_check_final_state(); 172 173 /* LDV_COMMENT_END_FUNCTION_CALL_SECTION */ 174 return; 175 176 } 177 #endif 178 179 /* LDV_COMMENT_END_MAIN */ 180 181 #include "engine-blast.h" 182 183 /* Module locks counter (1 is the initial state; it shouldn't go lower). We do not distinguish different modules. */ 184 int ldv_module_refcounter = 1; 185 186 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_module_get') Increment module reference counter (unless the module pointer is NULL). */ 187 void ldv_module_get(struct module *module) 188 { 189 /* LDV_COMMENT_OTHER Do nothing if the module pointer is NULL */ 190 if (module){ 191 /* LDV_COMMENT_CHANGE_STATE Increment module reference counter. */ 192 ldv_module_refcounter++; 193 } 194 } 195 196 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_try_module_get') Try to get module. The operation may succeed and return 1, or fail and return 0. */ 197 int ldv_try_module_get(struct module *module) 198 { 199 int module_get_succeeded; 200 201 /* LDV_COMMENT_OTHER Do nothing if the module pointer is NULL */ 202 if (module){ 203 204 /* LDV_COMMENT_OTHER Model success or failure of getting the module. */ 205 module_get_succeeded = ldv_undef_int(); 206 207 if (module_get_succeeded == 1) { 208 /* LDV_COMMENT_CHANGE_STATE Increment module reference counter. */ 209 ldv_module_refcounter++; 210 /* LDV_COMMENT_RETURN Return 1 telling about success. */ 211 return 1; 212 } 213 else 214 { 215 /* LDV_COMMENT_RETURN Return 0 telling that module get has failed.. */ 216 return 0; 217 } 218 } 219 } 220 221 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_module_put') Put module (unless module pointer is zero). Check if the module reference counter was greater than zero. */ 222 void ldv_module_put(struct module *module) 223 { 224 /* LDV_COMMENT_OTHER Do nothing if the module pointer is NULL */ 225 if (module){ 226 /* LDV_COMMENT_ASSERT This assertion fails if the module was put more times than it was got */ 227 ldv_assert(ldv_module_refcounter > 1); 228 /* LDV_COMMENT_CHANGE_STATE Decrease reference counter thus putting the module. */ 229 ldv_module_refcounter--; 230 } 231 } 232 233 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_module_put_and_exit') Put the module and stop execution. */ 234 void ldv_module_put_and_exit() 235 { 236 ldv_module_put((struct module*)1); 237 /* LDV_COMMENT_OTHER Stop execution. */ 238 LDV_STOP: goto LDV_STOP; 239 } 240 241 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_module_refcount') Get the reference counter of the module. */ 242 unsigned int ldv_module_refcount(void) 243 { 244 /* LDV_COMMENT_RETURN Return reference counter */ 245 return ldv_module_refcounter - 1; 246 } 247 248 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='check_final_state') At the end of execution, module reference counter must be the same as at the beginning. */ 249 void ldv_check_final_state(void) 250 { 251 /* LDV_COMMENT_ASSERT If this assertion is violated, then the module was put somewhere duiring the execution, and wasn't got! */ 252 ldv_assert(ldv_module_refcounter == 1); 253 }

Here is the explanation of the rule violation arisen in your driver for the corresponding kernel.

Note that there may be no error indeed. Please see on error trace and source code to understand whether there is an error in your driver.

The Error trace column contains the path on which rule is violated. You can choose some entity classes to be shown or hiden by clicking on the corresponding checkboxes or in the advanced Others menu. Also you can show or hide each particular entity by clicking on the corresponding - or +. In hovering on some entities you can see their descriptions and meaning. Also the error trace is binded with the source code. Line numbers are shown as links on the left. You can click on them to open the corresponding line in source code. Line numbers and file names are shown in entity descriptions.

The Source code column contains content of files related with the error trace. There are your driver (note that there are some our modifications at the end), kernel headers and rule source code. Tabs show the currently opened file and other available files. In hovering you can see file names in titles. On clicking the corresponding file content will be shown.