--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on November 2010 ---
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