Mixing
Can ACSL denote that an assignment should be hidden?
up vote
1
down vote
favorite
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 microseconds = 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?
frama-c acsl
asked yesterday
Rafael Bachmann
356
add a comment |
up vote
1
down vote
favorite
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 microseconds = 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?
frama-c acsl
asked yesterday
Rafael Bachmann
356
add a comment |
up vote
1
down vote
favorite
up vote
1
down vote
favorite
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 microseconds = 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?
frama-c acsl
asked yesterday
Rafael Bachmann
356
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 microseconds = 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?
frama-c acsl
frama-c acsl
asked yesterday
Rafael Bachmann
356
asked yesterday
Rafael Bachmann
356
asked yesterday
Rafael Bachmann
356
asked yesterday
Rafael Bachmann
356
asked yesterday
Rafael Bachmann
356
356
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
up vote
1
down vote
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 (not 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.
answered yesterday
Virgile
6,529830
add a comment |
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
1
down vote
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 (not 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.
answered yesterday
Virgile
6,529830
add a comment |
up vote
1
down vote
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 (not 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.
answered yesterday
Virgile
6,529830
add a comment |
up vote
1
down vote
up vote
1
down vote
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 (not 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.
answered yesterday
Virgile
6,529830
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 (not 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.
answered yesterday
Virgile
6,529830
answered yesterday
Virgile
6,529830
answered yesterday
Virgile
6,529830
answered yesterday
Virgile
6,529830
6,529830
add a comment |
add a comment |
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53372397%2fcan-acsl-denote-that-an-assignment-should-be-hidden%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
