Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] A variation domain failed to be computed
  • From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
  • Date: Wed, 06 May 2009 17:41:59 +0200
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;
}