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] problem with \old()

  • Subject: [Frama-c-discuss] problem with \old()
  • From: der.herr at hofr.at (Nicholas Mc Guire)
  • Date: Tue, 9 Nov 2010 16:14:07 +0100
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