frama-clang.md 5.57 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.11. The frama-clang plugin can be downloaded
[here](/download/frama-clang-0.0.11.tar.gz).
48

49
50
51
Frama-Clang also has its own public git [repository](https://git.frama-c.com/pub/frama-clang),
whose `master` branch should always be synchronized with Frama-C's own `master` branch.

52
53
### Requirements

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

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

### Installation steps

```
Virgile Prevosto's avatar
Virgile Prevosto committed
67
68
tar xzvf frama-clang-0.0.11.tar.gz
cd frama-clang-0.0.11
69
70
71
72
73
74
75
76
77
./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
78
79
80
81
82
#### v0.0.11
- Compatibility with Frama-C 23.x Vanadium
- Compatibility with Clang 12.0
- Slightly improved ACSL++ parsing
- Various bug fixes
83

Virgile Prevosto's avatar
Virgile Prevosto committed
84
85
86
87
88
89
90
91
92
93
#### 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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
#### 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

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
149
150
151
152
153
154
155
156
#### 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

157
158
- [0.0.10](/download/frama-clang-0.0.10.tar.gz)
compatible with Frama-C 22.0
Virgile Prevosto's avatar
Virgile Prevosto committed
159
160
161
- [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
162
163
164
compatible with Frama-C 20.0
- [0.0.7](/download/frama-clang-0.0.7.tar.gz)
compatible with Frama-C 19.x
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
- [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>