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] A question on Frama-C input/output analysis

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