Project

General

Profile

Actions
Copy link

Bug #10755

closed

Double free for environment models

Added by Evgeny Novikov about 3 years ago. Updated about 3 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Ilja Zakharov
Category:
Environment models
Target version:
3.1
Start date:
03/15/2021
Due date:
% Done:

0%

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

Description

Likely recent changes in EMG or/and environment model specifications resulted in CPAchecker SMG started to reveal double free for environment models. For me it looks strange that there are phrases like "Callback callback postcondition" (it is not clear what second word "callback" means). There are following drivers demonstrating such the behavior:
  1. drivers/hid/hid-a4tech.ko
  2. drivers/hid/hid-apple.ko
  3. drivers/hid/hid-corsair.ko
  4. drivers/hid/hid-elan.ko
  5. drivers/hid/hid-microsoft.ko
  6. drivers/hid/hid-saitek.ko
  7. drivers/hid/hid-zydacron.ko
  8. drivers/media/platform/sti/bdisp/bdisp.ko
  9. drivers/platform/chrome/wilco_ec/wilco_ec_debugfs.ko
  10. drivers/platform/x86/ideapad-laptop.ko
  11. drivers/platform/x86/intel_telemetry_debugfs.ko
  12. drivers/staging/greybus/gb-uart.ko
  13. drivers/usb/host/isp1362-hcd.ko
  14. drivers/usb/host/sl811-hcd.ko
  15. drivers/usb/typec/tcpm/fusb302.ko

Please, check that after a fix verification results will change for all mentioned drivers.

More unlikely this is a result of recent changes in CPAchecker SMG, but I am not sure in this.

Actions
Copy link

Also available in: Atom PDF