Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add assert checks for http interface functions #231

Merged
merged 7 commits into from
Aug 9, 2021
Merged

Add assert checks for http interface functions #231

merged 7 commits into from
Aug 9, 2021

Conversation

Bujain
Copy link
Contributor

@Bujain Bujain commented Jul 26, 2021

Added assert checks in the ota_http.c to check if the http interface functions are not pointing at NULL.

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

@Bujain Bujain changed the title Add fail check Add assert checks for http interface functions Jul 26, 2021
pvyawaha
pvyawaha previously approved these changes Jul 28, 2021
View reviewed changes
pvyawaha
pvyawaha reviewed Jul 28, 2021
View reviewed changes
source/ota_http.c Outdated
@@ -51,7 +51,7 @@ OtaErr_t initFileTransfer_Http( OtaAgentContext_t * pAgentCtx )
OtaFileContext_t * fileContext = NULL;

LogDebug( ( "Invoking initFileTransfer_Http" ) );
assert( pAgentCtx != NULL && pAgentCtx->pOtaInterface != NULL );
assert( pAgentCtx != NULL && pAgentCtx->pOtaInterface != NULL && pAgentCtx->pOtaInterface->http.init != NULL );
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Minor ( ( ) && ( ) .. will make it slightly more readable.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have added those changes to the last commit.

@Bujain Bujain merged commit 813dcbc into aws:main Aug 9, 2021
@Bujain Bujain deleted the addFailCheck branch August 9, 2021 19:29
Bujain added a commit to Bujain/ota-for-aws-iot-embedded-sdk that referenced this pull request Aug 9, 2021
@Bujain
Merge pull request #2 from aws/main
6122c14 
Add assert checks for http interface functions (aws#231)
Bujain added a commit that referenced this pull request Aug 23, 2021
@Bujain @pvyawaha
@divekarshubham @archigup
Update doxygen in cbmc-proof branch (#275)
c544dba 
* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
This was referenced Aug 24, 2021
Merged
Merged
Merged
Merged
Merged
Merged
Bujain added a commit that referenced this pull request Aug 30, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Merge CBMC-proof branch with main (#279)
2a8536e 
* Add CBMC-proofs infrastructure (#242)

* Update ci.yml

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
@Bujain Bujain mentioned this pull request Aug 31, 2021
Merged
3 tasks
Bujain added a commit that referenced this pull request Sep 9, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of updateBase64DecodingBuffer function (#271)
3cb6e0b 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proof of updateBase64DecodingBuffer function.

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Updated comments

* updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 9, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of preprocessBase64Index function (#270)
5cd2f96 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proof of preprocessBase64Index function

* removed cbmc_proof template code

* Updated source directory

* Fix spell-check errors

* Fix formatting errors

* Add spelling

* Add spellings

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Updated macro declaration

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 9, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of decodeBase64IndexBuffer function (#269)
f9e1168 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proof of decodeBase64IndexBuffer function

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* removed vscode folder

* removed vscode folder

* Free dynamically allocated variable

* Fix formatting errors

* Removed assumption

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 9, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of base64Decode function (#268)
c42a16c 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for base64Decode function

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Free dynamic allocated variables

* Updated comment

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 9, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of decodeFIleBlock_Mqtt function (#277)
f830187 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Updated source directory

* Add spellings

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Add CBMC proof of decodeFileBlock_Mqtt function

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 9, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add the CBMC proof of requestFileBlock_Mqtt function (#273)
aba6ef1 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* Add CBMC proof of requestFileBlock_Mqtt function

* Updated the stubs and spellings

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Updated comments and removed unncessary variables

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 9, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of cleanupControl_Mqtt function (#266)
3d60675 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* Add CBMC proof of cleanupControl_Mqtt function

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* update comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 9, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of updateJobStatusMqtt function (#264)
e12b470 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* Add CBMC proof of updateJobStatus_Mqtt function

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* updated comments and removed unused variables

* Fix spell-check errors

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 9, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of requestJobMqtt function (#263)
7e145b6 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* Add CBMC proof  equestJob_Mqtt functionn

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* removed unnecessary variables

* fix formatting error

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 9, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proofs for unsubscribefromdatastream function (#257)
01c8855 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC-proof for unsubscribeFromDataStream function

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added assert checks for stringBuilder

* add new words

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Updated comments and removed unnecessary variables

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 9, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of OTA_CBOR_Decode_GetStreamResponseMessage (#278)
55a90ba 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Updated source directory

* Add spellings

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Add CBMC proof of OTA_CBOR_Decode_GetStreamResponseMessage function

* Removed unwanted stubs

* Updated stub comments and spell check errors

* Update comments

* Fix formatting error

* Added returnCBOR function

* update include path

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 9, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Added CBMC proofs for subscribeToJobNotificationTopics function (#256)
d8f8f3f 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC-proof files of stringBuilder function

* Added CBMC-proof for subscribeToJobNotificationTopics function

* Added assertions to stringBuilder stub

* Updated error messages

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Updated function name and removed unwinding of loops

* fixed formatting errors

* Fix spell check errors

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Updated documentation

* Updated doxygen config

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* updated comments

* Fix minor issues with build CBMC proofs.

* Updated proof root and proof name

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Co-authored-by: Mark R. Tuttle <[email protected]>
Bujain added a commit that referenced this pull request Sep 9, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of cleanupData_Mqtt function (#265)
d8e70c3 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* Add CBMC proof of cleanupData_Mqtt function

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Updated comments and remove unwanted variables

* Removed unwanted variables

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 13, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of prvBuildstatusMessageFinish function (#262)
458a275 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* Add CBMC proof of prvbuildstatusmessagefinish function

* Fix formatting errors

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Update comments

Co-authored-by: Shubham Divekar <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 13, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of buildStatusMessageReceiving (#272)
fc6fae5 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* Add CBMC proof of buildStatusMessageReceiving function

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Updated spellings

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* update comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 14, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of prvBuildStatusMessageSelfTest (#261)
af00add 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* Add CBMC proof of prvBuildStatusMessageSelfTest function

* Updated comments

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Update comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 20, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of OTA_CBOR_Encode_GetStreamRequestMessage functions (#…
2d52505 
…280)

* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Updated source directory

* Add spellings

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Add CBMC proof of bool OTA_CBOR_Encode_GetStreamRequestMessage function

* removed vscode settings

* Add header file for malloc

* update include path

* Free dynamically allocated variables

* Uncrustified

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 20, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of initFileTransfer_Mqtt function (#276)
f024a39 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Add CBMC proof of initFileTransfer_Mqtt function

* update comments

* update comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Sep 20, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of UnsubscribefromJobNotificationTopic function (#258)
eb0df7e 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC-proof of unsubscribeFromJobNotificationTopic function.

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Update stringbuilder function and added words to spell check

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Updated comments

* fix spell-check issues

* Added assert to check the interface is initialized

* Fix formatting issues

* Removed new line

* Update comment

* Fix formatting

* Fix formatting errors

* removed unused variables

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Bujain added a commit that referenced this pull request Oct 25, 2021
@Bujain @AniruddhaKanhere
@yanjos-dev @pvyawaha @divekarshubham @archigup
Add CBMC proof of checkDataType function (#293)
cee0641 
* Add CBMC-proofs infrastructure

* Add CBMC-proofs infrastructure (#242)

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Update ci.yml

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Addition to CBMC infrastructure (#243)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of setDataInterface function (#245)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setDataInterface function

* removed unnecessary variables

* Updated documentation

* Uncrustified

* Updated year in copyright notice

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added template inside proof directory

* Added CBMC proof of OTA_HTTP_strerror function (#252)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of OTA_HTTP_strerror function

* Removed extra line and updated error log

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC proofs for RequestdataBlock_Http function (#248)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC Proof of requestDataBlock_Http function

* Removed extra line

* Update Comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for OTA_MQTT_strerror function (#247)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for OTA_MQTT_strerror function

* Removed extra line

* Updated comments

* Fixed formatting errors

* Updated error log

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proofs for setControlInterface function (#246)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for setControlInterface function

* Removed extra line

* Added macro for the function

* Fix formating errors

* Fix spell check errors

* Added preprocessor definition for setControlInterface function

Co-authored-by: Aniruddha Kanhere <[email protected]>

* removed extra line

* Uncrustified'

* CBMC Proof of initFileTransfer_Http function (#249)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC proof of initFileTransfer_Http function

* Removed extra line

* Updated Comments

* Updated error log and comments

* Updated comments

* Fix formatting errors

Co-authored-by: Aniruddha Kanhere <[email protected]>

* CBMC proof of decodeFileBlock_Http function (#250)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for decodeFileBlock_Http function

* Removed extra line

* Updated Comments

* Fix formatting errors

* Updated comments

* Fix spell check error

* Updated comments

* Fix spell check errors

* Updated arugments to malloc

* updated the datatype in malloc argument

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof of CleanupData_Http function (#251)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Added CBMC proof for cleanupData_Http function

* removed extra line

* Updated Comments

* Fixed formatting errors

* Update error log

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added CBMC proof for stringBuilderUInt32Hex function  (#253)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* added CBMC-proof files

* Added Unwinding flag

* Updated buffer initialization

* Fixed spell check and formatting errorst

* Updated comments

* Added loop unwinding

* Updated comments

* Fix formatting errors

* Added comment

* updated the arguments to malloc

* Updated comments

Co-authored-by: Joshua Yan <[email protected]>

* Updated comments

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>

* Added CBMC proof of stringBuilderUInt32Decimal function (#254)

* Add CBMC-proofs infrastructure

* Added value to not update the submodule

* Added Include paths and preprocessor defines

* Added template define file

* Updated to ignore the output files on git push

* Added words

* Updated Project Name

* Updated source directory path

* Add checks on the branch

* Updated Submodule update value

* Added litani submodule update

* Update Project name

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Added new line in the end of the file

* Remove whitespace

* Add CBMC-proof files for stringBuilderUInt32Decimal

* Fixed spell check and formatting errors

* Updated Comments

* Add loop unwinding

* Updated comments

* Updated comments

* Updated spellings

* updated arguments to the malloc

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Updated source directory

* Add spellings

* Update doxygen in cbmc-proof branch (#275)

* Add assert checks for http interface functions (#231)

* Add assert checks for http interface functions

* Uncrustified

* Added spaces in assertion arguments

Co-authored-by: Prasad Vyawahare <[email protected]>

* Adding a Pull request template (#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>

* Add CBMC proof of checkDataType function

* Resolve conflicts

* add words

* Fix spell check errors

* Fix spell check error

* Removed unused variables

* Add return value check

* uncrustified

* Add check for return value

* Uncrustified

* remove optional variables

Co-authored-by: Aniruddha Kanhere <[email protected]>
Co-authored-by: Joshua Yan <[email protected]>
Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@n9wxu n9wxu n9wxu approved these changes

@pvyawaha pvyawaha pvyawaha approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@Bujain @n9wxu @pvyawaha