Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Casting to a generic function pointer

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>