--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on June 2017 ---
(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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170602/bfd98283/attachment-0001.html> -------------- 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/bfd98283/attachment-0001.bin>