Can ACSL denote that an assignment should be hidden?

Question

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?

Answer 1

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.