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: Andre.OLIVEIRAMARONEZE at cea.fr (Andre Maroneze)
  • Date: Fri, 2 Jun 2017 17:38:14 +0200
  • In-reply-to: <CADHp1Nyd7BNtVMmzPzjEaYrE7e6-JpYfuPCzu2ZZ=-mBPXu=+A@mail.gmail.com>
  • References: <CADHp1NwbeCmzOVdJC6hsbz8CyyoGXUctkQQD=L8YSOyOM=ZReA@mail.gmail.com> <CA+yPOVhS9e02cWYVCtZyKymjBQFcZMOoLK5O5ic5rtk4RRT=uQ@mail.gmail.com> <CADHp1Nyd7BNtVMmzPzjEaYrE7e6-JpYfuPCzu2ZZ=-mBPXu=+A@mail.gmail.com>
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

-- 
André Maroneze
Ingénieur-chercheur CEA/LIST
Laboratoire Sûreté et Sécurité des Logiciels


-------------- 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/20170602/f8f88c08/attachment.bin>