Klever

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 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.