Feature #9931
Updated by Evgeny Novikov over 4 years ago
Some environment models can result in faults. Typical examples are the following:
# Assertions can fail within _ldv_check_final_state()_.
# CPAchecker SMG can reveal, say, memory leaks, when an environment model frees memory for object for which another environment model allocated memory and that was passed to a driver callback that allocated but did not free another memory.
In both cases corresponding actions are not callback actions by definition (although the first one is called so by mistake), so, they are not included in error trace patterns of unsafe marks. This is wrong, since these patterns miss error trace parts important from the point of view of checking.
In addition, I suggest to name environment model functions in a more user friendly way. For instance, _ldv_emg_wrapper_platram_probe_2()_ does not seem to be a good choice. I am almost sure, that it can be safely named _ldv_platram_probe()_. Perhaps, you need to add some more unique identifiers to support several instances of platform_driver within one driver as well as within several drivers analyzed together. So, the right name can look like _ldv_plat_ram_platram_driver_platram_probe()_. Ditto, there should be nice names of specific environment model functions, that, say, allocates/frees memory for objects to be passed to drivers, e.g. _ldv_plat_ram_platram_driver_allocate_resources()_ and _ldv_plat_ram_platram_driver_free_resources()_.