Skip to content

Commit c7b904b

Browse files
author
Matthieu Lemerre
committed
Add quickstart tutorial
1 parent 4453056 commit c7b904b

File tree

2 files changed

+380
-1
lines changed

2 files changed

+380
-1
lines changed

‎assets/codexoutputs/quickstart_c.html

Lines changed: 332 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,332 @@
1+
2+
<!DOCTYPE HTML>
3+
<html lang="en">
4+
5+
<head>
6+
<script src="https://ajax.googleapis.com/ajax/libs/jquery/1.12.4/jquery.min.js"></script>
7+
<script type='text/javascript'>
8+
clicked = [];
9+
10+
$(document).ready(function () {
11+
12+
$(".expnest").mouseup(function () {
13+
$(this).css({"background-color": $(this).css("background-color"), "color": "black"});
14+
$("#eidinfo" + $(this).attr("data-eid")).show();
15+
clicked.push($(this));
16+
});
17+
18+
$(".expnest").hover(
19+
function () {
20+
if (clicked.length == 0) {
21+
$(this).css({"background-color": $(this).css("background-color"), "color": "black"});
22+
$("#eidinfo" + $(this).attr("data-eid")).show();
23+
}
24+
},
25+
function () {
26+
if (clicked.length == 0) {
27+
$(this).removeAttr('style');
28+
$("#eidinfo" + $(this).attr("data-eid")).hide();
29+
}
30+
});
31+
32+
$(".code-container").mousedown(function (e) {
33+
if ((e.offsetX <= e.target.clientWidth && e.offsetY <= e.target.clientHeight) ||
34+
(e.target.clientWidth == 0 && e.target.clientHeight == 0)) {
35+
clicked.forEach(c => {c.removeAttr('style'); $("#eidinfo" + c.attr("data-eid")).hide();});
36+
clicked = [];
37+
}
38+
});
39+
40+
});
41+
</script>
42+
<style>
43+
44+
.def {
45+
display: none;
46+
}
47+
48+
.expnest:hover+.expinfo>.def {
49+
display: inline-block;
50+
}
51+
52+
.expinfo {
53+
border: 1px solid black;
54+
border-radius: 12px;
55+
}
56+
57+
.expinfo>.eidinfo {
58+
display: none;
59+
}
60+
61+
.expnest0:hover {
62+
background-color: #DDFFD6;
63+
color: #000000;
64+
}
65+
66+
.expnest1:hover {
67+
background-color: #FFC2C2;
68+
color: #000000;
69+
}
70+
71+
.expnest2:hover {
72+
background-color: #ADF8FF;
73+
color: #000000;
74+
}
75+
76+
.expnest3:hover {
77+
background-color: #FEFFD6;
78+
color: #000000;
79+
}
80+
81+
.expnest4:hover {
82+
background-color: #DCD6FF;
83+
color: #000000;
84+
}
85+
86+
.expnest5:hover {
87+
background-color: #FFE3C2;
88+
color: #000000;
89+
}
90+
91+
.expnest6:hover {
92+
background-color: #C2D9FF;
93+
color: #000000;
94+
}
95+
96+
.expnest7:hover {
97+
background-color: #F9C8E0;
98+
color: #000000;
99+
}
100+
101+
.expnest8:hover {
102+
background-color: #DCD6FF;
103+
color: #000000;
104+
}
105+
106+
.expnest9:hover {
107+
background-color: #BDB2FF;
108+
color: #000000;
109+
}
110+
111+
.expnest10:hover {
112+
background-color: #FFECD6;
113+
color: #000000;
114+
}
115+
116+
.expnest11:hover {
117+
background-color: #FFD6A5;
118+
color: #000000;
119+
}
120+
121+
.expnest12:hover {
122+
background-color: #D6E6FF;
123+
color: #000000;
124+
}
125+
126+
.expnest13:hover {
127+
background-color: #A0C4FF;
128+
color: #000000;
129+
}
130+
131+
.expnest14:hover {
132+
background-color: #FBDAEB;
133+
color: #000000;
134+
}
135+
136+
.expnest15:hover {
137+
background-color: #F7B6D7;
138+
color: #000000;
139+
}
140+
141+
.expnest0 {
142+
background-color: #f0f0f0;
143+
}
144+
145+
.font-expnest0 {
146+
background-color: #DDFFD6;
147+
}
148+
149+
.font-expnest1 {
150+
background-color: #FFC2C2;
151+
}
152+
153+
.font-expnest2 {
154+
background-color: #ADF8FF;
155+
}
156+
157+
.font-expnest3 {
158+
background-color: #FEFFD6;
159+
}
160+
161+
.font-expnest4 {
162+
background-color: #DCD6FF;
163+
}
164+
165+
.font-expnest5 {
166+
background-color: #FFE3C2;
167+
}
168+
169+
.font-expnest6 {
170+
background-color: #C2D9FF;
171+
}
172+
173+
.font-expnest7 {
174+
background-color: #F9C8E0;
175+
}
176+
177+
.font-expnest8 {
178+
background-color: #DCD6FF;
179+
}
180+
181+
.font-expnest9 {
182+
background-color: #BDB2FF;
183+
}
184+
185+
.font-expnest10 {
186+
background-color: #FFECD6;
187+
}
188+
189+
.font-expnest11 {
190+
background-color: #FFD6A5;
191+
}
192+
193+
.font-expnest12 {
194+
background-color: #D6E6FF;
195+
}
196+
197+
.font-expnest13 {
198+
background-color: #A0C4FF;
199+
}
200+
201+
.font-expnest14 {
202+
background-color: #FBDAEB;
203+
}
204+
205+
.font-expnest15 {
206+
background-color: #F7B6D7;
207+
}
208+
209+
body {
210+
/* background-color: #001B2E; */
211+
}
212+
213+
.code-container {
214+
font-family: monospace;
215+
line-height: 1.5;
216+
color: /* #FFF8EB; */ #000000;
217+
overflow: auto;
218+
height: 92vh;
219+
}
220+
221+
.expinfo {
222+
/* background-color: #ADB6C4; */
223+
background-color: #eeeeee;
224+
padding: 10px;
225+
font-family: monospace;
226+
line-height: 1.5;
227+
color: #000;
228+
}
229+
230+
.column {
231+
float: left;
232+
overflow: auto;
233+
}
234+
235+
.row:after {
236+
content: "";
237+
display: table;
238+
clear: both;
239+
}
240+
241+
/* Syntax highlighting for C keywords */
242+
.code-container .keyword {
243+
color: #800080 /* 579dd6;
244+
font-weight: bold; */
245+
}
246+
247+
.code-container .type {
248+
color: #228b22;
249+
}
250+
251+
.code-container .vardecl {
252+
color: #a0522d;
253+
}
254+
255+
/* Syntax highlighting for C comments */
256+
.code-container .comment {
257+
color: #6a9955;
258+
/* green */
259+
font-style: italic;
260+
}
261+
262+
/* Syntax highlighting for C strings */
263+
.code-container .string {
264+
color: #ce9079;
265+
/* red */
266+
}
267+
268+
/* Syntax highlighting for C numbers */
269+
.code-container .number {
270+
color: #b5cea8;
271+
/* orange */
272+
}
273+
274+
/* Syntax highlighting for C preprocessor directives */
275+
.code-container .preprocessor {
276+
color: #c586c0;
277+
/* gray */
278+
}
279+
280+
/* Syntax highlighting for C functions */
281+
.code-container .function-name {
282+
color: #0000ff;
283+
}
284+
285+
.scrollbar::-webkit-scrollbar-track
286+
{
287+
border: 1px solid black;
288+
background-color: #FFF8EB;
289+
}
290+
291+
.scrollbar::-webkit-scrollbar
292+
{
293+
width: 10px;
294+
}
295+
296+
.scrollbar::-webkit-scrollbar-thumb
297+
{
298+
background-color: #ADB6C4;
299+
}
300+
</style>
301+
<meta http-equiv="content-type" content="text/html; charset=utf-8">
302+
<title>Frama-C/Codex Analysis results</title>
303+
</head>
304+
305+
<body>
306+
<div class="row">
307+
<pre class="scrollbar column code-container" style="width: 45%; margin: 0px;">
308+
/* Generated by Frama-C */
309+
<a name="vi-global-main"></a><span class="type"><span class="type"><span class="type">int</span> <span class="vardecl"><span class="vardecl"><a data-eid="0" href="#vi-global-main" class="expnest expnest0 function-name">main</a></span>(<span class="type"><span class="type">int</span> <span class="vardecl">i</span></span>)</span></span></span>
310+
{
311+
<span class="statement"><span class="type"><span class="type">int</span> <span class="vardecl">x</span></span> = <span data-eid="1" class="expnest expnest0"><span data-eid="2" class="expnest expnest0">i</span></span>;</span>
312+
<span class="keyword">if</span> (<span data-eid="3" class="expnest expnest0"><span data-eid="4" class="expnest expnest1"><span data-eid="5" class="expnest expnest1">i</span></span> &gt; <span data-eid="6" class="expnest expnest1">8</span></span>) <span class="statement"><span data-eid="7" class="expnest expnest0">x</span> = <span data-eid="8" class="expnest expnest0">8</span>;</span>
313+
<span class="keyword">return</span> <span data-eid="9" class="expnest expnest0"><span data-eid="10" class="expnest expnest0">x</span></span>;
314+
}
315+
316+
317+
</pre><div class="column expinfo" style="height: 92vh; width: 54%; padding: 0px;"><div class="scrollbar" style="padding: 10px; font-family: sans; background-color: #8C96A7; color: black; min-height: 5vh; max-height: 20vh; overflow: auto;">
318+
<div style="font-variant: small-caps">Unproved alarms:</div>
319+
<div style="font-variant: small-caps">Proved 0/0 alarms</div></div>
320+
<hr style="border: 1px solid black; margin: 0px;">
321+
<table style="width: 100%"> <tr> <th style="font-style: italic">/</th> <th>Name</th> <th>Type</th> <th>Value</th> </tr><tr class="font-expnest0 eidinfo" id="eidinfo1" style="display: none"><td>Expr</td> <td>i</td> <td>int</td> <td>[--..--]</td></tr>
322+
<tr class="font-expnest0 eidinfo" id="eidinfo2" style="display: none"><td>Lval</td> <td>i</td> <td>int</td></tr>
323+
<tr class="font-expnest0 eidinfo" id="eidinfo3" style="display: none"><td>Expr</td> <td>i > 8</td> <td>int</td> <td>{0; 1}</td></tr>
324+
<tr class="font-expnest1 eidinfo" id="eidinfo4" style="display: none"><td>Expr</td> <td>i</td> <td>int</td> <td>[--..--]</td></tr>
325+
<tr class="font-expnest1 eidinfo" id="eidinfo5" style="display: none"><td>Lval</td> <td>i</td> <td>int</td></tr>
326+
<tr class="font-expnest1 eidinfo" id="eidinfo6" style="display: none"><td>Expr</td> <td>8</td> <td>int</td> <td>{8}</td></tr>
327+
<tr class="font-expnest0 eidinfo" id="eidinfo7" style="display: none"><td>Lval</td> <td>x</td> <td>int</td></tr>
328+
<tr class="font-expnest0 eidinfo" id="eidinfo8" style="display: none"><td>Expr</td> <td>8</td> <td>int</td> <td>{8}</td></tr>
329+
<tr class="font-expnest0 eidinfo" id="eidinfo9" style="display: none"><td>Expr</td> <td>x</td> <td>int</td> <td>[-0x80000000..8]</td></tr>
330+
<tr class="font-expnest0 eidinfo" id="eidinfo10" style="display: none"><td>Lval</td> <td>x</td> <td>int</td></tr>
331+
<tr class="font-expnest0 eidinfo" id="eidinfo0" style="display: none"><td>Func</td> <td>main</td> <td>undefined ctype</td></tr>
332+
</table></div></body></html>

