--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on July 2018 ---
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. On Wed, Jul 4, 2018 at 7:02 PM, Andre Maroneze < Andre.OLIVEIRAMARONEZE at cea.fr> wrote: > I was not able to reproduce the warning, unless I explicitly add > `-no-frama-c-stdlib` to the command line. I tried downloading the same > version of nginx just in case, but there are several parsing issues > (missing includes from external libraries) which require some patches > before the analysis can be run. Therefore I assume I do not have the exact > same source code that you are using, which might explain why I failed to > reproduce it. > > The cause may be an issue with the source list, or with mixing Frama-C's > libc and the system's (for instance, you use `-I/usr/include/openssl`, > which is prone to issues, since it may end up including several files from > your system's libc, which are likely to be incompatible with Frama-C's > libc). For some reason, it is possible that Frama-C is not including its > own libc, thus the warning about the lack of specification for strlen. It > could even be somehow related to the preprocessor used. > > Note that, since Frama-C Chlorine, Eva builtins have their preconditions > taken into account, before the actual builtin code is run. This ensures > that all preconditions are always checked. In the end, it is possible that > the warning message will have no practical effect on your analysis, since > the builtin will execute anyway (as you can see by the message "builtin > Frama_C_strlen: invalid base: NULL"). > > As a side note, `-main main` is not necessary (it is set by default), > neither is `-cpp-frama-c-compliant` (it is set by default, and unless you > use `-cpp-command` and you have a non-gcc, non-Clang preprocessor, you > shouldn't need it). > > On 04/07/18 16:26, Divya Muthukumaran wrote: > > Here it is: > > frama-c -main main -verbose 3 -machdep gcc_x86_64 -c11 > -cpp-frama-c-compliant $SRCS -cpp-extra-args="-I. > -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/usr/include/openssl > -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 -D > NGX_HAVE_SCHED_SETAFFINITY -DSSL_CTRL_SET_TLSEXT_TICKET_KEY_CB" > -impact-pragma ngx_alloc -impact-print -no-val-alloc-returns-null > > > -- > 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/20180704/b912ba28/attachment.html>