Bug #7637
closedProperly determine entry point beginning
100%
Description
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.
Updated by Vladimir Gratinskiy over 7 years ago
- Description updated (diff)
- Due date set to 10/26/2016
- Status changed from New to Resolved
- % Done changed from 0 to 100
Implemented in commit "4b97c8d" of "better-unsafes-and-marks" branch.
Earlier there was the same, but Bridge considered entry point is where the first assumption with assumption scope "entry_point" found. But in error traces the first assumption scope was "ldv_entry_point". I've deleted this condition.
Updated by Evgeny Novikov over 7 years ago
Great! Now error trace visualizer doesn't depend on underlying environment model generator.
Updated by Ilja Zakharov over 7 years ago
- Status changed from Resolved to Verified
Updated by Ilja Zakharov over 7 years ago
- Status changed from Verified to Closed
Merged in 6e2305dc.