--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on March 2011 ---
Hello, > Recently I used Frama-C to analyze the input/output information for each C > function. However, I found for some functions, there are many inputs (more > than 200, but most of them are similar). > > Here is one sample input, and hope that you could help me figure out why > these are generated by Frama-C. > > ##star_star_star_xx_pointer_0nth__inner_pointer_0nth__field[bits 0 to > 549755813887]## xx_pointer is one of pointers used in a function, > inner_pointer is a field of structure, pointed by xx_pointer, while field is > a field of structure, pointed by inner_pointer. These variables are generated by the value analysis to act as target for pointers (using -lib-entry, all global pointer variables; without -lib-entry, only the entry point's arguments). You are using a rather old version of Frama-C. One change since the version you are using was to change the format of the generated names to be shorter and more readable. Another change that came in Carbon was to generate fewer of these variables for large arrays. In previous version, for an array of size n, n target variables would be generated. Now, the maximum number of generated variable is limited to the value of option -context-width. You can obtain more information about the behavior of the current version in this respect in section 5.2.4, page 50 of http://frama-c.com/download/frama-c-value-analysis.pdf . Pascal