Frama-C-discuss mailing list archives

mattator at gmail.com (Matt) · Fri, 2 Jun 2017 18:21:23 +0200

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

Frama-C-discuss mailing list archives

[Frama-c-discuss] Support LLVM database "compile_commands.json"