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 CBMC proof of buildStatusMessageReceiving #272

Merged
merged 46 commits into from
Sep 13, 2021
Merged

Add CBMC proof of buildStatusMessageReceiving #272

merged 46 commits into from
Sep 13, 2021

Conversation

Bujain
Copy link
Contributor

@Bujain Bujain commented Aug 23, 2021 •
edited
Loading

Add CBMC proof of buildStatusMessageReceiving function

Description

Add CBMC proof of buildStatusMessageReceiving function

Checklist:

  • I have tested my changes. No regression in existing tests.
  • My code is formatted using Uncrustify.
  • I have read and applied the rules stated in CONTRIBUTING.md.

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

Bujain and others added 30 commits August 4, 2021 23:32
@Bujain
Add CBMC-proofs infrastructure
0bbf408
@Bujain
Add CBMC-proofs infrastructure (aws#242)
95529f8
@Bujain
Added value to not update the submodule
21ee448
@Bujain
Added Include paths and preprocessor defines
4b189aa
@Bujain
Added template define file
ae17c09
@Bujain
Updated to ignore the output files on git push
4a2ed43
@Bujain
Added words
6c5d6f5
@Bujain
Updated Project Name
b4a774c
@Bujain
Updated source directory path
db409b7
@AniruddhaKanhere
Merge branch 'cbmc-proof' into cbmc_infra
402e6b8
@AniruddhaKanhere
Update ci.yml
92b5b00
@AniruddhaKanhere
Add checks on the branch
62ddec4
@Bujain
Updated Submodule update value
67ad6b0
@Bujain
Merge branch 'cbmc_infra' of https://github.com/Bujain/ota-for-aws-io…
1f5668f 
…t-embedded-sdk into cbmc_infra
@Bujain
Added litani submodule update
3bda16a
@Bujain @AniruddhaKanhere
Update Project name
2c7f2ee 
Co-authored-by: Aniruddha Kanhere <[email protected]>
@Bujain
Added new line in the end of the file
e88c8c0
@AniruddhaKanhere
Remove whitespace
d274f81
@Bujain @AniruddhaKanhere
Addition to CBMC infrastructure (aws#243)
a085b6a 
* 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]>
@Bujain @AniruddhaKanhere
Added CBMC proof of setDataInterface function (aws#245)
fcb1efe 
* 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]>
@Bujain
Added template inside proof directory
f561a6c
@Bujain
Merge pull request #2 from aws/main
6122c14 
Add assert checks for http interface functions (aws#231)
@Bujain @AniruddhaKanhere
Added CBMC proof of OTA_HTTP_strerror function (aws#252)
e684033 
* 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]>
@Bujain @AniruddhaKanhere
Add CBMC proofs for RequestdataBlock_Http function (aws#248)
08fa29e 
* 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]>
@Bujain @AniruddhaKanhere
Added CBMC proofs for OTA_MQTT_strerror function (aws#247)
5a72e20 
* 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]>
@Bujain @AniruddhaKanhere
Added CBMC proofs for setControlInterface function (aws#246)
d470ee5 
* 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]>
@Bujain
removed extra line
4a2b21d
@Bujain
Merge branch 'cbmc_infra' of https://github.com/Bujain/ota-for-aws-io…
08b6b5c 
…t-embedded-sdk into cbmc_infra
@Bujain
Uncrustified'
b331892
@Bujain
Merge pull request #3 from Bujain/cbmc_infra
6f1dbe1 
Add CBMC proof infrastructure
Bujain and others added 6 commits August 17, 2021 23:43
@Bujain
Add CBMC proof of buildStatusMessageReceiving function
475122d
@Bujain @AniruddhaKanhere
CBMC Proof of initFileTransfer_Http function (aws#249)
8f4d71e 
* 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]>
@Bujain @AniruddhaKanhere
CBMC proof of decodeFileBlock_Http function (aws#250)
98cfba1 
* 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]>
@Bujain @AniruddhaKanhere
Added CBMC proof of CleanupData_Http function (aws#251)
194fca7 
* 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]>
@Bujain @AniruddhaKanhere @yanjos-dev
Added CBMC proof for stringBuilderUInt32Hex function (aws#253)
3bc7195 
* 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]>
@Bujain @AniruddhaKanhere
Added CBMC proof of stringBuilderUInt32Decimal function (aws#254)
71ce0bf 
* 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]>
@Bujain Bujain requested a review from divekarshubham August 23, 2021 18:40
@Bujain Bujain force-pushed the buildStatusMessageReceiving branch 2 times, most recently from 7e3eaca to 475122d Compare August 23, 2021 21:18
Bujain and others added 4 commits August 23, 2021 21:20
@Bujain
Updated spellings
743aa08
@Bujain
Merge branch 'aws:main' into buildStatusMessageReceiving
52bd2cf
@Bujain @pvyawaha
@divekarshubham @archigup
Update doxygen in cbmc-proof branch (aws#275)
c544dba 
* Add assert checks for http interface functions (aws#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 (aws#239)

* Adding a Pull request template

* Exclude .github from formatting check

* Applying PR feedback

* Update doxygen version to 1.9.2 (aws#274)

Co-authored-by: Prasad Vyawahare <[email protected]>
Co-authored-by: Shubham Divekar <[email protected]>
Co-authored-by: Archit Gupta <[email protected]>
@Bujain
Merge branch 'cbmc-proof' into buildStatusMessageReceiving
a22bea7
@Bujain Bujain changed the base branch from cbmc-proof to main August 31, 2021 22:19
divekarshubham
divekarshubham previously approved these changes Sep 2, 2021
View reviewed changes
@Bujain Bujain merged commit fc6fae5 into aws:main Sep 13, 2021
@Bujain Bujain deleted the buildStatusMessageReceiving branch September 21, 2021 14:42
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

@divekarshubham divekarshubham divekarshubham 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.
4 participants
@Bujain @n9wxu @divekarshubham @AniruddhaKanhere