--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on September 2009 ---
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; } }