Bug

[В начало]

Ошибка # 138

Показать/спрятать трассу ошибок
Error trace
Function bodies
Blocks
  • Others...
    Function bodies without model function calls
    Initialization function calls
    Initialization function bodies
    Entry point
    Entry point body
    Function calls
    Skipped function calls
    Formal parameter names
    Declarations
    Assumes
    Assume conditions
    Returns
    Return values
    DEG initialization
    DEG function calls
    Model function calls
    Model function bodies
    Model asserts
    Model state changes
    Model function function calls
    Model function function bodies
    Model returns
    Model others
    Identation
    Line numbers
    Expand signs
-entry_point
{
487 ldv_s_adp5520_bl_driver_platform_driver = 0;
475 LDV_IN_INTERRUPT = 1;
484 ldv_initialize() { /* Function call is skipped due to function is undefined */}
490 goto ldv_29189;
490 tmp___0 = nondet_int() { /* Function call is skipped due to function is undefined */}
490 assume(tmp___0 != 0);
493 goto ldv_29188;
491 ldv_29188:;
494 tmp = nondet_int() { /* Function call is skipped due to function is undefined */}
494 switch (tmp);
495 assume(!(tmp == 0));
517 assume(!(tmp == 1));
538 assume(tmp == 2);
541 assume(ldv_s_adp5520_bl_driver_platform_driver == 0);
546 -adp5520_bl_probe(var_group2)
{
295 ret = 0;
297 +devm_kzalloc(&(pdev->dev), 192UL, 37748928U)
297 data = (struct adp5520_bl *)tmp;
298 assume(!(((unsigned long)data) == ((unsigned long)((struct adp5520_bl *)0))));
301 data->master = pdev->dev.parent;
302 +dev_get_platdata((const struct device *)(&(pdev->dev)))
302 data->pdata = (struct adp5520_backlight_platform_data *)tmp___0;
304 unsigned long __CPAchecker_TMP_0 = (unsigned long)(data->pdata);
304 assume(!(__CPAchecker_TMP_0 == ((unsigned long)((struct adp5520_backlight_platform_data *)0))));
309 data->id = pdev->id;
310 data->current_brightness = 0;
312 __mutex_init(&(data->lock), "&data->lock", &__key) { /* Function call is skipped due to function is undefined */}
314 __memset((void *)(&props), 0, 24UL) { /* Function call is skipped due to function is undefined */}
315 props.type = 1;
316 props.max_brightness = 127;
317 bl = devm_backlight_device_register(&(pdev->dev), pdev->name, data->master, (void *)data, &adp5520_bl_ops, (const struct backlight_properties *)(&props)) { /* Function call is skipped due to function is undefined */}
320 +IS_ERR((const void *)bl)
320 assume(((int)tmp___2) == 0);
325 bl->props.brightness = 127;
326 unsigned int __CPAchecker_TMP_1 = (unsigned int)(data->pdata->en_ambl_sens);
326 assume(__CPAchecker_TMP_1 != 0U);
327 -ldv_sysfs_create_group_5(&(bl->dev.kobj), &adp5520_bl_attr_group)
{
99 -ldv_sysfs_create_group(ldv_func_arg1, ldv_func_arg2)
{
21 tmp = ldv_undef_int() { /* Function call is skipped due to function is undefined */}
21 assume(tmp != 0);
22 LDV_SYSFS_GROUPS = LDV_SYSFS_GROUPS + 1;
23 return 0;;
}
99 return tmp;;
}
330 assume(!(ret != 0));
335 +platform_set_drvdata(pdev, (void *)bl)
336 +adp5520_bl_setup(bl)
336 ret = tmp___3 | ret;
337 +backlight_update_status(bl)
339 return ret;;
}
547 ldv_check_return_value(res_adp5520_bl_probe_18) { /* Function call is skipped due to function is undefined */}
548 ldv_check_return_value_probe(res_adp5520_bl_probe_18) { /* Function call is skipped due to function is undefined */}
549 assume(res_adp5520_bl_probe_18 != 0);
550 goto ldv_module_exit;
592 +ldv_check_final_state()
}
Source code
1 2 /* 3 * Backlight driver for Analog Devices ADP5520/ADP5501 MFD PMICs 4 * 5 * Copyright 2009 Analog Devices Inc. 6 * 7 * Licensed under the GPL-2 or later. 8 */ 9 10 #include <linux/kernel.h> 11 #include <linux/init.h> 12 #include <linux/platform_device.h> 13 #include <linux/fb.h> 14 #include <linux/backlight.h> 15 #include <linux/mfd/adp5520.h> 16 #include <linux/slab.h> 17 #include <linux/module.h> 18 19 struct adp5520_bl { 20 struct device *master; 21 struct adp5520_backlight_platform_data *pdata; 22 struct mutex lock; 23 unsigned long cached_daylight_max; 24 int id; 25 int current_brightness; 26 }; 27 28 static int adp5520_bl_set(struct backlight_device *bl, int brightness) 29 { 30 struct adp5520_bl *data = bl_get_data(bl); 31 struct device *master = data->master; 32 int ret = 0; 33 34 if (data->pdata->en_ambl_sens) { 35 if ((brightness > 0) && (brightness < ADP5020_MAX_BRIGHTNESS)) { 36 /* Disable Ambient Light auto adjust */ 37 ret |= adp5520_clr_bits(master, ADP5520_BL_CONTROL, 38 ADP5520_BL_AUTO_ADJ); 39 ret |= adp5520_write(master, ADP5520_DAYLIGHT_MAX, 40 brightness); 41 } else { 42 /* 43 * MAX_BRIGHTNESS -> Enable Ambient Light auto adjust 44 * restore daylight l3 sysfs brightness 45 */ 46 ret |= adp5520_write(master, ADP5520_DAYLIGHT_MAX, 47 data->cached_daylight_max); 48 ret |= adp5520_set_bits(master, ADP5520_BL_CONTROL, 49 ADP5520_BL_AUTO_ADJ); 50 } 51 } else { 52 ret |= adp5520_write(master, ADP5520_DAYLIGHT_MAX, brightness); 53 } 54 55 if (data->current_brightness && brightness == 0) 56 ret |= adp5520_set_bits(master, 57 ADP5520_MODE_STATUS, ADP5520_DIM_EN); 58 else if (data->current_brightness == 0 && brightness) 59 ret |= adp5520_clr_bits(master, 60 ADP5520_MODE_STATUS, ADP5520_DIM_EN); 61 62 if (!ret) 63 data->current_brightness = brightness; 64 65 return ret; 66 } 67 68 static int adp5520_bl_update_status(struct backlight_device *bl) 69 { 70 int brightness = bl->props.brightness; 71 72 if (bl->props.power != FB_BLANK_UNBLANK) 73 brightness = 0; 74 75 if (bl->props.fb_blank != FB_BLANK_UNBLANK) 76 brightness = 0; 77 78 return adp5520_bl_set(bl, brightness); 79 } 80 81 static int adp5520_bl_get_brightness(struct backlight_device *bl) 82 { 83 struct adp5520_bl *data = bl_get_data(bl); 84 int error; 85 uint8_t reg_val; 86 87 error = adp5520_read(data->master, ADP5520_BL_VALUE, &reg_val); 88 89 return error ? data->current_brightness : reg_val; 90 } 91 92 static const struct backlight_ops adp5520_bl_ops = { 93 .update_status = adp5520_bl_update_status, 94 .get_brightness = adp5520_bl_get_brightness, 95 }; 96 97 static int adp5520_bl_setup(struct backlight_device *bl) 98 { 99 struct adp5520_bl *data = bl_get_data(bl); 100 struct device *master = data->master; 101 struct adp5520_backlight_platform_data *pdata = data->pdata; 102 int ret = 0; 103 104 ret |= adp5520_write(master, ADP5520_DAYLIGHT_MAX, 105 pdata->l1_daylight_max); 106 ret |= adp5520_write(master, ADP5520_DAYLIGHT_DIM, 107 pdata->l1_daylight_dim); 108 109 if (pdata->en_ambl_sens) { 110 data->cached_daylight_max = pdata->l1_daylight_max; 111 ret |= adp5520_write(master, ADP5520_OFFICE_MAX, 112 pdata->l2_office_max); 113 ret |= adp5520_write(master, ADP5520_OFFICE_DIM, 114 pdata->l2_office_dim); 115 ret |= adp5520_write(master, ADP5520_DARK_MAX, 116 pdata->l3_dark_max); 117 ret |= adp5520_write(master, ADP5520_DARK_DIM, 118 pdata->l3_dark_dim); 119 ret |= adp5520_write(master, ADP5520_L2_TRIP, 120 pdata->l2_trip); 121 ret |= adp5520_write(master, ADP5520_L2_HYS, 122 pdata->l2_hyst); 123 ret |= adp5520_write(master, ADP5520_L3_TRIP, 124 pdata->l3_trip); 125 ret |= adp5520_write(master, ADP5520_L3_HYS, 126 pdata->l3_hyst); 127 ret |= adp5520_write(master, ADP5520_ALS_CMPR_CFG, 128 ALS_CMPR_CFG_VAL(pdata->abml_filt, 129 ADP5520_L3_EN)); 130 } 131 132 ret |= adp5520_write(master, ADP5520_BL_CONTROL, 133 BL_CTRL_VAL(pdata->fade_led_law, 134 pdata->en_ambl_sens)); 135 136 ret |= adp5520_write(master, ADP5520_BL_FADE, FADE_VAL(pdata->fade_in, 137 pdata->fade_out)); 138 139 ret |= adp5520_set_bits(master, ADP5520_MODE_STATUS, 140 ADP5520_BL_EN | ADP5520_DIM_EN); 141 142 return ret; 143 } 144 145 static ssize_t adp5520_show(struct device *dev, char *buf, int reg) 146 { 147 struct adp5520_bl *data = dev_get_drvdata(dev); 148 int ret; 149 uint8_t reg_val; 150 151 mutex_lock(&data->lock); 152 ret = adp5520_read(data->master, reg, &reg_val); 153 mutex_unlock(&data->lock); 154 155 if (ret < 0) 156 return ret; 157 158 return sprintf(buf, "%u\n", reg_val); 159 } 160 161 static ssize_t adp5520_store(struct device *dev, const char *buf, 162 size_t count, int reg) 163 { 164 struct adp5520_bl *data = dev_get_drvdata(dev); 165 unsigned long val; 166 int ret; 167 168 ret = kstrtoul(buf, 10, &val); 169 if (ret) 170 return ret; 171 172 mutex_lock(&data->lock); 173 adp5520_write(data->master, reg, val); 174 mutex_unlock(&data->lock); 175 176 return count; 177 } 178 179 static ssize_t adp5520_bl_dark_max_show(struct device *dev, 180 struct device_attribute *attr, char *buf) 181 { 182 return adp5520_show(dev, buf, ADP5520_DARK_MAX); 183 } 184 185 static ssize_t adp5520_bl_dark_max_store(struct device *dev, 186 struct device_attribute *attr, 187 const char *buf, size_t count) 188 { 189 return adp5520_store(dev, buf, count, ADP5520_DARK_MAX); 190 } 191 static DEVICE_ATTR(dark_max, 0664, adp5520_bl_dark_max_show, 192 adp5520_bl_dark_max_store); 193 194 static ssize_t adp5520_bl_office_max_show(struct device *dev, 195 struct device_attribute *attr, char *buf) 196 { 197 return adp5520_show(dev, buf, ADP5520_OFFICE_MAX); 198 } 199 200 static ssize_t adp5520_bl_office_max_store(struct device *dev, 201 struct device_attribute *attr, 202 const char *buf, size_t count) 203 { 204 return adp5520_store(dev, buf, count, ADP5520_OFFICE_MAX); 205 } 206 static DEVICE_ATTR(office_max, 0664, adp5520_bl_office_max_show, 207 adp5520_bl_office_max_store); 208 209 static ssize_t adp5520_bl_daylight_max_show(struct device *dev, 210 struct device_attribute *attr, char *buf) 211 { 212 return adp5520_show(dev, buf, ADP5520_DAYLIGHT_MAX); 213 } 214 215 static ssize_t adp5520_bl_daylight_max_store(struct device *dev, 216 struct device_attribute *attr, 217 const char *buf, size_t count) 218 { 219 struct adp5520_bl *data = dev_get_drvdata(dev); 220 int ret; 221 222 ret = kstrtoul(buf, 10, &data->cached_daylight_max); 223 if (ret < 0) 224 return ret; 225 226 return adp5520_store(dev, buf, count, ADP5520_DAYLIGHT_MAX); 227 } 228 static DEVICE_ATTR(daylight_max, 0664, adp5520_bl_daylight_max_show, 229 adp5520_bl_daylight_max_store); 230 231 static ssize_t adp5520_bl_dark_dim_show(struct device *dev, 232 struct device_attribute *attr, char *buf) 233 { 234 return adp5520_show(dev, buf, ADP5520_DARK_DIM); 235 } 236 237 static ssize_t adp5520_bl_dark_dim_store(struct device *dev, 238 struct device_attribute *attr, 239 const char *buf, size_t count) 240 { 241 return adp5520_store(dev, buf, count, ADP5520_DARK_DIM); 242 } 243 static DEVICE_ATTR(dark_dim, 0664, adp5520_bl_dark_dim_show, 244 adp5520_bl_dark_dim_store); 245 246 static ssize_t adp5520_bl_office_dim_show(struct device *dev, 247 struct device_attribute *attr, char *buf) 248 { 249 return adp5520_show(dev, buf, ADP5520_OFFICE_DIM); 250 } 251 252 static ssize_t adp5520_bl_office_dim_store(struct device *dev, 253 struct device_attribute *attr, 254 const char *buf, size_t count) 255 { 256 return adp5520_store(dev, buf, count, ADP5520_OFFICE_DIM); 257 } 258 static DEVICE_ATTR(office_dim, 0664, adp5520_bl_office_dim_show, 259 adp5520_bl_office_dim_store); 260 261 static ssize_t adp5520_bl_daylight_dim_show(struct device *dev, 262 struct device_attribute *attr, char *buf) 263 { 264 return adp5520_show(dev, buf, ADP5520_DAYLIGHT_DIM); 265 } 266 267 static ssize_t adp5520_bl_daylight_dim_store(struct device *dev, 268 struct device_attribute *attr, 269 const char *buf, size_t count) 270 { 271 return adp5520_store(dev, buf, count, ADP5520_DAYLIGHT_DIM); 272 } 273 static DEVICE_ATTR(daylight_dim, 0664, adp5520_bl_daylight_dim_show, 274 adp5520_bl_daylight_dim_store); 275 276 static struct attribute *adp5520_bl_attributes[] = { 277 &dev_attr_dark_max.attr, 278 &dev_attr_dark_dim.attr, 279 &dev_attr_office_max.attr, 280 &dev_attr_office_dim.attr, 281 &dev_attr_daylight_max.attr, 282 &dev_attr_daylight_dim.attr, 283 NULL 284 }; 285 286 static const struct attribute_group adp5520_bl_attr_group = { 287 .attrs = adp5520_bl_attributes, 288 }; 289 290 static int adp5520_bl_probe(struct platform_device *pdev) 291 { 292 struct backlight_properties props; 293 struct backlight_device *bl; 294 struct adp5520_bl *data; 295 int ret = 0; 296 297 data = devm_kzalloc(&pdev->dev, sizeof(*data), GFP_KERNEL); 298 if (data == NULL) 299 return -ENOMEM; 300 301 data->master = pdev->dev.parent; 302 data->pdata = dev_get_platdata(&pdev->dev); 303 304 if (data->pdata == NULL) { 305 dev_err(&pdev->dev, "missing platform data\n"); 306 return -ENODEV; 307 } 308 309 data->id = pdev->id; 310 data->current_brightness = 0; 311 312 mutex_init(&data->lock); 313 314 memset(&props, 0, sizeof(struct backlight_properties)); 315 props.type = BACKLIGHT_RAW; 316 props.max_brightness = ADP5020_MAX_BRIGHTNESS; 317 bl = devm_backlight_device_register(&pdev->dev, pdev->name, 318 data->master, data, &adp5520_bl_ops, 319 &props); 320 if (IS_ERR(bl)) { 321 dev_err(&pdev->dev, "failed to register backlight\n"); 322 return PTR_ERR(bl); 323 } 324 325 bl->props.brightness = ADP5020_MAX_BRIGHTNESS; 326 if (data->pdata->en_ambl_sens) 327 ret = sysfs_create_group(&bl->dev.kobj, 328 &adp5520_bl_attr_group); 329 330 if (ret) { 331 dev_err(&pdev->dev, "failed to register sysfs\n"); 332 return ret; 333 } 334 335 platform_set_drvdata(pdev, bl); 336 ret |= adp5520_bl_setup(bl); 337 backlight_update_status(bl); 338 339 return ret; 340 } 341 342 static int adp5520_bl_remove(struct platform_device *pdev) 343 { 344 struct backlight_device *bl = platform_get_drvdata(pdev); 345 struct adp5520_bl *data = bl_get_data(bl); 346 347 adp5520_clr_bits(data->master, ADP5520_MODE_STATUS, ADP5520_BL_EN); 348 349 if (data->pdata->en_ambl_sens) 350 sysfs_remove_group(&bl->dev.kobj, 351 &adp5520_bl_attr_group); 352 353 return 0; 354 } 355 356 #ifdef CONFIG_PM_SLEEP 357 static int adp5520_bl_suspend(struct device *dev) 358 { 359 struct backlight_device *bl = dev_get_drvdata(dev); 360 361 return adp5520_bl_set(bl, 0); 362 } 363 364 static int adp5520_bl_resume(struct device *dev) 365 { 366 struct backlight_device *bl = dev_get_drvdata(dev); 367 368 backlight_update_status(bl); 369 return 0; 370 } 371 #endif 372 373 static SIMPLE_DEV_PM_OPS(adp5520_bl_pm_ops, adp5520_bl_suspend, 374 adp5520_bl_resume); 375 376 static struct platform_driver adp5520_bl_driver = { 377 .driver = { 378 .name = "adp5520-backlight", 379 .pm = &adp5520_bl_pm_ops, 380 }, 381 .probe = adp5520_bl_probe, 382 .remove = adp5520_bl_remove, 383 }; 384 385 module_platform_driver(adp5520_bl_driver); 386 387 MODULE_AUTHOR("Michael Hennerich <hennerich@blackfin.uclinux.org>"); 388 MODULE_DESCRIPTION("ADP5520(01) Backlight Driver"); 389 MODULE_LICENSE("GPL"); 390 MODULE_ALIAS("platform:adp5520-backlight"); 391 392 393 394 395 396 /* LDV_COMMENT_BEGIN_MAIN */ 397 #ifdef LDV_MAIN0_sequence_infinite_withcheck_stateful 398 399 /*###########################################################################*/ 400 401 /*############## Driver Environment Generator 0.2 output ####################*/ 402 403 /*###########################################################################*/ 404 405 406 407 /* 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. */ 408 void ldv_check_final_state(void); 409 410 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Test correct return result. */ 411 void ldv_check_return_value(int res); 412 413 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Test correct return result of probe() function. */ 414 void ldv_check_return_value_probe(int res); 415 416 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Initializes the model. */ 417 void ldv_initialize(void); 418 419 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Reinitializes the model between distinct model function calls. */ 420 void ldv_handler_precall(void); 421 422 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Returns arbitrary interger value. */ 423 int nondet_int(void); 424 425 /* LDV_COMMENT_VAR_DECLARE_LDV Special variable for LDV verifier. */ 426 int LDV_IN_INTERRUPT; 427 428 /* LDV_COMMENT_FUNCTION_MAIN Main function for LDV verifier. */ 429 void ldv_main0_sequence_infinite_withcheck_stateful(void) { 430 431 432 433 /* LDV_COMMENT_BEGIN_VARIABLE_DECLARATION_PART */ 434 /*============================= VARIABLE DECLARATION PART =============================*/ 435 /** STRUCT: struct type: backlight_ops, struct name: adp5520_bl_ops **/ 436 /* content: static int adp5520_bl_update_status(struct backlight_device *bl)*/ 437 /* LDV_COMMENT_END_PREP */ 438 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "adp5520_bl_update_status" */ 439 struct backlight_device * var_group1; 440 /* LDV_COMMENT_BEGIN_PREP */ 441 #ifdef CONFIG_PM_SLEEP 442 #endif 443 /* LDV_COMMENT_END_PREP */ 444 /* content: static int adp5520_bl_get_brightness(struct backlight_device *bl)*/ 445 /* LDV_COMMENT_END_PREP */ 446 /* LDV_COMMENT_BEGIN_PREP */ 447 #ifdef CONFIG_PM_SLEEP 448 #endif 449 /* LDV_COMMENT_END_PREP */ 450 451 /** STRUCT: struct type: platform_driver, struct name: adp5520_bl_driver **/ 452 /* content: static int adp5520_bl_probe(struct platform_device *pdev)*/ 453 /* LDV_COMMENT_END_PREP */ 454 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "adp5520_bl_probe" */ 455 struct platform_device * var_group2; 456 /* LDV_COMMENT_VAR_DECLARE Variable declaration for test return result from function call "adp5520_bl_probe" */ 457 static int res_adp5520_bl_probe_18; 458 /* LDV_COMMENT_BEGIN_PREP */ 459 #ifdef CONFIG_PM_SLEEP 460 #endif 461 /* LDV_COMMENT_END_PREP */ 462 /* content: static int adp5520_bl_remove(struct platform_device *pdev)*/ 463 /* LDV_COMMENT_END_PREP */ 464 /* LDV_COMMENT_BEGIN_PREP */ 465 #ifdef CONFIG_PM_SLEEP 466 #endif 467 /* LDV_COMMENT_END_PREP */ 468 469 470 471 472 /* LDV_COMMENT_END_VARIABLE_DECLARATION_PART */ 473 /* LDV_COMMENT_BEGIN_VARIABLE_INITIALIZING_PART */ 474 /*============================= VARIABLE INITIALIZING PART =============================*/ 475 LDV_IN_INTERRUPT=1; 476 477 478 479 480 /* LDV_COMMENT_END_VARIABLE_INITIALIZING_PART */ 481 /* LDV_COMMENT_BEGIN_FUNCTION_CALL_SECTION */ 482 /*============================= FUNCTION CALL SECTION =============================*/ 483 /* LDV_COMMENT_FUNCTION_CALL Initialize LDV model. */ 484 ldv_initialize(); 485 486 487 int ldv_s_adp5520_bl_driver_platform_driver = 0; 488 489 490 while( nondet_int() 491 || !(ldv_s_adp5520_bl_driver_platform_driver == 0) 492 ) { 493 494 switch(nondet_int()) { 495 496 case 0: { 497 498 /** STRUCT: struct type: backlight_ops, struct name: adp5520_bl_ops **/ 499 500 501 /* content: static int adp5520_bl_update_status(struct backlight_device *bl)*/ 502 /* LDV_COMMENT_END_PREP */ 503 /* LDV_COMMENT_FUNCTION_CALL Function from field "update_status" from driver structure with callbacks "adp5520_bl_ops" */ 504 ldv_handler_precall(); 505 adp5520_bl_update_status( var_group1); 506 /* LDV_COMMENT_BEGIN_PREP */ 507 #ifdef CONFIG_PM_SLEEP 508 #endif 509 /* LDV_COMMENT_END_PREP */ 510 511 512 513 514 } 515 516 break; 517 case 1: { 518 519 /** STRUCT: struct type: backlight_ops, struct name: adp5520_bl_ops **/ 520 521 522 /* content: static int adp5520_bl_get_brightness(struct backlight_device *bl)*/ 523 /* LDV_COMMENT_END_PREP */ 524 /* LDV_COMMENT_FUNCTION_CALL Function from field "get_brightness" from driver structure with callbacks "adp5520_bl_ops" */ 525 ldv_handler_precall(); 526 adp5520_bl_get_brightness( var_group1); 527 /* LDV_COMMENT_BEGIN_PREP */ 528 #ifdef CONFIG_PM_SLEEP 529 #endif 530 /* LDV_COMMENT_END_PREP */ 531 532 533 534 535 } 536 537 break; 538 case 2: { 539 540 /** STRUCT: struct type: platform_driver, struct name: adp5520_bl_driver **/ 541 if(ldv_s_adp5520_bl_driver_platform_driver==0) { 542 543 /* content: static int adp5520_bl_probe(struct platform_device *pdev)*/ 544 /* LDV_COMMENT_END_PREP */ 545 /* LDV_COMMENT_FUNCTION_CALL Function from field "probe" from driver structure with callbacks "adp5520_bl_driver". Standart function test for correct return result. */ 546 res_adp5520_bl_probe_18 = adp5520_bl_probe( var_group2); 547 ldv_check_return_value(res_adp5520_bl_probe_18); 548 ldv_check_return_value_probe(res_adp5520_bl_probe_18); 549 if(res_adp5520_bl_probe_18) 550 goto ldv_module_exit; 551 /* LDV_COMMENT_BEGIN_PREP */ 552 #ifdef CONFIG_PM_SLEEP 553 #endif 554 /* LDV_COMMENT_END_PREP */ 555 ldv_s_adp5520_bl_driver_platform_driver++; 556 557 } 558 559 } 560 561 break; 562 case 3: { 563 564 /** STRUCT: struct type: platform_driver, struct name: adp5520_bl_driver **/ 565 if(ldv_s_adp5520_bl_driver_platform_driver==1) { 566 567 /* content: static int adp5520_bl_remove(struct platform_device *pdev)*/ 568 /* LDV_COMMENT_END_PREP */ 569 /* LDV_COMMENT_FUNCTION_CALL Function from field "remove" from driver structure with callbacks "adp5520_bl_driver" */ 570 ldv_handler_precall(); 571 adp5520_bl_remove( var_group2); 572 /* LDV_COMMENT_BEGIN_PREP */ 573 #ifdef CONFIG_PM_SLEEP 574 #endif 575 /* LDV_COMMENT_END_PREP */ 576 ldv_s_adp5520_bl_driver_platform_driver=0; 577 578 } 579 580 } 581 582 break; 583 default: break; 584 585 } 586 587 } 588 589 ldv_module_exit: 590 591 /* LDV_COMMENT_FUNCTION_CALL Checks that all resources and locks are correctly released before the driver will be unloaded. */ 592 ldv_final: ldv_check_final_state(); 593 594 /* LDV_COMMENT_END_FUNCTION_CALL_SECTION */ 595 return; 596 597 } 598 #endif 599 600 /* LDV_COMMENT_END_MAIN */

Here is an explanation of a rule violation arisen while checking your driver against a corresponding kernel.

Note that it may be false positive, i.e. there isn't a real error indeed. Please analyze a given error trace and related source code to understand whether there is an error in your driver.

Error trace column contains a path on which the given rule is violated. You can expand/collapse some entity classes by clicking on corresponding checkboxes in a main menu or in an advanced Others menu. Also you can expand/collapse each particular entity by clicking on +/-. In hovering on some entities you can see some tips. Also the error trace is bound with related source code. Line numbers may be shown as links on the left. You can click on them to open corresponding lines in source code.

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

Ядро Модуль Правило Верификатор Вердикт Статус Время создания Описание проблемы
linux-4.7-rc1.tar.xz drivers/video/backlight/adp5520_bl.ko 151_1a CPAchecker Bug Fixed 2016-07-09 01:20:47 L0261

Комментарий

Reported: 9 Jul 2016

[В начало]