Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] beginners problem - pointer swap example

Hello,

> I just started playing around with frama-c and I am going through the
> examples in the mini-tutorial.

I gather that you mean the ACSL mini-tutorial at
http://frama-c.com/download/acsl-tutorial.pdf .

> So far I was able to run all the
> examples, but I am stuck at the complete specification of the pointer
> swap example.

A little bit of context: Frama-C is a C analysis framework. Different
analyses are implemented as plug-ins. Two prominent plug-ins are the
value analysis and Jessie, that both can be used for the verification
of ACSL properties. However, they work differently: they have
different strengths and weaknesses, and many annotations intended for
one cannot be proved with the other.

The ACSL tutorial explains ACSL, the annotation language, which exists
independently of what is currently implemented in Frama-C and what can
currently be verified using the value analysis or Jessie. The examples
in the beginning can be verified with Jessie, but not the most
difficult examples at the end (after chapter 6 or so). The value
analysis does even worse on the ACSL mini-tutorial examples.

The value analysis and Jessie are not the only plug-ins in Frama-C.
There are plug-ins that build upon the results of other plug-ins. The
value analysis was especially intended to have other analyses take
advantage of its results. The -users option is such a plug-in, and it
is in fact undocumented and unsupported (because it is not documented
in any of the manuals).
If -users was documented anywhere, it would be in the value analysis
manual, because it is one of the analyses derived from the value
analysis results. When you activate -users, this automatically
activates the value analysis. This is why you see some messages about
your annotations, but the messages are essentially that the value
analysis could not prove your annotations, which is normal.

If you are interested in verifying functional properties of the same
nature as you see in the ACSL tutorial, I recommend you now move to:

http://www.first.fraunhofer.de/owx_download/acsl-by-example-5_1_0.pdf

Unlike the ACSL mini-tutorial, it contains only examples that have
been tested with Jessie.

you can then (or alternately) move to :
http://frama-c.com/jessie_tutorial_index.html

If you want to know more about the value analysis, which basically is
more automatic, less powerful, and supports more low-level C
constructs than Jessie, read the "Tutorial" chapter in the value
analysis manual:
http://frama-c.com/download/frama-c-value-analysis.pdf and continue
with http://blog.frama-c.com/index.php?tag/value (read the posts from
bottom to top).

> So here is my code:
>
>> #include<stdio.h>
>>
>> /*@ requires \valid(p) && \valid(q);
>>     ensures *p<=*q;
>>     ensures (*p==\old(*p) && *q==\old(*q)) || (*p==\old(*q) &&
>> *q==\old(*p));
>> */
>> void max_ptr(int *p, int *q)
>> {
>>   if (*p > *q){
>>       int tmp = *p;
>>       *p = *q;
>>       *q = tmp;
>>    }
>> }
>>
>> int main (int argc, char **argv)
>> {
>>   int p = 55;
>>   int q = 6;
>>
>>   max_ptr (&p, &q);
>>   printf("p: %d, q: %d\n\n", p, q);
>>
>> return 0;
>> }

Actually, with this example you can use the value analysis because you
have provided a main() function. The value analysis is able to analyze
the program precisely (at the end      p ? {6; } and  q ? {55; }) with
the commandline:

frama-c -val ptr.c

Although it is precise for the values contained in the variables
during execution, it cannot tell you that the post-condition is
satisfied in this execution because it does not handle the \old
construct.

Jessie should allow you to prove that the post-condition is
intrinsically guaranteed by the function max_ptr as long as the
callers always respect the pre-condition. This is a much stronger
property than just checking the truth values of the annotations for
all executions from a provided main (which is what the value analysis
does).
To use Jessie on this example, comment out the #include <stdio.h> (I
told you that Jessie does not support all C constructs) and comment
out the main function: you don't need it, because you are going to
prove that max_ptr intrinsically satisfies its contract.

Once you have commented all this, and assuming you have all the tools
installed, type:

frama-c -jessie ptr.c

Clicking on one of the prover buttons, you may be able to obtain the
result as in the attached screenshot. This means that the function
max_ptr has been completely verified against its contract.

Best regards,

Pascal
-------------- next part --------------
A non-text attachment was scrubbed...
Name: jessie_ptr.png
Type: image/png
Size: 83506 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101108/4aac7910/attachment-0001.png>