--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on July 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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>