Newer
Older
---
layout: default
css: plugin
title: Kernel & Plugins - Frama-C
---
<body class="page-template page-template-page-kernel_plugins page-template-page-kernel_plugins-php page page-id-16 nonTouch">
<div id="wrapper" class="hfeed">
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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
{% include headers.html header=2 %}
<div id="container" class="mainContainer">
<div class="tabs">
<div class="wrap">
<a class="active tabLink" href="kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
"/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
<div class="tabOptions">
<div class="pluginSearch">
<form class="searchForm" method="get" action="kernel-plugin.html" data-parsley-validate="">
<button type="submit" class="submit searchLink" title="Search"><i class="icon icon-search"></i></button>
<input type="text" name="plugin" placeholder="Search for the plugins here" data-parsley-required="">
<div class="error" id="top_search_error" style="display: none;" role="alert"></div>
</form><a class="btn" target="_blank" href=
"https://framac.s3.amazonaws.com/production/uploads/2017/08/frama-c-plugin-development-guide.pdf.pdf"><span>Write
Your Own Plugin</span></a>
</div>
</div>
</div>
</div>
<div class="pluginSliderWrapper">
<div class="pluginSwiper swiper-container">
<div class="swiper-wrapper">
<div class="swiper-slide" id="post_details" style="background-image: url(kernel-plugin.html);background-size:cover;">
<div>
<h3>WP<i class="icon-arrow-thin-rgt"></i></h3>
<p>Deductive proofs of ACSL contracts</p>
<p><a class="readMore" href="/html/documentation/wp.html">Read More</a></p>
</div>
</div>
<div class="swiper-slide" id="post_details" style="background-image: url(kernel-plugin.html);background-size:cover;">
<div>
<h3>E-ACSL<i class="icon-arrow-thin-rgt"></i></h3>
<p>Runtime Verification Tool</p>
<p><a class="readMore" href="/html/documentation/e-acsl.html">Read More</a></p>
</div>
</div>
<div class="swiper-slide" id="post_details" style=
"background-image: url(https://framac.s3.amazonaws.com/production/uploads/2017/08/eva2-2.jpg);background-size:cover;">
<div>
<h3>Evolved Value Analysis (EVA)<i class="icon-arrow-thin-rgt"></i></h3>
<p>Automatically computes variation domains for the variables of the program.</p>
<p><a class="readMore" href="/html/documentation/eva.html">Read More</a></p>
</div>
</div>
</div>
<div class="swiper-pagination"></div>
</div>
<div class="nextPrev">
<div class="swiper-button-prev"></div>
<div class="swiper-button-next"></div>
</div>
</div>
<div class="pagePlugin pages">
<div class="bgTextbig">
Plugin
</div>
<div class="wrap">
<div class="docListwrap">
<section>
<div class="docListTitle">
<span>Main analyzers</span>
</div><a role="link" href="/html/documentation/jessie.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Jessie"><span>Jessie</span></h4>
<p>A deductive verification plug-in.</p>
</div></a> <a role="link" href="/html/documentation/wp.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="WP"><span>WP</span></h4>
<p>Deductive proofs of ACSL contracts</p>
</div></a> <a role="link" href="/html/documentation/e-acsl.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="E-ACSL"><span>E-ACSL</span></h4>
<p>Runtime Verification Tool</p>
</div></a> <a role="link" href="/html/documentation/eva.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Evolved Value Analysis (EVA)"><span>Evolved Value Analysis (EVA)</span></h4>
<p>Automatically computes variation domains for the variables of the program.</p>
</div></a>
</section>
<section>
<div class="docListTitle">
<span>For test-case generation</span>
</div><a role="link" href="/html/documentation/pathcrawler.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="PathCrawler"><span>PathCrawler</span></h4>
<p>PathCrawler automatically finds test-case inputs to ensure coverage of a C function. It can be used for
structural unit testing, as a complement to static analysis or to study the...</p>
</div></a>
</section>
<section>
<div class="docListTitle">
<span>For concurrent programs</span>
</div><a role="link" href="/html/documentation/mthread.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Mthread"><span>Mthread</span></h4>
<p>Analyzes concurrent C programs, taking into account all possible thread interactions. Provides precise
information about shared variables, which mutex protects a part of the code, etc.</p>
</div></a>
</section>
<section>
<div class="docListTitle">
<span>For code transformation</span>
</div><a role="link" href="/html/documentation/semantic-constant-folding.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Semantic constant folding"><span>Semantic constant folding</span></h4>
<p>Makes use of the results of the EVA plug-in to replace, in the source code, the constant expressions by their
values.</p>
</div></a> <a role="link" href="/html/documentation/spare-code.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Spare code"><span>Spare code</span></h4>
<p>Removes "spare code", code that does not contribute to the final results of the program.</p>
</div></a> <a role="link" href="/html/documentation/variadic.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Variadic"><span>Variadic</span></h4>
<p>Variadic simplifies variadic functions for other plug-ins.</p>
</div></a>
</section>
<section>
<div class="docListTitle">
<span>For browsing unfamiliar code</span>
</div><a role="link" href="/html/documentation/studia.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Studia"><span>Studia</span></h4>
<p>Studia helps with EVA case studies on the GUI.</p>
</div></a> <a role="link" href="/html/documentation/metrics-calculation.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Metrics calculation"><span>Metrics calculation</span></h4>
<p>Allows the user to compute various metrics from the source code.</p>
</div></a> <a role="link" href="/html/documentation/sparecode.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Occurrence analysis plug-in"><span>Occurrence analysis plug-in</span></h4>
<p>Also provided as a simple example for new plug-in development, this plug-in allows the user to reach the
statements where a given variable is used.</p>
</div></a> <a role="link" href="/html/documentation/impact.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Impact analysis"><span>Impact analysis</span></h4>
<p>Highlights the locations in the source code that are impacted by a modification.</p>
</div></a> <a role="link" href="/html/documentation/scope.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Scope & Data-flow browsing"><span>Scope & Data-flow
browsing</span></h4>
<p>Allows the user to navigate the dataflow of the program, from definition to use or from use to definition.</p>
</div></a>
</section>
</div>
</div>
</div>
{% include footer.html %}
<div class="clear"></div>
</div>
</div>
</body>