--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on October 2016 ---
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