--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on May 2009 ---
Here is a small code sample: #include <pwd.h> int main() { int ret; struct passwd *pw = getpwnam("root"); if (pw->pw_passwd[0] == 0) ret = pw->pw_passwd[0]; else ret = 1; return ret; } The variation domain of the returned value is {0; 1; }, but somehow the value analysis plugin fails to compute it. Apparently when assigning 'ret' to 'pw->pw_passwd[0]' it forgots that 'pw->pw_passwd[0]' should be '0' in that codeblock and fallback to 'alloced_return_getpwnam'. So I was wondering if it's should be reported as a bug or if it's the intended behavior. Because If I use a temporary variable, I can get the correct variation domain: include <pwd.h> int main() { int ret; struct passwd *pw = getpwnam("root"); char tmp = pw->pw_passwd[0]; if (tmp == 0) ret = tmp; else ret = 1; return ret; } Also I was wondering if there is way to make the value analysis plugin provides only 'real value' variation domains. I'm not sure how to say this properly so as an example, in the code sample following this sentence, the value analysis plugin would give me of course {0; } for the variation domain of 'ret' in 'code 1', but would also give me [1..255] (the whole range of possible values minus '0') in 'code 2' instead of 'alloced_return_getpwnam'. #include <pwd.h> int main() { struct passwd *pw = getpwnam("root"); char ret = pw->pw_passwd[0]; if (ret == 0) /* code 1 */ else /* code 2 */ return ret; }