--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] termination



I'm trying to prove this contract holds (using Frama-C+Jessie) but can't find any annotation to make it work. Any ideas?

/*@
  @ terminates c>0;
  @ assigns \nothing;
  @*/
void f (int c) {
  /*@
    @ loop assigns \nothing;
    @*/
  while(!c) {
  }
  return;
}