--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on January 2012 ---
Hello everyone, I have problems to make Frama-C compute on this small example : //------------------------------------------------------------------ #include <stdio.h> #include <stdlib.h> #include <string.h> int main (int argc, char * argv []) { if (argc == 2) { unsigned int len = strlen (argv[1]) + 1; char * s = malloc (len); if (s) { strncpy (s, argv [1], len); printf ("arg1: %s\n", s); } } return 0; } //------------------------------------------------------------------ with options : -val -cpp-extra-args="-I`frama-c -print-path`/libc" to use Frama-C libc specifications. More precisely, it seems that the value analysis detect that the call to [printf] is unreachable because [strncpy] doesn't return properly. I thought that maybe it was because of [strncpy] precondition, so I tried to add: //@ assert \valid_range(s,0,len-1) && valid_string(argv[1]); just before the call to [strncpy], but it doesn't change anything. Does anybody have some advices to make Frama-C value analysis happy ? I don't really care about the precision of the result since I want to work on the PDG later on. I just need to have a reasonable over-approximation of the behaviours, ie. with a reachable call to [printf]. Thanks in advance for your help, -- Anne.