Newer
Older
1
2
3
4
5
6
7
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
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
---
css: documentation
layout: default
title: Documentation - Frama-C
---
<body class="page-template page-template-page-documentation page-template-page-documentation-php page page-id-20 nonTouch">
<div id="wrapper" class="hfeed">
{% include headers.html header=4 %}
<div id="container" class="mainContainer">
<div class="pageDocumentation pages">
<div class="bgTextbig">
Documentation
</div>
<div class="wrap">
<h1 class="pageTitle">Documentation</h1>
<div class="pageBanner" style=
"background-image:url('https://framac.s3.amazonaws.com/production/uploads/2017/07/banner.jpg');background-size:cover;">
<p>All the documentation<br>
you need !</p>
</div>
<div class="docListwrap">
<section>
<div class="docListTitle">
<span>PLUG-INS</span>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Link Test"><span>Link Test</span></h4>
<p>This is a test to see if HTTP link is accepted instead of PDF</p><span class="docReadMore">Read
More</span><a class="linkReadmore" href="link-test/index.html"></a> <a class="btnPdfDownload" target="_blank"
href="http://www.dummies.com/"><i class="icon-download-arrow"></i></a>
</div>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Studia"><span>Studia</span></h4>
<p>Studia helps with EVA case studies on the GUI.</p><a class="btnPdfDownload" target="_blank" href=
"https://framac.s3.amazonaws.com/production/uploads/2017/10/user-manual-Phosphorus-20170501.pdf"><i class=
"icon-download-arrow"></i></a>
</div>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="WP"><span>WP</span></h4>
<p>Deductive proofs of ACSL contracts</p><span class="docReadMore">Read More</span><a class="linkReadmore" href=
"wp/index.html"></a> <a class="btnPdfDownload" target="_blank" href=
"https://framac.s3.amazonaws.com/production/uploads/2017/10/wp-manual-Phosphorus-20170501.pdf"><i class=
"icon-download-arrow"></i></a>
</div>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="E-ACSL"><span>E-ACSL</span></h4>
<p>Runtime Verification Tool</p><span class="docReadMore">Read More</span><a class="linkReadmore" href=
"e-acsl/index.html"></a> <a class="btnPdfDownload" target="_blank" href=
"https://framac.s3.amazonaws.com/production/uploads/2017/10/e-acsl-manual.pdf"><i class=
"icon-download-arrow"></i></a>
</div>
</div>
<div 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><span class="docReadMore">Read
More</span><a class="linkReadmore" href="pathcrawler/index.html"></a> <a class="btnPdfDownload" target="_blank"
href="http://www.google.fr"><i class="icon-download-arrow"></i></a>
</div>
</div>
<div 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><span class=
"docReadMore">Read More</span><a class="linkReadmore" href="mthread/index.html"></a> <a class="btnPdfDownload"
target="_blank" href=
"https://framac.s3.amazonaws.com/production/uploads/2017/10/frama-c-mthread-manual.pdf"><i class=
"icon-download-arrow"></i></a>
</div>
</div>
<div 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><span class="docReadMore">Read
More</span><a class="linkReadmore" href="metrics-calculation/index.html"></a> <a class="btnPdfDownload" target=
"_blank" href="https://framac.s3.amazonaws.com/production/uploads/2017/10/frama-c-metrics-manual.pdf"><i class=
"icon-download-arrow"></i></a>
</div>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Variadic"><span>Variadic</span></h4>
<p>Variadic simplifies variadic functions for other plug-ins.</p><span class="docReadMore">Read
More</span><a class="linkReadmore" href="variadic/index.html"></a>
</div>
</div>
<div 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><span class="docReadMore">Read
More</span><a class="linkReadmore" href="/html/documentation/eva.html"></a> <a class="btnPdfDownload" target="_blank" href=
"https://framac.s3.amazonaws.com/production/uploads/2017/08/Form10C.pdf"><i class="icon-download-arrow"></i></a>
</div>
</div>
</section>
<section>
<div class="docListTitle">
<span>ACSL (ANSI/ISO-C Specification Language)</span>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="ACSL Reference Manual"><span>ACSL Reference Manual</span></h4>
<p>Lorem Ipsum is simply dummy text of the printing and typesetting industry. Lorem Ipsum has been the industrys
standard dummy text ever since the 1500s, when an unknown printer took...</p><a class="btnPdfDownload" target=
"_blank" href="https://framac.s3.amazonaws.com/production/uploads/2017/08/download.pdf"><i class=
"icon-download-arrow"></i></a>
</div>
</div>
</section>
</div>
</div>
</div>
{% include footer.html %}
<div class="clear"></div>
</div>
</div>
</body>