--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on July 2018 ---
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 -mainmain > -verbose3-machdepgcc_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-pragmangx_alloc > -impact-print-no-val-alloc-returns-null > -- 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/20180704/71066d45/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/20180704/71066d45/attachment-0001.bin>