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: Thu, 1 Jun 2017 12:18:45 +0200
  • In-reply-to: <CA+yPOVhS9e02cWYVCtZyKymjBQFcZMOoLK5O5ic5rtk4RRT=uQ@mail.gmail.com>
  • References: <CADHp1NwbeCmzOVdJC6hsbz8CyyoGXUctkQQD=L8YSOyOM=ZReA@mail.gmail.com> <CA+yPOVhS9e02cWYVCtZyKymjBQFcZMOoLK5O5ic5rtk4RRT=uQ@mail.gmail.com>
> 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