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] 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