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

[Frama-c-discuss] problem with \old()



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