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] Casting to a generic function pointer

Thanks very much Andre. Your reply and the blog post were very helpful, and
after getting past those initial errors I am able to make more progress.
But I am running into this error below-- a bit strange because the the
frama-c libc definition of struct tcp_info has that field it is complaining

/data/.opam/system/share/frama-c/libc/netinet/tcp.h:  u_int32_t

Unless that definition is being picked up for somewhere else -- is there
any way I can figure out where it is reading that definition from?



  preprocessing with "gcc -E -C -I.  -I/data/.opam/system/share/frama-c/libc
-I/data/nginx-1.9.14/src/http -I/data/nginx-1.9.14/src/http/modules
-I/data/nginx-1.9.14/src/mail -I/data/nginx-1.9.14/src/stream
-I/data/nginx-1.9.14/objs -I/data/nginx-1.9.14/src/os/unix
-I/data/nginx-1.9.14/src/core -I/data/nginx-1.9.14/src/event -include
__fc_stubs.h -dD -nostdinc -m64 src/http/ngx_http_variables.c"

[kernel] Parsing src/http/ngx_http_variables.c (with preprocessing)

[kernel] Parsing /tmp/ngx_http_variables.ca1c446.ibcf80c.pp to Cabs

[kernel] Parsing /tmp/ngx_http_variables.ca1c446.ibcf80c.pp

[kernel] Converting /tmp/ngx_http_variables.ca1c446.ibcf80c.pp from Cabs to

[kernel] src/http/ngx_http_variables.c:1045: User Error:

  Cannot find field tcpi_rttvar in type struct tcp_info


  1044      case 1:

  1045          value = ti.tcpi_rttvar;


  1046          break;


[kernel] User Error: stopping on file "src/http/ngx_http_variables.c" that
has errors.


On Fri, Jul 6, 2018 at 7:26 PM, Andre Maroneze <

> Just to inform you, the blog post about parsing code bases such as nginx
> is online:
> realistic-code-bases-with-Frama-C
> On 05/07/18 15:22, Andre Maroneze wrote:
> Yes, it is related to using preprocessed files. Your preprocessed file
> must have included your system's headers, which do not include Frama-C's
> ACSL specifications for functions such as strlen(). As such, when Frama-C
> parses the .i files, it finds just a prototype without any specifications,
> and it will not assume that the function called strlen() in *your* file
> is necessarily the one from <string.h>.
> One solution might be to rename the .i file as a .c (to ensure Frama-C
> will preprocess it), manually add "#include <string.h>" and similar files,
> and try to parse it again. However, this is likely to create conflicts
> between the types in your prototypes with the ones in Frama-C's libc. You
> may have to erase some declarations from your preprocessed file.
> The overall question of parsing such code bases is interesting and will be
> the subject of a future post in the Frama-C blog.
> The summarized version is that the reason why `cpu_set_t` is not known is
> because it is not POSIX, and thus not present in Frama-C's libc. You should
> manually add such a typedef or macro to define it, probably based on the
> type used in your system. Something similar to this should work:
> typedef unsigned long __cpu_mask;
> # define __NCPUBITS (8 * sizeof (__cpu_mask))
> # define CPU_SETSIZE 1024
> typedef struct {
>   __cpu_mask __bits[CPU_SETSIZE / __NCPUBITS];
> } cpu_set_t;
> These definitions are based on those found in my system's libc.
> To parse nginx, you will likely need to include other types and
> definitions in a similar way. In the end, this step may take a significant
> amount of time, which is one of the reasons that the
> open-source-case-studies repository (
> open-source-case-studies) exists: so that only one person will ever have
> to work through this parsing stage, allowing others to proceed from there.
> As a final note: it is helpful, when possible, to disable optional,
> non-portable features from ./configure scripts, either with options such as
> --without-<feature>, or by manually editing the generated config.h file
> (e.g. objs/ngx_auto_config.h), and setting HAVE_<FEATURE> macros to 0.
> On 04/07/18 23:17, Divya Muthukumaran wrote:
> Thanks for the detailed answer Andre. I'm not sure if it has something to
> do with the fact that I am running this on preprocessed *.i files.
> I tried to run them on the original *.c files, but that fails with:
> [kernel] /data/nginx-1.9.14/src/os/unix/ngx_setaffinity.h:16:
>   syntax error:
>   Location: line 16, between columns 8 and 18, before or at token:
> ngx_cpuset_t
>   15
>   16    typedef cpu_set_t ngx_cpuset_t;
>         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>   17
> I did try frama-c on a toy example with the strlen and malloc calls and
> that works perfectly.
> --
> André Maroneze
> Researcher/Engineer CEA/LIST
> Software Reliability and Security Laboratory
> _______________________________________________
> Frama-c-discuss mailing listFrama-c-discuss at lists.gforge.inria.fr
> --
> André Maroneze
> Researcher/Engineer CEA/LIST
> Software Reliability and Security Laboratory
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>