Skip to content
Snippets Groups Projects
Commit 06d3689f authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

update README

parent ec9af29a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 70 additions and 0 deletions
README → README.md
+ 70
− 0
View file @ 06d3689f
/**************************************************************************/
/* */
/* This file is part of Frama-Clang */
/* */
/* Copyright (C) 2012-2020 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
/* you can redistribute it and/or modify it under the terms of the GNU */
/* Lesser General Public License as published by the Free Software */
/* Foundation, version 2.1. */
/* */
/* It is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
/* GNU Lesser General Public License for more details. */
/* */
/* See the GNU Lesser General Public License version 2.1 */
/* for more details (enclosed in the file LICENSE). */
/* */
/**************************************************************************/
This archive contains Frama-Clang, a Frama-C plug-in for parsing C++ files, 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 based on Clang, the C/C++/Objective-C front-end of the LLVM compiler
infrastructure. infrastructure.
== Installation == # Installation
The following packages must be present on the system in order to compile The following packages must be present on the system in order to compile
Frama-Clang Frama-Clang
- llvm and clang (version 6.x, 7.x or 8.x) - llvm and clang (version >= 6.x, preferably 9 or 10)
- For Ubuntu and Debian, install the following packages: - For Ubuntu and Debian, install the following packages:
libclang-<version>-dev clang-<version> libclang-<version>-dev clang-<version>
(with their dependencies). (with their dependencies).
...@@ -38,51 +16,55 @@ Frama-Clang ...@@ -38,51 +16,55 @@ Frama-Clang
(packages such as llvm<version>, llvm<version>-devel and ncurses-devel (packages such as llvm<version>, llvm<version>-devel and ncurses-devel
should be included in their dependencies; otherwise, you might need to should be included in their dependencies; otherwise, you might need to
install them as well) install them as well)
- Frama-C version Silicon-20161101 - Frama-C version 21.x Scandium
- OCaml version 4.02.3 or higher - OCaml version 4.05 or higher
(i.e. the same version than the one that was used to compile Frama-C). (i.e. the same version than the one that was used to compile Frama-C).
- The corresponding camlp4 version - The corresponding camlp5 version
The front-end can then be compiled with the traditional commands The front-end can then be compiled with the traditional commands
```
./configure ./configure
make make
make install make install
```
Depending on the exact configuration of the system, Depending on the exact configuration of the system,
the last step might require administrator rights. See ./configure --help the last step might require administrator rights. See `./configure --help`
for possible customization of the configuration stage. for possible customization of the configuration stage.
== Usage == # Usage
Once installed, Frama-Clang will be automatically called by Frama-C's kernel Once installed, Frama-Clang will be automatically called by Frama-C's kernel
whenever a C++ source file is encountered. More precisely, files ending 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 `.cpp`, `.C`, `.cxx`, `.c++` or `.cc` will be treated as C++ files.
with .ii will be considered as already pre-processed C++ files. Files ending with `.ii` will be considered as already pre-processed C++ files.
Options of the plug-in are the following. Options of the plug-in are the following.
- -cxx-demangling-full tells Frama-C to display C++ global - `-cxx-demangling-full` tells Frama-C to display C++ global
identifiers with their fully-qualified name (e.g. ::A::x) identifiers with their fully-qualified name (e.g. `::A::x`)
- -cxx-demangling-short tells Frama-C to display global - `-cxx-demangling-short` tells Frama-C to display global
C++ identifiers with their unqualified name (e.g. x) C++ identifiers with their unqualified name (e.g. `x`)
- -cxx-keep-mangling tells Frama-C to display global C++ - `-cxx-keep-mangling` tells Frama-C to display global C++
identifiers with the name they have in the C translation (e.g. identifiers with the name they have in the C translation (e.g.
_Z1A1x, that allows to distinguish between overloaded symbols. `_Z1A1x`, that allows to distinguish between overloaded symbols.
This mangled name is computed from the fully-qualified C++ name This mangled name is computed from the fully-qualified C++ name
according to the rules described in the Itanium C++ ABI. according to the rules described in the Itanium C++ ABI. Pretty-printing
- -cxx-cstdlib-path <path> specifies where to look for standard the AST with this option should result in compilable C code.
- `-cxx-cstdlib-path <path>` specifies where to look for standard
C library headers (default is the path to Frama-C's headers) C library headers (default is the path to Frama-C's headers)
- -cxx-c++stdlib-path <path> specifies where to look for - `-cxx-c++stdlib-path <path>` specifies where to look for
standard C++ library headers (default is the path to Frama-Clang headers, standard C++ library headers (default is the path to Frama-Clang headers,
which are very incomplete) which are very incomplete)
- -cxx-nostdinc do not include in the search paths - `-cxx-nostdinc` do not include in the search paths
Frama-C's C/C++ standard headers location Frama-C's C/C++ standard headers location (i.e. rely on the system's headers)
- -cxx-clang-command <cmd> allows to change the name of the - `-cxx-clang-command <cmd>` allows changing the name of the
command that launches clang and its plugin that outputs the intermediate AST. 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 This should only be needed if the front-end as a whole has not been installed
properly. properly.
In addition, any command-line option taking a function name as argument (e.g. In addition, any command-line option taking a function name as
-main, -slevel-function, ...) will accept a fully qualified C++ name (provided argument (e.g. `-main`, `-eva-slevel-function`, ...) will accept a
it refers to an existing function in the code under analysis of course). Note fully qualified C++ name (provided it refers to an existing function
however that it is currently not possible to distinguish between overloaded in the code under analysis of course). Note however that it is
functions using this mechanism. currently not possible to distinguish between overloaded functions
using this mechanism.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment