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] Support LLVM database "compile_commands.json"


  • Subject: [Frama-c-discuss] Support LLVM database "compile_commands.json"
  • From: mattator at gmail.com (Matt)
  • Date: Fri, 2 Jun 2017 18:21:23 +0200
  • In-reply-to: <daaca234-14df-b09f-50ab-bc339c561199@cea.fr>
  • References: <CADHp1NwbeCmzOVdJC6hsbz8CyyoGXUctkQQD=L8YSOyOM=ZReA@mail.gmail.com> <CA+yPOVhS9e02cWYVCtZyKymjBQFcZMOoLK5O5ic5rtk4RRT=uQ@mail.gmail.com> <CADHp1Nyd7BNtVMmzPzjEaYrE7e6-JpYfuPCzu2ZZ=-mBPXu=+A@mail.gmail.com> <46842_1496418150_59318765_46842_7803_2_65660f0f-2295-8665-b624-b24f3360f6f8@cea.fr> <daaca234-14df-b09f-50ab-bc339c561199@cea.fr>

first of all thanks for your help. I did try to look into it but
couldn't come up with a solution yet.
I wanted to try the brand new frama-c but it's not on opam yet  (EDIT:
looks ok now https://github.com/ocaml/opam-repository/pull/9379) and
building from source fails on ubuntu for the same reason as
https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2017-January/005200.html
. Not sure how to patch that as I am not familiar with ocaml (yet).

As you discovered gcc7 should work if you compile your own libmpack-c
until they tag a release. I don't use it though.


The result of compiling https://github.com/teto/neovim/tree/framac
(neovim-dev + one commit to bypass a framac error) was compiled with:
gcc --version
gcc (Ubuntu 6.3.0-12ubuntu2) 6.3.0 20170406

and should be available publicly at
https://www.dropbox.com/s/rz7zqgpfdk17u4e/build.tar.gz?dl=0 (it's my
"neovim/build" folder, ~250Mo) . If you have no dropbox account, click
on the "small/hidden" link to skip the dropbox popup asking for
registration.

I launch frama-c via the script ./frama.sh at
https://github.com/teto/neovim/tree/framac . something akin to
"./frama.sh -verbose=40 -kernel-verbose=40".

I have some time to investigate problems within my reach/help with
adding it to the case studies. First I would like to understand the
high level problem here:
the files are already processed so how come the source uses 2
different definitions of an integer ? Is it a problem with the neovim
preprocessing options ?

Best regards and once again thanks for your time.

Matt

2017-06-02 17:48 GMT+02:00 Andre Maroneze <Andre.OLIVEIRAMARONEZE at cea.fr>:
> (sorry, the correct URL is
> https://github.com/Frama-C/open-source-case-studies)
>
>
> On 02/06/17 17:38, Andre Maroneze wrote:
>
> Could you please provide the .i files for download somewhere?
>
> I tried running the commands you described, and I had two issues:
>
> 1. GCC 7 has a new warning about implicit fallthrough, which was triggered
> with -Werror in one of the dependencies of neovim (msgpack), so I had to
> find out about how to avoid it (I'm not familiar with cmake);
> 2. After solving the first issue, I realized that only .o files were being
> saved in the directory build/src/nvim/CMakeFiles/nvim.dir. I do have .i
> files in build/src/nvim/auto, but trying to parse everything at once leads
> to other errors (e.g. macro FUNC_ATTR_ALWAYS_INLINE not being defined). So I
> assume I'm doing it wrong, or something changed in my version of GCC.
>
> Anyway, having the list of preprocessed files would help reproduce the
> errors. Ideally, if we manage to parse it and obtain interesting results, we
> could put it in the Frama-C repository for open source case studies
> (https://git.frama-c.com/frama-c/open-source-case-studies).
>
>
> On 01/06/17 12:18, Matt wrote:
>
> Syntactic metrics are not exactly the main target of Frama-C. Are you
> planning to use EVA (which looks like a major endeavor on neovim)
> afterwards?
>
> I am mostly trying to get a feeling for formal methods. Cyclomatic
> complexity seemed like an easy first step before trying to use ACSL.
>
> As for the rest, I found out that with gcc>=4.6 you can use
> -save-temps=obj to save the intermediate files in their own folder. To
> sum up.
> ==
> cd neovim
> mkdir build
> rm -rf CMakeFiles CMakeCache.txt
> CFLAGS=" -save-temps=obj" cmake .. -DMIN_LOG_LEVEL=0
> -DCMAKE_BUILD_TYPE=Debug -DCMAKE_INSTALL_PREFIX=$PWD/root
> make
> frama-c $(find build/src/nvim/CMakeFiles/nvim.dir -type f -iname '*.i')
> ==
>
> So far I am trying to get around the following error. The paths given
> at the end of the log are not really helpful. I'll try to deal with it
> but any hint is welcome.
> /usr/include/x86_64-linux-gnu/bits/byteswap.h:47:[kernel] warning:
> Calling undeclared function __builtin_bswap32. Old style K&R code?
> /usr/include/x86_64-linux-gnu/bits/byteswap.h:111:[kernel] warning:
> Calling undeclared function __builtin_bswap64. Old style K&R code?
> [kernel] user error: Incompatible declaration for libuv_process_spawn:
>                       Definitions of type LibuvProcess are not
> isomorphic. Reason follows:
>                       Definitions of struct libuv_process are not
> isomorphic. Reason follows:
>                       Definitions of type uv_process_t are not
> isomorphic. Reason follows:
>                       Definitions of struct uv_process_s are not
> isomorphic. Reason follows:
>                       Definitions of type int64_t are not isomorphic.
> Reason follows:
>                       different integer types long long and long
>                       struct uv_process_s {
>                          void *data ;
>                          uv_loop_t *loop ;
>                          uv_handle_type type ;
>                          void (*close_cb)(uv_handle_t *handle) ;
>                          void *handle_queue[2] ;
>                          union __anonunion_u_102 u ;
> <-------------- this field differ
>                          uv_handle_t *next_closing ;
>                          unsigned int flags ;
>                          void (*exit_cb)(uv_process_t *, int64_t
> exit_status, int term_signal) ;
>                          int pid ;
>                          void *queue[2] ;
>                          int status ;
>                       };
>                       struct uv_process_s {
>                          void *data ;
>                          uv_loop_t *loop ;
>                          uv_handle_type type ;
>                          void (*close_cb)(uv_handle_t *handle) ;
>                          void *handle_queue[2] ;
>                          union __anonunion_u_98 u ;
> <-------------- this field differ
>                          uv_handle_t *next_closing ;
>                          unsigned int flags ;
>                          void (*exit_cb)(uv_process_t *, int64_t
> exit_status, int term_signal) ;
>                          int pid ;
>                          void *queue[2] ;
>                          int status ;
>                       };
>
>                       First declaration was at
> build/include/event/libuv_process.h.generated.h:6
>                       Current declaration is at
> build/include/event/libuv_process.h.generated.h:6
>
> Cheers
> Matt
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
>
> --
> André Maroneze
> Ingénieur-chercheur CEA/LIST
> Laboratoire Sûreté et Sécurité des Logiciels
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss