--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on July 2018 ---
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 list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -- André Maroneze Researcher/Engineer CEA/LIST Software Reliability and Security Laboratory -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180706/4e765e94/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 3797 bytes Desc: S/MIME Cryptographic Signature URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180706/4e765e94/attachment-0001.bin>