search

aws / aws-iot-core-mqtt-file-streams-embedded-c

MIT License
2 stars 6 forks source link

Fix CBMC proofs for mqttDownloader_processReceivedDataBlock #27

Closed kar-rahul-aws closed 5 months ago

kar-rahul-aws commented 6 months ago

Issue #, if available: CBMC proofs fail for mqttDownloader_processReceivedDataBlock with the following error

  {
    "messageText": "wrong number of function arguments: expected 8, but got 5",
    "messageType": "ERROR",
    "sourceLocation": {
      "file": "proofs.c",
      "function": "proof_mqttDownloader_processReceivedDataBlock",
      "line": "143",
      "workingDirectory": "/home/ubuntu/Temp/karahulx_coreMQTTFileStreams/aws-iot-core-mqtt-file-streams-embedded-c/test/cbmc"
    }
  },
  {
    "messageText": "CONVERSION ERROR",
    "messageType": "ERROR"
  }

Description of changes: This PR fixes CBMC proofs for the mqttDownloader_processReceivedDataBlock API .