Can ACSL denote that an assignment should be hidden?
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?
frama-c acsl
asked Nov 19 '18 at 10:13
Rafael BachmannRafael Bachmann
426
add a comment |
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?
frama-c acsl
asked Nov 19 '18 at 10:13
Rafael BachmannRafael Bachmann
426
add a comment |
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?
frama-c acsl
asked Nov 19 '18 at 10:13
Rafael BachmannRafael Bachmann
426
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?
frama-c acsl
frama-c acsl
asked Nov 19 '18 at 10:13
Rafael BachmannRafael Bachmann
426
asked Nov 19 '18 at 10:13
Rafael BachmannRafael Bachmann
426
edited Nov 26 '18 at 17:23
Rafael Bachmann
asked Nov 19 '18 at 10:13
Rafael BachmannRafael Bachmann
426
asked Nov 19 '18 at 10:13
Rafael BachmannRafael Bachmann
426
asked Nov 19 '18 at 10:13
Rafael BachmannRafael Bachmann
426
426
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
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.
answered Nov 19 '18 at 15:38
VirgileVirgile
6,879931
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
StackExchange.using("externalEditor", function () {
StackExchange.using("snippets", function () {
StackExchange.snippets.init();
});
});
}, "code-snippets");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "1"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
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
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
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.
answered Nov 19 '18 at 15:38
VirgileVirgile
6,879931
add a comment |
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.
answered Nov 19 '18 at 15:38
VirgileVirgile
6,879931
add a comment |
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.
answered Nov 19 '18 at 15:38
VirgileVirgile
6,879931
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.
answered Nov 19 '18 at 15:38
VirgileVirgile
6,879931
edited Nov 26 '18 at 16:59
answered Nov 19 '18 at 15:38
VirgileVirgile
6,879931
answered Nov 19 '18 at 15:38
VirgileVirgile
6,879931
answered Nov 19 '18 at 15:38
VirgileVirgile
6,879931
6,879931
add a comment |
add a comment |
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
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
