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

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>