--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on May 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] A variation domain failed to be computed



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;
}