package frama-clang
Install
Dune Dependency
Authors
Maintainers
Sources
md5=10709f16660d4c58a0923e3133b7290c
sha512=6b6358b01188c590e8aa5cfcb7a8f0876c5a3e56fd900167a98f573c42e0d15603757455fd2d8d80ad4129cb22920eb07f81e3e0638ebb963bbe10eda4cb7fb6
README.md.html
README.md
This archive contains Frama-Clang, a Frama-C plug-in for parsing C++ files, based on Clang, the C/C++/Objective-C front-end of the LLVM compiler infrastructure.
Installation
The following packages must be present on the system in order to compile Frama-Clang
llvm and clang (version >= 11)
For Ubuntu and Debian, install the following packages: libclang-
-dev clang- (with their dependencies). For Fedora, install the following packages: llvm
-static clang clang-devel (packages such as llvm , llvm -devel and ncurses-devel should be included in their dependencies; otherwise, you might need to install them as well)
Frama-C version 25.x Manganese
OCaml version 4.08.1 or higher (i.e. the same version than the one that was used to compile Frama-C).
The corresponding
camlp5
versionfor newer OCaml versions which do not include the
Genlex
module,camlp-streams
(available throughopam
, it should normally be installed together withcamlp5
if needed)
The front-end can then be compiled with the traditional commands
./configure
make
make install
Depending on the exact configuration of the system, the last step might require administrator rights. See ./configure --help
for possible customization of the configuration stage.
Usage
Once installed, Frama-Clang will be automatically called by Frama-C's kernel whenever a C++ source file is encountered. More precisely, files ending with .cpp
, .C
, .cxx
, .c++
or .cc
will be treated as C++ files. Files ending with .ii
will be considered as already pre-processed C++ files.
Options of the plug-in are the following.
-cxx-unmangling key
indicates what to do when outputting a C++ symbol name.key
can be one the following:help
: outputs a list of existingkey
with a short descriptionfully-qualified
: displays the fully qualified name (e.g.::A::x
)without-qualifier
: only display the unqualified name (e.g.x
)none
: do not any transformation, displays the name as it is stored in Frama-C's AST (e.g._Z1A1x
)
-cxx-parseable-output
indicates that the pretty-printed code resulting from the translation should be able to be parsed again by Frama-C. implies-cxx-unmangling none
-cxx-cstdlib-path <path>
specifies where to look for standard C library headers (default is the path to Frama-C's headers)-cxx-c++stdlib-path <path>
specifies where to look for standard C++ library headers (default is the path to Frama-Clang headers, which are very incomplete)-cxx-nostdinc
do not include in the search paths Frama-C's C/C++ standard headers location (i.e. rely on the system's headers)-cxx-clang-command <cmd>
allows changing the name of the command that launches clang and its plugin that outputs the intermediate AST. This should only be needed if the front-end as a whole has not been installed properly.
Older versions of the plug-in used specific options for unmangling. These are now obsolete:
-cxx-demangling-full
: use-cxx-unmangling fully-qualified
-cxx-demangling-short
: use-cxx-unmangling without-qualifier
-cxx-keep-mangling
: use-cxx-unmangling none
In addition, any command-line option taking a function name as argument (e.g. -main
, -eva-slevel-function
, ...) will accept a fully qualified C++ name (provided it refers to an existing function in the code under analysis of course). Note however that it is currently not possible to distinguish between overloaded functions using this mechanism.