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] Adding some semantic meaning to a few (standard string) functions

  • Subject: [Frama-c-discuss] Adding some semantic meaning to a few (standard string) functions
  • From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
  • Date: Mon, 15 Dec 2008 14:11:01 +0100
In the example code at the end of this message, at line 28, frama-c is
able to tell that boo's value is 2. However, at line 23, it can't tell
that *foo's value is "foobar".

Note that I didn't wrote foo's value, but *foo's value. I know that
frama-c is already analyzing foo's value as a pointer. But analyzing (a
bit) what it's poiting at might be useful. Of course, since generally a
pointer can point at anything, in most case, it might see nothing, but
at least in the case of strings I think a few things might be computed.

So I was wondering if it would possible to add this kind of knowledge to
frama-c through a plugin.

Of course, If I were to code, for example, my own strcmp-like function,
there's no way to automatically deduce this. But at least, for standard
string functions, and only for a few of them, we might want to
statically give this knowledge to frama-c. For example, if strcmp return
0, then it can be seen as ==, and so from the statement line 20, we know
that *foo can be anything but {""}. We could also see strcpy as =, and
so after the statement line 20, *bar is in {"foobar"}, and so is foo at
the statement line 23.

Ideally, it could compute that at the statement line 30, tmp is in
{"bar"}.

So any comment on this ? Bad/good idea ? Achievable or not ? (at least
in some simple case like this example). I'm already reading the plugin
manual ^^.

Another question about something I noticed while writing this example.
The statement at line 20 was originally written like this:

if(bar != strcpy(bar, "foobar"))
	return -1;

But it makes frama-c think this condition is always true and so all code
after this statement is considered as dead code. Since strcpy in most
case (when everything goes right) will in fact return 'bar', I don't see
what is wrong here.

The example code:

1.  #include <string.h>
2.  #include <stdio.h>
3.  
4.  extern char *foo;
5.  extern int boo;
6.  
7.  int main(){
8.  
9.  	int far;
10. 	char *tmp;
11. 
12. 	char bar[256];
13. 
14. 	if(foo == NULL || strlen(foo) > 254)
15. 		return -1;
16. 
17. 	if(strcmp(foo, "") == 0)
18. 		return 1;
19. 
20. 	strcpy(bar, "foobar");
21. 
22. 	if(strcmp(foo, bar) == 0)
23. 		printf(foo);
24. 
25. 	far = 2;
26. 
27. 	if(boo == far)
28. 		printf("%x", boo);
29. 	else if (boo == 3)
30. 		tmp = bar + boo;
31. 
32. 	return 0;
33. }
34.