--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on November 2010 ---
HI ! trying to run some simple examples from the tutorial/acsl-by-example but any of the examples that I tried to write up that include \old() give me "postcondition got status unknow" - other than that it seems that things are ok with the instalation. debian:~/examples# cat inc2.c /*@ requires \valid(p) ; ensures \old(*p) < *p ; */ void fun(int *p) { unsigned int t=*p; t++; *p=t; } void test(void){ unsigned int i=55; fun(&i); } debian:~/examples# frama-c -main test -users inc2.c [kernel] preprocessing with "gcc -C -E -I. inc2.c" [value] Analyzing a complete application starting at test [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization [value] computing for function fun <-test. Called from inc2.c:14. inc2.c:14:[value] Precondition of fun got status valid. inc2.c:10:[value] Function fun, behavior default: postcondition got status unknown [value] Recording results for fun [value] Done for function fun [value] Recording results for test [value] done for function test [users] ====== DISPLAYING USERS ====== test: fun ====== END OF USERS ========== explaination - pointers to docs - would be much appreciated. system ist Debian 5 - installation via godi (current defaults) frama-c 20100401#2 why 2.26#1 ocaml 3.11.2 alt-ergo 0.9.2r1 coq 8.2.1#4 thx! hofrat