This repository has been archived by the owner on Dec 8, 2022. It is now read-only.
Add CBMC OTA proof for prvRequestJob_MQTT #1965
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
feliperodri
reviewed
May 1, 2020
danielsn
reviewed
May 1, 2020
| pxAgentCtx.pvConnectionContext = &connContext; | ||
| __CPROVER_assume(pxAgentCtx.pvConnectionContext != NULL); | ||
|
|
||
| prvRequestJob_Mqtt(&pxAgentCtx); |
There was a problem hiding this comment.
Anything that can be asserted about pxAgentCtx after this operation finishes?
There was a problem hiding this comment.
pxAgentCtx is being operated on so it's possible that we could do some validation on what a "correct" pxAgentCtx would look like after the function has been called. Although this would be more along the lines of functional testing and is out of scope for this change.
markrtuttle
suggested changes
May 2, 2020
* Add NULL as a potential value for connContext * Add a newline to Makefile.json * Add a comment to the signature of function under test
yanjos-dev
force-pushed
the
cbmc/prvRequestJob_MQTT
branch
from
1e021ac to
95d52c6
Compare
markrtuttle
approved these changes
May 12, 2020
gkwicker
approved these changes
May 12, 2020
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
Added a CBMC proof for the prvRequestJob_MQTT OTA function.
Checklist:
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.