--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on November 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



Hi, all

I just started playing around with frama-c and I am going through the 
examples in the mini-tutorial. So far I was able to run all the
examples, but I am stuck at the complete specification of the pointer 
swap example. 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;
> } 

I am running frama-c with this command: "frama-c -users max_ptr.c", and 
I always get:
> max_ptr.c:21:[value] Precondition of max_ptr got status valid.
> max_ptr.c:14:[value] Function max_ptr, behavior default: postcondition 
> got status unknown

I tested it on Boron-20100401 and Lithium-20081201 with the same result, 
and the same code without checking the pointers for the
old values works...

I am sure I am doing something very stupid, but I am not able to find 
out what, so I hope someone is able to help me :-)

thanks in advance,
Andi