This function mocks a function that returns a continuously rising value until overflow occurs. It is like the millis() function in Arduino.
To prove the implementation, I need to increment (thus, assign) static variables to keep state between invocations. However, a function that calls mock_millis() should still be able to assign \nothing.
Is there a way to make WP ignore the assigns clause?
static int64_t milliseconds = 0;
/*@ assigns milliseconds;
behavior normal:
assumes milliseconds < INT64_MAX;
ensures \result == \old(milliseconds) + 1;
ensures milliseconds == \old(milliseconds) + 1;
behavior overflow:
assumes milliseconds == INT64_MAX;
ensures \result == 0;
ensures milliseconds == 0;
complete behaviors normal, overflow;
disjoint behaviors normal, overflow;
*/
int64_t mock_millis() {
if (milliseconds < INT64_MAX) {
milliseconds++;
} else {
milliseconds = 0;
}
return milliseconds;
}
I tried doing this with ghost variables, and noticed that a function that assigns a ghost variable cannot be assigns \nothing. I thought ghost variables were completely independent of the program implementation. Is there a special reason for this?
I assume your static variable is meant to be called milliseconds and not microseconds as it is now.
Your assumption about ghost variables is indeed wrong: ghost code is not supposed to interfere with real code and vice-versa (note that this is not enforced by Frama-C at this point). Hence if you declare milliseconds as ghost, any assignment to it is supposed to occur inside ghost code. But from a specification point of view, such assignments are nevertheless side-effects that need to be mentioned in the assigns clause.