Feature #11007
closed
Support more SMG-friendly select of nondeterministic values from integer range
Added by Evgeny Novikov over 2 years ago.
Updated over 2 years ago.
Category:
Environment models
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.
- 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.
- Status changed from Resolved to Closed
After some fixes in environment model specifications tests passed, so I merged the branch to master in fee61d52fda9.
Also available in: Atom
PDF