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
---
layout: post
author: Pascal Cuoq
date: 2010-09-30 12:52 +0200
categories: skein value
format: xhtml
title: "Progress of the value analysis tutorial"
summary:
---
{% raw %}
<p><a href="http://frama-c.com/download/value-analysis-Boron-20100401.pdf" hreflang="en">Boron's value analysis manual</a> has the beginning of a captivating tutorial and I figure that the suspense must be unbearable. I on the other hand already know how it ends. But I'm not telling yet. Neener-neener! Okay maybe later on this blog.</p>
<p>The new manual (with an expanded tutorial) will be released at the same time as Frama-C version Carbon which is not immediately for various technical reasons. The new version will have some amazing performance improvements but the Boron version is good enough for one of the steps that comes after the current tutorial ends:</p>
<blockquote><p><strong>Generalizing to arbitrary numbers of Update calls</strong></p>
<p>
As an exercise try to verify that there cannot be a run-time error
when hashing arbitrary contents by calling <code>Update(... 80)</code> an arbitrary number of times
between <code>Init</code> and <code>Final</code>. The general strategy
is to modify the C analysis context we have already written in a way
such that it is evident that it captures all such sequences of calls
and also in a way such that launched with adequate options
the value analysis does not emit any warning.</p>
<p>
The latter condition is harder than the former.
Observing results (with the GUI or observation functions
described in section 8.3) can help iterate towards
a solution. Be creative.</p>
</blockquote>
<p>Solution(s) in a few days.</p>
<p>Note: if you try the tutorial for the first time or on a new computer you may also appreciate this new paragraph in the documentation:</p>
<blockquote><p>Some compilation plaforms' headers define the names <code>memset</code>
and <code>memcpy</code> in a way that make it impossible to provide
your own implementation for these functions. If this happens for
yours you can try placing your own header in the analysis directory
under the name <code>string.h</code></p>
<pre><code>
typedef unsigned int size_t;
void* memcpy(void* region1 const void* region2 size_t n);
void* memset (void* dest int val size_t len);
</code></pre>
</blockquote> <p><a href="http://frama-c.com/download/value-analysis-Boron-20100401.pdf" hreflang="en">Boron's value analysis manual</a> has the beginning of a captivating tutorial and I figure that the suspense must be unbearable. I on the other hand already know how it ends. But I'm not telling yet. Neener-neener! Okay maybe later on this blog.</p>
<p>The new manual (with an expanded tutorial) will be released at the same time as Frama-C version Carbon which is not immediately for various technical reasons. The new version will have some amazing performance improvements but the Boron version is good enough for one of the steps that comes after the current tutorial ends:</p>
<blockquote><p><strong>Generalizing to arbitrary numbers of Update calls</strong></p>
<p>
As an exercise try to verify that there cannot be a run-time error
when hashing arbitrary contents by calling <code>Update(... 80)</code> an arbitrary number of times
between <code>Init</code> and <code>Final</code>. The general strategy
is to modify the C analysis context we have already written in a way
such that it is evident that it captures all such sequences of calls
and also in a way such that launched with adequate options
the value analysis does not emit any warning.</p>
<p>
The latter condition is harder than the former.
Observing results (with the GUI or observation functions
described in section 8.3) can help iterate towards
a solution. Be creative.</p>
</blockquote>
<p>Solution(s) in a few days.</p>
<p>Note: if you try the tutorial for the first time or on a new computer you may also appreciate this new paragraph in the documentation:</p>
<blockquote><p>Some compilation plaforms' headers define the names <code>memset</code>
and <code>memcpy</code> in a way that make it impossible to provide
your own implementation for these functions. If this happens for
yours you can try placing your own header in the analysis directory
under the name <code>string.h</code></p>
<pre><code>
typedef unsigned int size_t;
void* memcpy(void* region1 const void* region2 size_t n);
void* memset (void* dest int val size_t len);
</code></pre>
</blockquote>
{% endraw %}