CBMC proof harness type fixes #510
Conversation
These changes add necessary forward declarations (or system headers includes) and address inconsistencies in how we invoke functions from CBMC proof harnesses as compared to their original signatures.
test/cbmc/proofs/decodeBase64IndexBuffer/decodeBase64IndexBuffer_harness.c
Show resolved
Hide resolved
| @@ -34,6 +34,8 @@ | |||
| extern OtaAgentContext_t otaAgent; | |||
| extern void freeFileContextMem( OtaFileContext_t * const pFileContext ); | |||
|
|
|||
| __CPROVER_bool nondet_bool(); | |||
There was a problem hiding this comment.
Why does this need to be declared here? And why the special return type given the earlier example nondet_int was returning a standard type?
There was a problem hiding this comment.
Here, this is only used for a true/false decision. We could, however, also pick a different type (that can be converted to an int) in here.
| @@ -84,7 +86,7 @@ DocParseErr_t parseJobDoc( const JsonDocParam_t * pJsonExpectedParams, | |||
|
|
|||
| void getFileContextFromJob_harness() | |||
| { | |||
| OtaFileContext_t * pFileContext; | |||
| OtaFileContext_t * pFileContext = &fileContext; | |||
There was a problem hiding this comment.
Why not get rid of this previously unused variable instead of now assigning it a value?
There was a problem hiding this comment.
There actually is a good use for this variable, see the next change: it's now used in calling getFileContextFromJob (which was previously passed a variable of the wrong type).
| @@ -29,6 +29,8 @@ | |||
| /* FreeRTOS includes for OTA library. */ | |||
| #include "ota_os_freertos.h" | |||
|
|
|||
| #include <stdlib.h> | |||
There was a problem hiding this comment.
NIT: should we not include such standard libs before the headers of our own libraries as a rule of FreeRTOS?
There was a problem hiding this comment.
Happy to adjust this if there is such a rule, I wasn't aware. Edit: none of the other harnesses seem to be following this, so I haven't changed it for now. Please let me know if you'd like me to change it.
Description
These changes add necessary forward declarations (or system headers includes) and address inconsistencies in how we invoke functions from CBMC proof harnesses as compared to their original signatures.
Checklist:
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.