Skip to content

linux-3.4-32_1-drivers--usb--serial--usb_debug: stack-allocate var_group2

🤖 SoSy-Bot 🤖 requested to merge github/fork/tautschnig/init-var_group-5 into master

Created by: tautschnig

The initial counterexample produced by CBMC involved var_group2, which is passed to usb_debug_process_read_urb, where the underlying (non-allocated) storage is accessed via memcmp. Just allocate it as a local object.

Merge request reports