Added CBMC proof of setDataInterface function #245

Bujain · 2021-08-05T21:53:57Z

Description of changes:
In this PR, all the files related to the CBMC proof for setDataInterface function have been added.

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

…t-embedded-sdk into cbmc_infra

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

test/cbmc/proofs/setDataInterface/README.md

.github/workflows/ci.yml

test/cbmc/proofs/setDataInterface/cbmc-viewer.json

yanjos-dev · 2021-08-05T22:12:56Z

test/cbmc/proofs/setDataInterface/setDataInterface_harness.c

+    /* The maximum size of the protocol buffer is defined by OTA_PROTOCOL_BUFFER_SIZE
+     *  and thus size variable cannot exceed OTA_PROTOCOL_BUFFER_SIZE. */
+    __CPROVER_assume( protocolBufferSize <= OTA_PROTOCOL_BUFFER_SIZE );


This is not the maximum size, it's the exact size. So I don't think this makes sense to do. There may be other places where this macro is used and that could cause issues. For example, if there is a for loop that iterates up until the OTA_PROTOCOL_BUFFER_SIZE.

In this case, if the protocolBufferSize was smaller, which is possible with this code, there would be a segmentation fault as we step out of bounds of the array.

This is not a user config, so it won't change depending on the user's application and it won't change at runtime. In this case we can just allocate a static buffer of size OTA_PROTOCOL_BUFFER_SIZE. I noticed that the array is statically allocated in the ota.c source file, so I think this okay to do.

When you change this to static allocation:

Add a comment about how this buffer is statically allocated inside of the library source code based on macro that is not configurable by the user, so we know that it will always be this size.

Make sure to remove the free statement that you have.

Delete the unnecessary variables, namely protocolBufferSize.

Updated the file in (6584e87)

.github/workflows/ci.yml

test/cbmc/proofs/Makefile-template-defines

…aws-iot-embedded-sdk into setDataInterface

paulbartell · 2021-08-06T23:16:14Z

test/cbmc/proofs/setDataInterface/setDataInterface_harness.c

@@ -0,0 +1,49 @@
+/*
+ * AWS IoT Over-the-air Update v3.0.0
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.


Suggested change

* Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved.

* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.

I have updated the same.

* 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]>

* 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]>

* 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]>

* 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]>

* 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]>

* 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]>

* 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]>

* 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]>

* 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]>

* 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]>

* 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 files for publishStatusMessage 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]> * Fix cbmc failures and updated comments * Update source directory * update source directory * fix spell check errors * Updated comments and removed unnecessary variables Co-authored-by: Aniruddha Kanhere <[email protected]>

* 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]>

* 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 * Updated assumptions * Updated assumptions' * Removed copyright notice * 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 comments * Fix spell check and formatting errors * Added null terminator to every string Co-authored-by: Aniruddha Kanhere <[email protected]>

* 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]>

* 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]>

* 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]>

* 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]>

* 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]>

* 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]>

…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]>

* 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]>

* 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]>

* 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]>

Bujain and others added 17 commits August 4, 2021 23:32

Add CBMC-proofs infrastructure

0bbf408

Added value to not update the submodule

21ee448

Added Include paths and preprocessor defines

4b189aa

Added template define file

ae17c09

Updated to ignore the output files on git push

4a2ed43

Added words

6c5d6f5

Updated Project Name

b4a774c

Updated source directory path

db409b7

Merge branch 'cbmc-proof' into cbmc_infra

402e6b8

Add checks on the branch

62ddec4

Updated Submodule update value

67ad6b0

Merge branch 'cbmc_infra' of https://github.com/Bujain/ota-for-aws-io…

1f5668f

…t-embedded-sdk into cbmc_infra

Added litani submodule update

3bda16a

Update Project name

2c7f2ee

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

Added new line in the end of the file

e88c8c0

Remove whitespace

d274f81

Added CBMC proof for setDataInterface function

f54e3bd

Bujain requested review from AniruddhaKanhere and yanjos-dev August 5, 2021 21:54

yanjos-dev suggested changes Aug 5, 2021

View reviewed changes

AniruddhaKanhere reviewed Aug 5, 2021

View reviewed changes

.github/workflows/ci.yml Outdated Show resolved Hide resolved

test/cbmc/proofs/Makefile-template-defines Outdated Show resolved Hide resolved

Bujain and others added 5 commits August 6, 2021 00:25

removed unnecessary variables

6584e87

Updated documentation

00c584f

Merge branch 'cbmc-proof' into setDataInterface

b18f3a7

Uncrustified

11e33e5

Merge branch 'setDataInterface' of https://github.com/Bujain/ota-for-…

5052aae

…aws-iot-embedded-sdk into setDataInterface

yanjos-dev approved these changes Aug 6, 2021

View reviewed changes

paulbartell reviewed Aug 6, 2021

View reviewed changes

paulbartell approved these changes Aug 6, 2021

View reviewed changes

Updated year in copyright notice

2d459ee

Bujain merged commit fcb1efe into aws:cbmc-proof Aug 6, 2021

Bujain deleted the setDataInterface branch August 9, 2021 19:44

Bujain mentioned this pull request Aug 25, 2021

Merge CBMC-proof branch with main #279

Merged

3 tasks

Bujain mentioned this pull request Aug 31, 2021

Merge CBMC-proof branch with main (#279) Bujain/ota-for-aws-iot-embedded-sdk#27

Merged

3 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Added CBMC proof of setDataInterface function #245

Added CBMC proof of setDataInterface function #245

Bujain commented Aug 5, 2021

yanjos-dev Aug 5, 2021

Bujain Aug 6, 2021 •

edited

Loading

paulbartell Aug 6, 2021 •

edited

Loading

Bujain Aug 6, 2021

	* Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved.
	* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.

Added CBMC proof of setDataInterface function #245

Added CBMC proof of setDataInterface function #245

Conversation

Bujain commented Aug 5, 2021

yanjos-dev Aug 5, 2021

Choose a reason for hiding this comment

Bujain Aug 6, 2021 • edited Loading

Choose a reason for hiding this comment

paulbartell Aug 6, 2021 • edited Loading

Choose a reason for hiding this comment

Bujain Aug 6, 2021

Choose a reason for hiding this comment

Bujain Aug 6, 2021 •

edited

Loading

paulbartell Aug 6, 2021 •

edited

Loading