Skip to content

Commit d4628fb

Browse files
committed
Fix CBMC proofs for mqttDownloader_processReceivedDataBlock
1 parent 9fe11c2 commit d4628fb

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

test/cbmc/proofs.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -127,6 +127,9 @@ void proof_mqttDownloader_processReceivedDataBlock( void )
127127
MqttFileDownloaderContext_t context = { 0 };
128128
uint8_t * message;
129129
size_t messageLength;
130+
int32_t fileId;
131+
int32_t blockId;
132+
int32_t blockSize;
130133
uint8_t * data;
131134
size_t dataLength;
132135
bool ret;
@@ -143,6 +146,9 @@ void proof_mqttDownloader_processReceivedDataBlock( void )
143146
ret = mqttDownloader_processReceivedDataBlock( &context,
144147
message,
145148
messageLength,
149+
&fileId,
150+
&blockId,
151+
&blockSize,
146152
data,
147153
&dataLength );
148154
}

0 commit comments

Comments
 (0)