aws / ota-for-aws-iot-embedded-sdk

MIT License
60 stars 74 forks source link

Fix breaking OTA CBMC proofs #448

Closed AniruddhaKanhere closed 2 years ago

AniruddhaKanhere commented 2 years ago

Description

This PR fixes the broken CBMC proofs for the below two functions.

It does so by introducing a stub for the use of poll function introduced with https://github.com/aws/ota-for-aws-iot-embedded-sdk/pull/433. The stub non-deterministically returns either a success or a failure along with corresponding flag(s) being set.

Checklist:

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

AniruddhaKanhere commented 2 years ago

These changes were incorporated in https://github.com/aws/ota-for-aws-iot-embedded-sdk/pull/446.