Feature #11014
closed
Avoid infinite loops in environment models
Added by Evgeny Novikov over 2 years ago.
Updated about 2 years ago.
Category:
Environment models
Description
After Ilja has supported the way to configure the number of loop iterations for environment processes (#10929), we have an ability to simplify environment models.
- Related to Feature #10929: Do not invoke callbacks infinitely and allow to configure the number of iterations added
- Status changed from New to Closed
I implemented this in branch avoid-infinite-loops-in-env-models. This branch passed almost all test cases. There were only 2 regressions, one was positive (timeout -> false alarm) and one was negative (safe -> timeout).
Much more important that it helps CPAchecker SMG very considerably at verification of a bunch of drivers. For instance, when verifying 2141 drivers, it could prove 124 more safes (most of them were timeouts earlier). Moreover, several new unsafes were found while many false alarms due to some bugs in CPAchecker SMG have gone.
I merged the branch to master in ad04f7d01.
Also available in: Atom
PDF