--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on September 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie - problem with an example



Hello,

I've got a question regarding a specific example I am working on.
Below you can see a simplified part of it, because it's part of a more
complex scene.
It should actually only show that data->b <= data->a and that both are
always positive.
Running it in Jessie (still in Lithium version, int-model exact) alt-ergo
can't prove that data->b is always positive.
Does maybe anyone have an idea why it is not possible to prove that? Because
I don't see a way for b to increase negatively.

Your help would be very much appreciated,
Thanks in advance,

Kerstin

-------------------------------
struct MyData
{
  int a;
  int b;
}; 

/*@ predicate is_positive(integer a) = (a >= 0);
 */
/*@ ensures is_positive(\result);
 */ 
int something() ; 

/*@ requires \valid(data);
    requires is_positive(data->a);
    requires is_positive(data->b);
    requires data->b <= data->a;
    behavior no:
      assumes data->a > data->b + 10;
      assigns \nothing;
    behavior yes:
      assumes data->a <= data->b + 10; 
      assigns data->b;
    ensures data->b <= data->a;
 */
void refresh(struct MyData* data)
{
  if (data->a <= data->b + 10)
  {
    data->b = data->a; 
  }
}

/*@ requires \valid(data);
    requires is_positive(data->a);
    requires is_positive(data->b);
    requires data->a >= data->b;
    assigns data->a; 
 */
void refresh_loop(struct MyData* data)
{
  int x = 0;
  /*@ loop invariant \valid(data);
      loop invariant is_positive(data->a); 
      loop invariant is_positive(data->b); 
      loop invariant data->a >= data->b;
	*/ 
  while(1)
  {
    x = something(); 
    //@ assert is_positive(x);
    data->a = data->a + x;   // increased by just any positive number
    //@ assert is_positive(data->a);
    //@ assert is_positive(data->b);
    //@ assert data->a >= data->b;
    refresh(data);
    //@ assert is_positive(data->a);
    //@ assert data->a >= data->b;
  }  
}