--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on July 2018 ---
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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180705/1036dad2/attachment.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/20180705/1036dad2/attachment.bin>