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: Andre.OLIVEIRAMARONEZE at cea.fr (Andre Maroneze)
- Date: Fri, 2 Jun 2017 20:09:53 +0200
- In-reply-to: <CADHp1Ny5jonyCbpAuQgWHOycbi0j1koHUP8wu7Wrc4u2TpPT8A@mail.gmail.com>
- References: <CADHp1NwbeCmzOVdJC6hsbz8CyyoGXUctkQQD=L8YSOyOM=ZReA@mail.gmail.com> <CA+yPOVhS9e02cWYVCtZyKymjBQFcZMOoLK5O5ic5rtk4RRT=uQ@mail.gmail.com> <CADHp1Nyd7BNtVMmzPzjEaYrE7e6-JpYfuPCzu2ZZ=-mBPXu=+A@mail.gmail.com> <46842_1496418150_59318765_46842_7803_2_65660f0f-2295-8665-b624-b24f3360f6f8@cea.fr> <daaca234-14df-b09f-50ab-bc339c561199@cea.fr> <CADHp1Ny5jonyCbpAuQgWHOycbi0j1koHUP8wu7Wrc4u2TpPT8A@mail.gmail.com>
Thanks for the files! I have some good news and some bad news: the good news is, I was able to parse it. The bad news (for me at least), is that EVA could not go very far, due to a recursive call not far from the beginning of the program. This can be amended, but I don't hold much hope for a full static analysis on this kind of code, given the amount of dependencies, libraries which would have to be stubbed, etc. Still, it is good to know that we are at least able to parse it. First of all, let me take advantage of this moment to praise the new environment verifications added in Phosphorus, namely one that checks that the extended integer types defined in the C standard are consistent with those of the machdep currently used by Frama-C. These tests emit warnings such as: /usr/include/stdint.h:40:[kernel] warning: bad type 'long' (32 bits) for typedef 'int64_t'; check for mismatch between -machdep flag and headers used This was not present in the previous release, and I indeed had a type error similar (though not exactly the same) to the one you described when running Frama-C 14 - Silicon. The issue is that, by default, Frama-C assumes that the code is being compiled for x86-32, but the preprocessed files were produced by a 64-bit compiler. This generated mismatches between Frama-C's types and those in the files, which eventually led to inconsistent types later. The new release detects this inconsistency and warns about them, so simply adding "-machdep x86_64" to the command-line allowed me to parse everything. This does not solve everything, however: if you do so, there are still several dozens of messages of this type: /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? This is an unfortunate consequence of the fact that files preprocessed by GCC often include its builtins. However, Frama-C has a GCC-specific machdep, thus using "-machdep gcc_x86_64" (instead of "-machdep x86_64") allows such warnings to disappear. Note that there are still a few built-ins that are not supported by Frama-C, such as _Static_assert, __builtin_isnan, __builtin_isinf_sign, etc. Ideally, they should have a prototype and a minimal specification (e.g. if you want to run EVA, they need ACSL assigns clauses). However, it is possible that these functions are present in the code but not actually used during the analysis, so you may want to do it later, only for the functions actually called during execution. Also, you'll encounter several warnings related to variadic functions, such as: src/nvim/fileio.c:3852:[variadic] warning: Call to function function sprintf with non-static format argument: no specification will be generated. This is due to the fact that most calls use gettext, and therefore the strings are not static, so the Variadic plug-in (which automatically generates specifications for variadic functions) will not be able to do much. You may want to use option -variadic-no-translation to disable it and avoid the warnings, but note that some analyses might then become unsound. E.g., if you then run EVA on a program containing calls to sprintf, you may get a warning such as: [kernel] warning: Neither code nor specification for function sprintf, generating default assigns from the prototype This means that Frama-C did not find a specification for the function and created its own (since it is needed by EVA), but this generation is not guaranteed to be sound. Finally, I strongly recommend using the Frama-C save feature to store the result of parsing, for later reuse (either on the GUI, or by other analyses). There is a large amount of files to be parsed, and due to preprocessing, there are several (redundant) lines that further increase parsing time. To do it once and for all, you just need to do this: frama-c <kernel/parsing options, such as -machdep, etc.> <list of source files> -save parsed.sav frama-c -load parsed.sav <other analysis options, such as -val, -metrics, ...> or, to see the parsed result in the GUI: frama-c-gui -load parsed.sav Overall, though, if you intend to try a thorough analysis with EVA, first you'd have to remove/stub recursive calls, then stub calls to external library functions (e.g. from libuv ; such stubbing might be done via ACSL specifications), then consider issues related to concurrency/interrupts/signals, possibly consider how to model the environment (e.g. filesystem, network, user interaction, etc.)... If you just want to see how EVA works on an almost-ideal case (embedded software), I'd recommend case study debie1-e-free from the open-source-case-studies repository. You can easily modify the provided Makefile and obtain different analysis results, and try to add some ACSL specifications here and there and see how they impact the analysis. It's a small code base, but in my opinion a much better environment to "get a feeling about formal methods", without having to deal with several concurrent issues all at once. If you want a tutorial oriented towards functional specifications, based on deductive verification, I'd recommend ACSL by Example. Finally, there is a tutorial on the WP plug-in (deductive verification) on https://github.com/AllanBlanchard/tutoriel_wp/ (the original version is in French only, but it is being translated into English). On 02/06/17 18:21, Matt wrote: > 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 > -- André Maroneze Ingénieur-chercheur CEA/LIST Laboratoire Sûreté et Sécurité des Logiciels -------------- 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/a721ac18/attachment-0001.bin>
- Follow-Ups:
- [Frama-c-discuss] Support LLVM database "compile_commands.json"
- From: mattator at gmail.com (Matt)
- [Frama-c-discuss] Support LLVM database "compile_commands.json"
- References:
- [Frama-c-discuss] Support LLVM database "compile_commands.json"
- From: mattator at gmail.com (Matt)
- [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"
- From: mattator at gmail.com (Matt)
- [Frama-c-discuss] Support LLVM database "compile_commands.json"
- Prev by Date: [Frama-c-discuss] Support LLVM database "compile_commands.json"
- Next by Date: [Frama-c-discuss] Support LLVM database "compile_commands.json"
- Previous by thread: [Frama-c-discuss] Support LLVM database "compile_commands.json"
- Next by thread: [Frama-c-discuss] Support LLVM database "compile_commands.json"
- Index(es):