Actions
Feature #11007
closedSupport more SMG-friendly select of nondeterministic values from integer range
Start date:
11/09/2021
Due date:
% Done:
0%
Estimated time:
Published in build:
Description
Ilja implemented model function int ldv_random_int(int begin, int end) to generate nondeterministic integer values in range [begin, end). CPAchecker SMG does not work with that model function well since the limited support of predicates. Thus, we need to support another way to choose nondeterministic values from integer ranges for SMG.
Updated by Evgeny Novikov over 2 years ago
- Status changed from New to Resolved
I implemented this in branch smg-random-int.
Vital changes:- I renamed function ldv_random_int() to ldv_undef_int_range() (that is macro now) to avoid any confusion with standard functions returning a random value from a range.
- I included the end of range to the list of possible return values of ldv_undef_int_range(). This is controversial, but it looks more like the appropriate C standard function random().
In addition, I implemented test cases for both variants of ldv_undef_int_range().
At the moment the branch is tested by CI/CD.
Updated by Evgeny Novikov over 2 years ago
- Status changed from Resolved to Closed
After some fixes in environment model specifications tests passed, so I merged the branch to master in fee61d52fda9.
Actions