Bug #7637
Updated by Evgeny Novikov over 7 years ago
Unfortunately now CPAchecker output witnesses so that there isn't an explicit call to the main (entry point) function. That's why global initialization immediately are followed follows by entry point declarations and statements. Bridge likely decides to pass into the entry point when it encounters a first really called function, e.g. _ldv_initialize()_ or a function representing _insmod/rmmod_. I suppose to uniformly determine a proper entry point beginning as a first edge in an error trace that has an assumption attribute.