--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on August 2010 ---
Well, I couldn't reproduce the soundness issue, so I can't confirm that I eliminated it, but I suggest changing pop.spec so: #include "stack.h" #include "stack.pred" /*@ requires Valid(s); //ensures 0 == 1; // jessie detects this behavior not_empty: assumes !Empty(s); assigns s->n; ensures s->n == \old(s->n) - 1; // ensures !Empty(s); // probably unsound // ensures \forall integer i; 0 <= i < s->n ==> // s->c[i] == \old(s->c[i]); ensures \result == 0; // ensures Valid(s); // probably unnecessary with assigns clause behavior empty: assumes Empty(s); assigns \nothing; // ensures Empty(s); ensures \result == -1; // ensures Valid(s); */ int pop(Stack* s); The first clause I commented, "ensures !Empty(s);" is probably unsound. The others should be unnecessary because they are implied by the assigns clause that I recommend you use instead. Pascal