Feature #7392
Updated by Evgeny Novikov almost 8 years ago
Experiments show that some rule specifications can be checked together quite efficiently that It is with much less resources and without considerable changes in obtained verification verdicts. That is why we need a way to specify manually such groups of rules. In addition it is suggested to create just one big default common aspect and mark its parts by identifiers of rules or groups group of rules. Therefore, the user only specifies rules to check and the strategy, common aspect is added automatically in optimal way. Thus, common aspect should be similar to the following: #ifdef __REQUIREMENT_GROUP_68_69 around: call(struct urb *usb_alloc_urb(.., gfp_t flags, ..)) { struct urb *res = ldv_linux_usb_urb_usb_alloc_urb(); ldv_assume(!ldv_is_err(res)); ldv_linux_alloc_irq_check_alloc_flags(flags); ldv_linux_alloc_spin_lock_check_alloc_flags(flags); ldv_linux_alloc_usb_lock_check_alloc_flags(flags); return res; } #endif