C Instrumentation Framework

From http://forge.ispras.ru/issues/2462#note-10:
It seems that sound implementation of rerouter needs rule models to be extended rather considerably. When argument signature for, say, mutex_lock can't be calculated we need to call something like ldv_all_mutex_lock that will try to lock all known mutexes nondeterministically. "All" means that we should use template foreach like for ldv_initialize and ldv_check_final_state. Since there is neither iteration through model states nor nondeterminism in model for mutex_lock we better need to develop a separate model (that was called ldv_all_mutex_lock before). Since different functions have different sematics (some returns void, some returns error codes, some decrease counters) we need to develop such the separate models for all functions that have corresponding models already.
That's why some experiments should be executed before implementation. May be these experiments will show that we do can distinguish different object not only just by their names but also by names of references to them.