Frama-C-discuss mailing list archives

divya84 at gmail.com (Divya Muthukumaran) · Thu, 12 Jul 2018 07:04:33 +0100

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
about.

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

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?

--------------------------------------------------------------------------------

[kernel:pp]

  preprocessing with "gcc -E -C -I.  -I/data/.opam/system/share/frama-c/libc
-D__FRAMAC__ -D__FC_MACHDEP_X86_64 -D__USE_GNU
-I/data/open-source-case-studies/nginx-1.9.14/ext_headers
-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
CIL

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

  Cannot find field tcpi_rttvar in type struct tcp_info

  1043

  1044      case 1:

  1045          value = ti.tcpi_rttvar;

        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

  1046          break;

  1047

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

Thanks,
Divya

On Fri, Jul 6, 2018 at 7:26 PM, Andre Maroneze <
Andre.OLIVEIRAMARONEZE at cea.fr> wrote:

> Just to inform you, the blog post about parsing code bases such as nginx
> is online:
>
> http://blog.frama-c.com/index.php?post/2018/07/06/Parsing-
> 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 (https://github.com/Frama-C/
> 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
>   14    #if (NGX_HAVE_SCHED_SETAFFINITY)
>   15
>   16    typedef cpu_set_t ngx_cpuset_t;
>         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>   17
>   18    #elif (NGX_HAVE_CPUSET_SETAFFINITY)
>
> 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.frhttps://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
>
> --
> AndrÃ© Maroneze
> Researcher/Engineer CEA/LIST
> Software Reliability and Security Laboratory
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180712/aa07f1ce/attachment.html>

Frama-C-discuss mailing list archives

[Frama-c-discuss] Casting to a generic function pointer