You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
sigh I'd hoped we'd moved on beyond duplicated functionality (remembering that time when we had four loop detection systems...). Yes; it would be good to not have this repeated. If your suggestion with test-gen is to be implemented (and it does sound like a good idea) it will have to be done by someone with access to test-gen (and the delegated legal authority to contribute it under BSD 4 clause).
See https://github.com/diffblue/cbmc/blob/develop/src/cbmc/bmc.cpp#L562 and https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/unwind.cpp#L53. The former is better but is specific to BMC, the latter includes comparisons to signed -1 instead of
std::numeric_limits::max
. As a result another duplicate has been made in https://github.com/diffblue/test-gen/pull/1236 which should be moved somewhere in CBMC and used by the existing two implementations.The text was updated successfully, but these errors were encountered: