frama-clang.md 5.18 KB
Newer Older
1
2
3
4
5
6
---
layout: plugin
title: Frama-Clang
description: C++ front-end to Frama-C, based on the clang compiler.
key: front
distrib_mode: free
7
manual_pdf: /download/frama-clang-manual.pdf
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
---

![Frama-Clang logo](/assets/img/plugins/frama-clang.png)

## Overview

Frama-Clang is a plugin that allows Frama-C to take as input C++ programs.
As its name implies, it is based on the [clang](http://clang.llvm.org)
compiler, the C/C++/Objective-C front-end of the [llvm](http://llvm.org)
platform. More precisely, Frama-Clang is composed of two parts: a clang plugin
(written in C++) that produces a simplified version of the clang AST, and a
normal Frama-C plugin that takes as input this simplified version and produces
a normal Frama-C AST.

When this plug-in is in use, Frama-C will consider all files ending in `.cpp`,
`.c++`, `.C`, `.cxx`, `.cc` and `.ii` (considered as already pre-processed)
as C++ files and give them to Frama-Clang to translate them into Frama-C's
internal representation (i.e. a plain C AST).
Once this has been done, any existing analyses can be launched as usual.

**Caveat:** Frama-Clang is currently in an early stage of development.
It is known to be incomplete and comes without any bug-freeness guarantees.
Moreover, the translation from C++ to C does not make any attempts to optimize
the resulting code for the back-end analyzers such as [Eva](eva.html) or
[WP](wp.html).
Further work is thus needed before Frama-Clang can claim to be a grown-up
plug-in. Feel free to [contact us](mailto:support@frama-c.com) if you're
interested in participating in its maturation.

Allan Blanchard's avatar
Allan Blanchard committed
37
38
39
40
41
## Further Reading

For more details about **Frama-Clang** plug-in,
please consult the [Frama-Clang manual]({{page.manual_pdf}}).

42
43
44
45
## Installation

### Download

Virgile Prevosto's avatar
Virgile Prevosto committed
46
47
The current version is 0.0.10. The frama-clang plugin can be downloaded
[here](/download/frama-clang-0.0.10.tar.gz).
48
49
50

### Requirements

Virgile Prevosto's avatar
Virgile Prevosto committed
51
52
- Frama-C 22.x Titanium
- OCaml 4.08.0 or higher, the same version as the one used to
53
compile Frama-C itself
Allan Blanchard's avatar
Allan Blanchard committed
54
- camlp5 (a version compatible with the OCaml version you're using)
Virgile Prevosto's avatar
Virgile Prevosto committed
55
- clang and libclang >= 6 (preferably >=9)
56
57
58

You also need llvm-config (llvm-config-x.y for Debian and Ubuntu users,
as explained in
Allan Blanchard's avatar
Allan Blanchard committed
59
[this bug report](https://bugs.launchpad.net/ubuntu/+source/llvm-3.1/+bug/991493)).
60
61
62
63

### Installation steps

```
Virgile Prevosto's avatar
Virgile Prevosto committed
64
65
tar xzvf frama-clang-0.0.10.tar.gz
cd frama-clang-0.0.10
66
67
68
69
70
71
72
73
74
75
./configure
make
make install
```

Depending on your Frama-C installation, this last step might
require root permissions.

### Changes

Virgile Prevosto's avatar
Virgile Prevosto committed
76
77
78
79
80
81
82
83
84
85
#### v0.0.10
- Compatibility with Frama-C 22.x Titanium
- Compatibility with Clang 11.0
- Don't generate code for implicit member functions and operators when they're
  not used.
- Don't generate code for templated member functions that are in fact never
  instantiated.
- header `<cstdbool>` undefines `bool`, `true` and `false` if they are macros
  (partial fix for https://git.frama-c.com/pub/frama-c/#2546)

Allan Blanchard's avatar
Allan Blanchard committed
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
#### v0.0.9

- Compatibility with Frama-C 21.x Scandium
- Compatibility with Clang 10.0
- Support for implicit initialization of POD objects.

#### v0.0.8

- Compatibility with Frama-C 20.0 Calcium
- Compatibility with Clang 9.0
- Proper conversion of ghost statements
- Support for <tt>\exit_status</tt> in ACSL++
- C++ part of the plug-in is now free from g++ warnings
- move away from camlp4 in favor of camlp5

101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
#### v0.0.7

- Compatibility with Frama-C 19.x Potassium
- Compatibility with Clang 6.0, 7.0 and 8.0
- Rewritten ACSL++ parser, providing easier extensibility
and maintenance
- Frama-Clang now has a
[manual]({{page.manual_pdf}})
- Improved support of STL
- Preliminary support for lambdas
- Improved support of template instantiations

#### v0.0.6

- Compatibility with Frama-C 17 Chlorine

#### v0.0.5

- Compatibility with Clang/LLVM as packaged by Debian/Ubuntu

#### v0.0.4

- Compatibility with Frama-C 16 Sulfur
- Compatibility with Clang/LLVM 5.0.0
- Improved translation for `const`-qualified objects
- Fixes translation of implicit functions for classes with
virtual inheritance

#### v0.0.3

- Compatibility with Frama-C 15 Phosphorus
- Improved handling of constructors and destructors for local
variables

#### v0.0.2

- Compatibility with Frama-C 14 Silicon
- Adding compatibility with Clang/LLVM 3.9.0 and 4.0.0
- Various fixes in support of virtual inheritance and
templates
- Better support for parsing GNU STL headers

#### v0.0.1

- Initial release

### Previous versions

Virgile Prevosto's avatar
Virgile Prevosto committed
149
150
151
- [0.0.9](/download/frama-clang-0.0.9.tar.gz)
compatible with Frama-C 21.0
- [0.0.8](/download/frama-clang-0.0.8.tar.gz)
Allan Blanchard's avatar
Allan Blanchard committed
152
153
154
compatible with Frama-C 20.0
- [0.0.7](/download/frama-clang-0.0.7.tar.gz)
compatible with Frama-C 19.x
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
- [0.0.6](/download/frama-clang-0.0.6.tar.gz)
compatible with Frama-C 17.0
- [0.0.5](/download/frama-clang-0.0.5.tar.gz)
compatible with Frama-C Sulfur-20171101
- [0.0.5](/download/frama-clang-0.0.4.tar.gz)
compatible with Frama-C Sulfur-20171101
- [0.0.3](/download/frama-clang-0.0.3.tar.gz)
compatible with Frama-C Phosphorus-20170501
- [0.0.2](/download/frama-clang-0.0.2.tar.gz)
compatible with Frama-C Silicon-20161101
- [0.0.1](/download/frama-clang-0.0.1.tar.gz)
compatible with Frama-C Aluminium-20160502

<p style="font-size: .8em"><a name="credit" id="credit"></a> The
llvm wyvern logo is <a href="http://llvm.org/Logo.html">© Apple,
inc</a>