From 508651ce86741798e7d919387badcf66e4d4c45b Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Mon, 29 Jan 2024 17:50:56 -0500 Subject: [PATCH] CI CD Update (#105) * Onboard to CI-CD Workflows * Use ubuntu latest for CBMC now that the default runner is multicore. * Fix broken link in CBMC proofs * Add the path to the manifest file * Ignore the coreMQTT source files in the coverage check * Add CMock to the manifest * Exclude 'dependency' instead of 'coreMQTT' as that match didn't work * Recurse submodules when doing doxygen as coreMQTT is needed for the doxygen output * Apply formatting changes * Remove trailing slash in CBMC proof url * Use the github hosted MQTT doxygen to see if that fixes the issue * Add the removed step to the workflow to download the tag, revert the doxyfile change --- .github/.cSpellWords.txt | 174 +++++++++++ .github/workflows/ci.yml | 127 ++++++-- .github/workflows/formatting.yml | 23 ++ cspell.config.yaml | 22 ++ lexicon.txt | 290 ------------------ manifest.yml | 10 +- source/core_mqtt_agent.c | 16 +- .../proofs/MQTTAgentCommand_Connect/README.md | 4 +- .../MQTTAgentCommand_Disconnect/README.md | 2 +- .../proofs/MQTTAgentCommand_Ping/README.md | 2 +- .../MQTTAgentCommand_ProcessLoop/README.md | 2 +- .../proofs/MQTTAgentCommand_Publish/README.md | 2 +- .../MQTTAgentCommand_Subscribe/README.md | 2 +- .../MQTTAgentCommand_Terminate/README.md | 2 +- .../MQTTAgentCommand_Unsubscribe/README.md | 2 +- .../cbmc/proofs/MQTTAgent_CancelAll/README.md | 2 +- .../proofs/MQTTAgent_CommandLoop/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Connect/README.md | 2 +- .../proofs/MQTTAgent_Disconnect/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Init/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Ping/README.md | 2 +- .../proofs/MQTTAgent_ProcessLoop/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Publish/README.md | 2 +- .../proofs/MQTTAgent_ResumeSession/README.md | 2 +- .../cbmc/proofs/MQTTAgent_Subscribe/README.md | 2 +- .../cbmc/proofs/MQTTAgent_Terminate/README.md | 2 +- .../proofs/MQTTAgent_Unsubscribe/README.md | 2 +- test/cbmc/sources/mqtt_agent_cbmc_state.c | 1 + test/cbmc/stubs/core_mqtt_stubs.c | 1 + 29 files changed, 364 insertions(+), 342 deletions(-) create mode 100644 .github/.cSpellWords.txt create mode 100644 .github/workflows/formatting.yml create mode 100644 cspell.config.yaml delete mode 100644 lexicon.txt diff --git a/.github/.cSpellWords.txt b/.github/.cSpellWords.txt new file mode 100644 index 00000000..69262e59 --- /dev/null +++ b/.github/.cSpellWords.txt @@ -0,0 +1,174 @@ +ACKS +Ack +CBMC +CBOR +CMOCK +CMock +CONNACK +COVERITY +CSDK +CTest +CmdCompleteCallback +Cmock +Coverity +DCMOCK +DECIHOURS +DNDEBUG +DOXYGEN +DUNITY +DUP +Decihours +Deserialized +Doxygen +FuncToTest +Init +LWT +MISRA +MQTT +MQTT's +MQTTAgentCommandFunc +MQTTAgentCommandFuncReturns +MQTTAgentConnectArgs +MQTTAgentSubscribeArgs +MQTTGetCurrentTimeFunc +MQTTQoS +MQTTRecvFailed +Misra +Mqtt +NONDET +NUM +Nondet +POSIX +PUBACK +PUBLISHes +QOS +QoS +Qos +RECV +SDK +STDC +SUBACK +SUBACK's +SYSCLK +SYSCLOCK +SYSClk +Struct +SysClk +SysClock +Sysclk +Sysclock +TODO +UNACKED +UNPADDED +UNSUB +UNSUBACK +Unpadded +Unprotect +Unprotected +Unsub +VECT +Vect +Wunused +ack +acked +acknowledgement +acknowledgements +acks +args +bool +br +bytesToRecv +cbmc +cbor +cmdCompleteCallback +cmdCompleteCb +cmock +connectArgs +connectCmdCallback +connectionArgs +const +coremqtt +coverity +ctest +ctestACK +decihours +deserialized +disconnectCmdCallback +doxygen +dup +endcond +enqueue +enqueued +enqueueing +enqueues +enum +enums +func +getpacketid +hu +ifndef +init +initalized +initializers +isystem +lcov +lwt +memset +messagectx +messagerecv +misra +mqtt +mypy +networkRecv +nondet +numSubscriptions +pAckInfo +pArgs +pCmdCallbackContext +pCmdCompleteCallbackContext +pCmdContext +pConnectArgs +pDeserializedInfo +pFuncName +pMqttInfoParam +pMsgCtx +pMsgInterface +pParams +pPendingAcks +pPublishArg +pSubackCodes +pSubscribeArgs +pSubscriptionArgs +pUnusedArg +pVoidConnectArgs +pVoidSubscribeArgs +params +pendingAcks +preprocessor +printf +publishCmdCompleteCb +pylint +pytest +pyyaml +qos +recv +sinclude +strlen +struct +structs +suback +subscribeArgs +subscribeCmdCompleteCb +sysclk +sysclock +th +uint +unpadded +unprotect +unsubscribeArgs +unsubscribeCmdCompleteCb +unsubscriptions +utest +vect +writev +xlarge diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 511fd2b0..cc4fd6ca 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,5 +1,11 @@ name: CI Checks +env: + bashPass: \033[32;1mPASSED - + bashInfo: \033[33;1mINFO - + bashFail: \033[31;1mFAILED - + bashEnd: \033[0m + on: push: branches: ["**"] @@ -12,11 +18,20 @@ jobs: runs-on: ubuntu-latest steps: - name: Clone This Repo - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: submodules: recursive - - name: Build + + - name: Perform Recursive Clone + shell: bash + run: git submodule update --checkout --init --recursive + + - env: + stepName: Build CoreMQTT run: | + # ${{ env.stepName }} + echo -e "::group::${{ env.bashInfo }} ${{ env.stepName }} ${{ env.bashEnd }}" + sudo apt-get install -y lcov cmake -S test -B build/ \ -G "Unix Makefiles" \ @@ -24,66 +39,91 @@ jobs: -DBUILD_CLONE_SUBMODULES=ON \ -DCMAKE_C_FLAGS='--coverage -Wall -Wextra -Werror -DNDEBUG -DLIBRARY_LOG_LEVEL=LOG_DEBUG' make -C build/ all - - name: Test - run: | - cd build/ - ctest -E system --output-on-failure - cd .. - - name: Run Coverage + + echo "::endgroup::" + echo -e "${{ env.bashPass }} ${{env.stepName}} ${{ env.bashEnd }}" + + - name: Run Tests + run: ctest --test-dir build -E system --output-on-failure + + - env: + stepName: Line and Branch Coverage Build run: | + # ${{ env.stepName }} + echo -e "::group::${{ env.bashInfo }} Build Coverage Target ${{ env.bashEnd }}" + # Build the coverage target make -C build/ coverage - declare -a EXCLUDE=("\*test\*" "\*CMakeCCompilerId\*" "\*mocks\*" "\*dependency\*") - echo ${EXCLUDE[@]} | xargs lcov --rc lcov_branch_coverage=1 -r build/coverage.info -o build/coverage.info + + echo -e "::group::${{ env.bashInfo }} Generate Coverage Report ${{ env.bashEnd }}" + # Generate coverage report, excluding extra directories + lcov --rc lcov_branch_coverage=1 -r build/coverage.info -o build/coverage.info '*test*' '*CMakeCCompilerId*' '*mocks*' '*dependency*' + + echo "::endgroup::" lcov --rc lcov_branch_coverage=1 --list build/coverage.info + echo -e "${{ env.bashPass }} ${{env.stepName}} ${{ env.bashEnd }}" + - name: Check Coverage uses: FreeRTOS/CI-CD-Github-Actions/coverage-cop@main with: - path: ./build/coverage.info + coverage-file: ./build/coverage.info + complexity: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v3 - name: Check complexity uses: FreeRTOS/CI-CD-Github-Actions/complexity@main with: path: ./ + horrid_threshold: 12 + doxygen: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 - - name: Download MQTT tag + - uses: actions/checkout@v3 + + - env: + stepName: Download MQTT tag + name: ${{ env.stepName }} run: | # We don't need to generate the coreMQTT docs, we only need the tag file. We can just download it. + echo -e "::group::${{ env.bashInfo }} ${{ env.stepName }} ${{ env.bashEnd }}" mkdir -p source/dependency/coreMQTT/docs/doxygen/output wget -O source/dependency/coreMQTT/docs/doxygen/output/mqtt.tag \ "https://freertos.org/Documentation/api-ref/coreMQTT/docs/doxygen/output/mqtt.tag" + echo -e "::endgroup::" + echo -e "${{env.bashPass}} ${{ env.stepName }} ${{ env.bashEnd }}" + - name: Run doxygen build uses: FreeRTOS/CI-CD-Github-Actions/doxygen@main with: path: ./ + spell-check: runs-on: ubuntu-latest steps: - name: Clone This Repo - uses: actions/checkout@v2 + uses: actions/checkout@v3 - name: Run spellings check uses: FreeRTOS/CI-CD-Github-Actions/spellings@main with: path: ./ + formatting: - runs-on: ubuntu-latest + runs-on: ubuntu-20.04 steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v3 - name: Check formatting uses: FreeRTOS/CI-CD-Github-Actions/formatting@main with: path: ./ + git-secrets: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v3 - name: Checkout awslabs/git-secrets - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: repository: awslabs/git-secrets ref: master @@ -94,19 +134,61 @@ jobs: run: | git-secrets --register-aws git-secrets --scan + memory_statistics: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v3 + with: + submodules: 'recursive' + + - name: Install Python3 + uses: actions/setup-python@v3 with: - submodules: 'recursive' + python-version: '3.11.0' + - name: Measure sizes uses: FreeRTOS/CI-CD-Github-Actions/memory_statistics@main with: config: .github/memory_statistics_config.json check_against: docs/doxygen/include/size_table.md + + + link-verifier: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v3 + - name: Check Links + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + uses: FreeRTOS/CI-CD-Github-Actions/link-verifier@main + with: + path: ./ + + + verify-manifest: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v3 + with: + submodules: true + fetch-depth: 0 + + # At time of writing the gitmodules are set not to pull + # Even when using fetch submodules. Need to run this command + # To force it to grab them. + - name: Perform Recursive Clone + shell: bash + run: git submodule update --checkout --init --recursive + + - name: Run manifest verifier + uses: FreeRTOS/CI-CD-GitHub-Actions/manifest-verifier@CI-CD-Overhaul + with: + path: ./ + fail-on-incorrect-version: true + proof_ci: - runs-on: cbmc_ubuntu-latest_64-core + runs-on: ubuntu-latest steps: - name: Set up CBMC runner uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main @@ -114,3 +196,4 @@ jobs: uses: FreeRTOS/CI-CD-Github-Actions/run_cbmc@main with: proofs_dir: test/cbmc/proofs + diff --git a/.github/workflows/formatting.yml b/.github/workflows/formatting.yml new file mode 100644 index 00000000..04786bad --- /dev/null +++ b/.github/workflows/formatting.yml @@ -0,0 +1,23 @@ +name: Format Pull Request Files + +on: + issue_comment: + types: [created] + +env: + bashPass: \033[32;1mPASSED - + bashInfo: \033[33;1mINFO - + bashFail: \033[31;1mFAILED - + bashEnd: \033[0m + +jobs: + Formatting: + name: Run Formatting Check + if: ${{ github.event.issue.pull_request && + ( ( github.event.comment.body == '/bot run uncrustify' ) || + ( github.event.comment.body == '/bot run formatting' ) ) }} + runs-on: ubuntu-20.04 + steps: + - name: Apply Formatting Fix + uses: FreeRTOS/CI-CD-Github-Actions/formatting-bot@main + id: check-formatting diff --git a/cspell.config.yaml b/cspell.config.yaml new file mode 100644 index 00000000..e7d8a56f --- /dev/null +++ b/cspell.config.yaml @@ -0,0 +1,22 @@ +--- +$schema: https://raw.githubusercontent.com/streetsidesoftware/cspell/main/cspell.schema.json +version: '0.2' +# Allows things like stringLength +allowCompoundWords: true +useGitignore: true +# Could split this up? And do a dictionary for each repo? +# But feel like if this isn't super slow +# That having just one single dictionary might be nicer? +dictionaryDefinitions: + - name: freertos-words + path: '.github/.cSpellWords.txt' + addWords: true +dictionaries: + - freertos-words +ignorePaths: + - 'node_modules' + - '.cSpellWords.txt' + - 'dependency' + - 'docs' + - 'ThirdParty' + diff --git a/lexicon.txt b/lexicon.txt deleted file mode 100644 index 89913d64..00000000 --- a/lexicon.txt +++ /dev/null @@ -1,290 +0,0 @@ -ack -acked -ackinfo -acks -addacknowledgment -agentcommandget -agentcommandrelease -agentcontext -agentinterface -agentmessagecontext -agentmessageinterface -agentmessagerecv -agentmessagesend -agentreceivemessage -agentsendmessage -api -apis -appcallback -args -aws -blocktimems -bool -br -bytesorerror -bytestorecv -bytestosend -cbmc -cleansession -cleansession -clearonlysubunsubentries -clientidentifierlength -clientidentifierlength -cmdcompletecallback -cmdcompletecb -com -commandcallback -commandcompletecallback -commandcontext -commandinfo -commandloop -commandtype -cond -config -configpagestyle -connack -connectargs -connectcallback -connectcmdcallback -connectinfo -connectionargs -connectstatus -connectstatus -const -copydoc -coremqtt -cpu -createandaddcommand -css -defgroup -deserialized -didn -disconnectcallback -disconnectcmdcallback -doesn -doxygen -dup -endcode -endcond -endif -endloop -enqueueing -enum -enums -fixedbuffer -foo -freertos -func -functotest -gcc -getcommand -getcurrenttimems -gettimestampms -github -html -https -ifndef -inc -incomingcallback -incomingpacketcontext -incomingpacketcontext -incomingpacketid -incomingpublishcallback -ingroup -init -initalized -int -iot -iso -keepaliveseconds -keepaliveseconds -logdebug -logerror -loginfo -logwarn -lwt -mainpage -malloc -md -memset -messagecontext -messageinterface -metadata -microcontroller -min -misra -mit -mqtt -mqttagent -mqttagentcommand -mqttagentcommandcontext -mqttagentcommandinfo -mqttagentcontext -mqttagentmessagecontext -mqttagentsubscribeargs -mqttbadparameter -mqttconnectinfo -mqttcontext -mqttcontexthandle -mqtteventcallback -mqttfixedbuffer -mqttgetcurrenttimefunc -mqttkeepalivetimeout -mqttneedmorebytes -mqttnomemory -mqttnotconnected -mqttpublishinfo -mqttrecvfailed -mqttsendfailed -mqttstatecollision -mqttstatus -mqttsubscribeinfo -mqttsuccess -multithreaded -multithreading -mutex -mygetcommandimplementation -mymessagerecvimplementation -mymessagesendimplementation -myreleasecommandimplementation -networkbuffer -networkinterfacereceivestub -networkinterfacesendstub -networkrecv -networksend -noninfringement -num -numsubscriptions -org -packetid -packetreceivedinloop -packettype -packinfo -pagentcontext -param -params -pargs -passwordlength -passwordlength -payloadlength -payloadlength -pbuffer -pclientidentifier -pclientidentifier -pcmdcallbackcontext -pcmdcompletecallbackcontext -pcmdcontext -pcommand -pcommandcompletecallback -pcommandcompletecallbackcontext -pcommandinfo -pcommandtorelease -pcommandtosend -pconnectargs -pconnectinfo -pcontext -pdata -pdeserializedinfo -pendingacks -pendloop -pflags -pfuncname -pincomingcallback -pincomingcallbackcontext -pincomingpacketcontext -pingrequestcompletecb -pingresp -pmqttagentcontext -pmqttcontext -pmqttinfoparam -pmsgctx -pmsginterface -pnetworkbuffer -pnetworkcontext -poriginalcommand -posix -ppacketinfo -pparams -ppassword -ppassword -ppayload -ppayload -ppendingacks -ppublisharg -ppublishinfo -preceivedcommand -preceivedpointer -preturnflags -preturninfo -printf -processloop -psubackcodes -psubscribeargs -psubscribeinfo -psubscriptionargs -pthread -ptopicfilter -ptopicname -ptopicname -ptransportinterface -puback -pubcomp -publishcmdcompletecb -publishinfo -pubrec -pubrel -punusedarg -pusername -pvoidconnectargs -pvoidsubscribeargs -pwillinfo -qos -receiveloop -recv -releasecommand -resending -resumesession -ret -returncode -returnflags -runprocessloop -sdk -sessionpresent -sizeof -someclientid -somepassword -sometransportcontext -someusername -statusreturn -strlen -struct -structs -stubgettime -stubpublishcallback -stubreceive -stubreceivethenfail -suback -sublicense -subscribeargs -subscribecmdcompletecb -subscribeinfo -td -terminatecallback -timeoutms -todo -topicfilterlength -topicnamelength -tr -transportinterface -uint -unsuback -unsubscribeargs -unsubscribecmdcompletecb -unsubscribecompletecb -unsubscribeinfo -usernamelength -utest -uxcontrolandlengthbytes -willinfo -writev -www diff --git a/manifest.yml b/manifest.yml index 57b8a77e..615e6922 100644 --- a/manifest.yml +++ b/manifest.yml @@ -2,10 +2,18 @@ name : "coreMQTT Agent" version: "v1.2.0" description: | "Agent for thread-safe use of coreMQTT.\n" +license: "MIT" dependencies: - name : "coreMQTT" version: "v2.1.0" repository: type: "git" url: "https://github.com/FreeRTOS/coreMQTT/" -license: "MIT" + path: source/dependency/coreMQTT + + - name: "CMock" + version: "3b443e5" + repository: + type: "git" + url: " https://github.com/ThrowTheSwitch/CMock.git" + path: "test/unit-test/CMock" diff --git a/source/core_mqtt_agent.c b/source/core_mqtt_agent.c index 91db4f8b..f9ec26b5 100644 --- a/source/core_mqtt_agent.c +++ b/source/core_mqtt_agent.c @@ -1015,16 +1015,16 @@ MQTTStatus_t MQTTAgent_Init( MQTTAgentContext_t * pMqttAgentContext, pNetworkBuffer ); #if ( MQTT_AGENT_USE_QOS_1_2_PUBLISH != 0 ) + { + if( returnStatus == MQTTSuccess ) { - if( returnStatus == MQTTSuccess ) - { - returnStatus = MQTT_InitStatefulQoS( &( pMqttAgentContext->mqttContext ), - pOutgoingPublishRecords, - MQTT_AGENT_MAX_OUTSTANDING_ACKS, - pIncomingPublishRecords, - MQTT_AGENT_MAX_OUTSTANDING_ACKS ); - } + returnStatus = MQTT_InitStatefulQoS( &( pMqttAgentContext->mqttContext ), + pOutgoingPublishRecords, + MQTT_AGENT_MAX_OUTSTANDING_ACKS, + pIncomingPublishRecords, + MQTT_AGENT_MAX_OUTSTANDING_ACKS ); } + } #endif /* if ( MQTT_AGENT_USE_QOS_1_2_PUBLISH != 0 ) */ if( returnStatus == MQTTSuccess ) diff --git a/test/cbmc/proofs/MQTTAgentCommand_Connect/README.md b/test/cbmc/proofs/MQTTAgentCommand_Connect/README.md index e2f69732..089ce897 100644 --- a/test/cbmc/proofs/MQTTAgentCommand_Connect/README.md +++ b/test/cbmc/proofs/MQTTAgentCommand_Connect/README.md @@ -5,7 +5,7 @@ This directory contains a memory safety proof for MQTTAgentCommand_Connect. The proof runs within 10 seconds on a t2.2xlarge. It provides complete coverage of: * MQTTAgentCommand_Connect() - + To run the proof. ------------- @@ -14,7 +14,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgentCommand_Disconnect/README.md b/test/cbmc/proofs/MQTTAgentCommand_Disconnect/README.md index 47234ab8..05d61a0d 100644 --- a/test/cbmc/proofs/MQTTAgentCommand_Disconnect/README.md +++ b/test/cbmc/proofs/MQTTAgentCommand_Disconnect/README.md @@ -14,7 +14,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgentCommand_Ping/README.md b/test/cbmc/proofs/MQTTAgentCommand_Ping/README.md index e0e17acf..4111d84f 100644 --- a/test/cbmc/proofs/MQTTAgentCommand_Ping/README.md +++ b/test/cbmc/proofs/MQTTAgentCommand_Ping/README.md @@ -14,7 +14,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgentCommand_ProcessLoop/README.md b/test/cbmc/proofs/MQTTAgentCommand_ProcessLoop/README.md index a820f5e0..b75344d6 100644 --- a/test/cbmc/proofs/MQTTAgentCommand_ProcessLoop/README.md +++ b/test/cbmc/proofs/MQTTAgentCommand_ProcessLoop/README.md @@ -14,7 +14,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgentCommand_Publish/README.md b/test/cbmc/proofs/MQTTAgentCommand_Publish/README.md index 65f20fdb..e1bb74b1 100644 --- a/test/cbmc/proofs/MQTTAgentCommand_Publish/README.md +++ b/test/cbmc/proofs/MQTTAgentCommand_Publish/README.md @@ -14,7 +14,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgentCommand_Subscribe/README.md b/test/cbmc/proofs/MQTTAgentCommand_Subscribe/README.md index 544b1755..cc457197 100644 --- a/test/cbmc/proofs/MQTTAgentCommand_Subscribe/README.md +++ b/test/cbmc/proofs/MQTTAgentCommand_Subscribe/README.md @@ -14,7 +14,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgentCommand_Terminate/README.md b/test/cbmc/proofs/MQTTAgentCommand_Terminate/README.md index 08ce9009..6f8225eb 100644 --- a/test/cbmc/proofs/MQTTAgentCommand_Terminate/README.md +++ b/test/cbmc/proofs/MQTTAgentCommand_Terminate/README.md @@ -14,7 +14,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgentCommand_Unsubscribe/README.md b/test/cbmc/proofs/MQTTAgentCommand_Unsubscribe/README.md index 52169b09..e2d9121b 100644 --- a/test/cbmc/proofs/MQTTAgentCommand_Unsubscribe/README.md +++ b/test/cbmc/proofs/MQTTAgentCommand_Unsubscribe/README.md @@ -14,7 +14,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgent_CancelAll/README.md b/test/cbmc/proofs/MQTTAgent_CancelAll/README.md index 20cd58a3..63c69dcb 100644 --- a/test/cbmc/proofs/MQTTAgent_CancelAll/README.md +++ b/test/cbmc/proofs/MQTTAgent_CancelAll/README.md @@ -14,7 +14,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgent_CommandLoop/README.md b/test/cbmc/proofs/MQTTAgent_CommandLoop/README.md index f53c9503..3f0a8ca4 100644 --- a/test/cbmc/proofs/MQTTAgent_CommandLoop/README.md +++ b/test/cbmc/proofs/MQTTAgent_CommandLoop/README.md @@ -42,7 +42,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgent_Connect/README.md b/test/cbmc/proofs/MQTTAgent_Connect/README.md index 2d0f157d..bee6f50e 100644 --- a/test/cbmc/proofs/MQTTAgent_Connect/README.md +++ b/test/cbmc/proofs/MQTTAgent_Connect/README.md @@ -26,7 +26,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgent_Disconnect/README.md b/test/cbmc/proofs/MQTTAgent_Disconnect/README.md index ae284f06..06971a05 100644 --- a/test/cbmc/proofs/MQTTAgent_Disconnect/README.md +++ b/test/cbmc/proofs/MQTTAgent_Disconnect/README.md @@ -11,7 +11,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgent_Init/README.md b/test/cbmc/proofs/MQTTAgent_Init/README.md index 51894d01..034c966a 100644 --- a/test/cbmc/proofs/MQTTAgent_Init/README.md +++ b/test/cbmc/proofs/MQTTAgent_Init/README.md @@ -11,7 +11,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgent_Ping/README.md b/test/cbmc/proofs/MQTTAgent_Ping/README.md index 23a470dd..36ec0d20 100644 --- a/test/cbmc/proofs/MQTTAgent_Ping/README.md +++ b/test/cbmc/proofs/MQTTAgent_Ping/README.md @@ -27,7 +27,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgent_ProcessLoop/README.md b/test/cbmc/proofs/MQTTAgent_ProcessLoop/README.md index 4bedb1c2..0d2a25f2 100644 --- a/test/cbmc/proofs/MQTTAgent_ProcessLoop/README.md +++ b/test/cbmc/proofs/MQTTAgent_ProcessLoop/README.md @@ -27,7 +27,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgent_Publish/README.md b/test/cbmc/proofs/MQTTAgent_Publish/README.md index 3656baf7..6c252a12 100644 --- a/test/cbmc/proofs/MQTTAgent_Publish/README.md +++ b/test/cbmc/proofs/MQTTAgent_Publish/README.md @@ -27,7 +27,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgent_ResumeSession/README.md b/test/cbmc/proofs/MQTTAgent_ResumeSession/README.md index b9242a76..07e54593 100644 --- a/test/cbmc/proofs/MQTTAgent_ResumeSession/README.md +++ b/test/cbmc/proofs/MQTTAgent_ResumeSession/README.md @@ -36,7 +36,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgent_Subscribe/README.md b/test/cbmc/proofs/MQTTAgent_Subscribe/README.md index 0d4ad1fe..ee8f16c0 100644 --- a/test/cbmc/proofs/MQTTAgent_Subscribe/README.md +++ b/test/cbmc/proofs/MQTTAgent_Subscribe/README.md @@ -27,7 +27,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgent_Terminate/README.md b/test/cbmc/proofs/MQTTAgent_Terminate/README.md index d2c96170..8355450f 100644 --- a/test/cbmc/proofs/MQTTAgent_Terminate/README.md +++ b/test/cbmc/proofs/MQTTAgent_Terminate/README.md @@ -26,7 +26,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/proofs/MQTTAgent_Unsubscribe/README.md b/test/cbmc/proofs/MQTTAgent_Unsubscribe/README.md index 25311f61..1b53e667 100644 --- a/test/cbmc/proofs/MQTTAgent_Unsubscribe/README.md +++ b/test/cbmc/proofs/MQTTAgent_Unsubscribe/README.md @@ -27,7 +27,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles. ------------- * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. diff --git a/test/cbmc/sources/mqtt_agent_cbmc_state.c b/test/cbmc/sources/mqtt_agent_cbmc_state.c index de3548d9..da6931ad 100644 --- a/test/cbmc/sources/mqtt_agent_cbmc_state.c +++ b/test/cbmc/sources/mqtt_agent_cbmc_state.c @@ -177,6 +177,7 @@ void addPendingAcks( MQTTAgentContext_t * pContext ) for( i = 0; i < MQTT_AGENT_MAX_OUTSTANDING_ACKS; i++ ) { #ifdef MAX_PACKET_ID + /* Limit the packet Ids so that the range of packet ids retrieved through * MQTT_PublishToResend can be limited as well. */ __CPROVER_assume( packetId < MAX_PACKET_ID ); diff --git a/test/cbmc/stubs/core_mqtt_stubs.c b/test/cbmc/stubs/core_mqtt_stubs.c index ff7197dd..6c617c43 100644 --- a/test/cbmc/stubs/core_mqtt_stubs.c +++ b/test/cbmc/stubs/core_mqtt_stubs.c @@ -189,6 +189,7 @@ uint16_t MQTT_PublishToResend( const MQTTContext_t * pMqttContext, else { #ifdef MAX_PACKET_ID + /* Limit the packet Ids so that the range of packet ids so that the * probability of finding a matching packet in the pending acks is high. */ __CPROVER_assume( packetId < MAX_PACKET_ID );