Frama-C-discuss mailing list archives

Andre.OLIVEIRAMARONEZE at cea.fr (Andre Maroneze) · Fri, 2 Jun 2017 17:48:20 +0200

(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>

Frama-C-discuss mailing list archives

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