--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on October 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Generating main function for Value Analysis



Dear Jens,

Le 27/10/2016 13:47, Gerlach, Jens a écrit :
> we are analyzing the source code of some C library with the Value Analysis.
>
> So, we have a large number of API functions often having user-defined structs as arguments.
> We think about generating a main function consisting of a loop in which in each cycle some API function is randomly called
> with randomly filled arguments.
> This way we could simulate the typcial usage of the library.
>
> Does Frama-C somehow support the task of generating such a main function?

I've actually developed a plug-in for one of our industrial partners 
which could help you. Indeed, from function's preconditions, it 
generates a main function which initializes the function context in 
order to satisfy the preconditions (but no more). Furthermore, the 
generated C code uses Value's built-ins whenever possible in a way that 
Value interprets it as precisely as possible.

For instance, if a function declaration is:

/*@ requires 0 < len <= 100;
   @ requires \valid(array+(0..len-1)); */
void init(int *array, int len);

It generates the following function context:

int __cfp_init(void)
{
   int __retres;
   int __cfp_len;
   int *__cfp_array;
   __cfp_len = Frama_C_int_interval(1,100);
   __cfp_array = (int *)malloc((unsigned int)(4LL * ((__cfp_len - 1LL) + 
1LL)));
   if (__cfp_array != (int *)0) init(__cfp_array,__cfp_len);
   __retres = 0;
   return __retres;
}

This plug-in is not freely available, but it should be possible to 
provide it in an official setting (e.g. an European project).

Best,
Julien