--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on December 2008 ---
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.