--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on January 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problems with Frama-C libc



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.