‎tutorials.md

Lines changed: 48 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,57 @@
22
title: Tutorials
33
layout: home
44
nav_order: 1
5+
sidebar: toc
56
---
67

8+
# List of tutorials
9+
{:.no_toc}
710

8-
## Tutorial: [Spatial Memory Safety with Dependent Types using Codex](/docs/tutorial_oopsla2024.pdf)
11+
* List replaced by toc
12+
{:toc}
13+
14+
# Quick start: verifying C code using Frama-C/Codex
15+
16+
1. Download the latest binary release of Frama-C/Codex at https://github.com/codex-semantics-library/codex/releases/
17+
2. Write a small C function in file `test.c`:
18+
```c
19+
int main(int i) { int x = i; if(i > 8) x = 8; return x; }
20+
```
21+
If GCC is not installed, use `test.i` instead of `test.c` (`.i` corresponds to already-preprocessed files).
22+
3. Launch the analysis and obtain a textual report of the analysis:
23+
```sh
24+
./frama_c_codex.exe -codex test.c -codex-exp-dump test.dump && cat test.dump
25+
```
26+
```
27+
test.c:1.26-27: `i' -> [--..--]
28+
test.c:1.32-37: `i > 8' -> {0; 1}
29+
test.c:1.32-33: `i' -> [--..--]
30+
test.c:1.53-54: `x' -> [-0x80000000..8]
31+
Unproved regular alarms:
32+
Unproved additional alarms:
33+
Proved 0/0 regular alarms
34+
Unproved 0 regular alarms and 0 additional alarms.
35+
Solved 0/0 user assertions, proved 0
36+
```
37+
If you are using Emacs' compilation-mode (probably works also in other editors), you can click on each expression and they will bring you to the location in the file.
38+
4. Obtain an HTML report of the analysis:
39+
```sh
40+
./frama_c_codex.exe -codex test.c -codex-html-dump test.html
41+
```
42+
<iframe src="{{ '/assets/codexoutputs/quickstart_c.html' | relative_url }}" width="100%" height="400px" frameborder="8" style="border:1px solid #000; border-radius:15px; box-shadow: 0 4px 8px rgba(0,0,0,0.3);"></iframe>
43+
5. That's all to get started! As there are no reported alarms, your code is memory-safe, free from division-by-zero errors, and free from others errors that Codex checks. The most useful options are:
44+
- `-codex` (launches Codex);
45+
- `-main` (selects the entry point of the analysis, if not `main`);
46+
- `-codex-exp-dump out.dump` (produces a textual dump of all expressions);
47+
- `-codex-html-dump out.html` (produces an HTML equivalent of the dump file);
48+
- `-codex-type-file a.typ` (uses TypedC specification, useful when
49+
analyzing functions independently, which is covered by the next
50+
tutorial)
51+
52+
Happy verification!
53+
54+
55+
# Tutorial: [Spatial Memory Safety using Codex and TypedC](/docs/tutorial_oopsla2024.pdf)
956

1057
This is the tutorial accompagnying the prototype of our [OOPSLA 2024
1158
research

0 commit comments

Comments
 (0)