--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on July 2018 ---
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>