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] Jessie - problem with an example


  • Subject: [Frama-c-discuss] Jessie - problem with an example
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
  • Date: Wed, 9 Sep 2009 10:31:23 +0200

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;
  }  
}