Klever 3.7 was primarily devoted to improving a quality of verification results for Linux kernel drivers. After all about 43% of original false alarms issued when checking memory safety have gone.
Following fixes and improvements in Klever 3.7 deserve an attention:
- Adding new environment models for the Linux kernel:
- Modeling the list API.
- Modeling the kref API.
- Adding model for the input_ff_create_memless() function.
- Adding models for check_add_overflow(), check_sub_overflow() and check_mul_overflow() macros that fixes the struct_size() model for new versions of the Linux kernel.
- Modeling v4l2_device(un)register()_ functions.
- Modeling the i2c_match_id() function.
- Adding model for the dev_err_probe() function.
- Adding models for the dynamic debug printing API.
- Fixing existing environment models for the Linux kernel:
- Modeling failures for calloc() and zalloc().
- Fixing the off-by-one error when choosing a device from MODULE_DEVICE_TABLE.
- Passing the same resource to probe and remove for HID drivers.
- Allocating memory for inode for file_operations callbacks.
- Allocating memory for tty_struct for tty_operations callbacks.
- Avoiding using implicit resources in environment model specifications.
- Adding a new section to the user documentation: Verifying New Program.
- Fixing tests for environment model specifications and Environment Model Generator.
- Updating CIF which main file was rewritten in C++ and that started to print keyword static for local variables.
- Updating CPAchecker that supports packed/aligned attributes and issues violation witnesses more efficiently.
- Updating Python dependencies.
We would like to thank very much everybody who made this great job possible!