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

  • Subject: [Frama-c-discuss] beginners problem - pointer swap example
  • From: andi.platschek at gmail.com (andi)
  • Date: Mon, 08 Nov 2010 15:58:05 +0100
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