--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on June 2017 ---
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