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
- Follow-Ups:
- [Frama-c-discuss] Support LLVM database "compile_commands.json"
- From: Andre.OLIVEIRAMARONEZE at cea.fr (Andre Maroneze)
- [Frama-c-discuss] Support LLVM database "compile_commands.json"
- Next by Date: [Frama-c-discuss] Support LLVM database "compile_commands.json"
- Next by thread: [Frama-c-discuss] Support LLVM database "compile_commands.json"
- Index(es):