From dcfe37b9f3c3ca0c03bc9de8370bfc500c05aa8e Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Mon, 29 Jan 2024 10:31:35 -0500 Subject: [PATCH 01/12] Onboard to CI-CD Workflows --- .github/.cSpellWords.txt | 174 +++++++++++++++++++ .github/workflows/ci.yml | 123 ++++++++++--- .github/workflows/formatting.yml | 23 +++ cspell.config.yaml | 22 +++ lexicon.txt | 290 ------------------------------- 5 files changed, 316 insertions(+), 316 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 0000000..69262e5 --- /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 511fd2b..7041696 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,78 @@ 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*' + + 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 - run: | - # We don't need to generate the coreMQTT docs, we only need the tag file. We can just download it. - 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" + - uses: actions/checkout@v3 - 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,18 +121,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: + if: ${{ github.event.pull_request }} || ${{ github.event.workflow }} runs-on: cbmc_ubuntu-latest_64-core steps: - name: Set up CBMC runner @@ -114,3 +184,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 0000000..04786ba --- /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 0000000..e7d8a56 --- /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 89913d6..0000000 --- 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 From 53ac77733f043dd54beffa4804977eed23aacda3 Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Mon, 29 Jan 2024 10:46:59 -0500 Subject: [PATCH 02/12] Use ubuntu latest for CBMC now that the default runner is multicore. --- .github/workflows/ci.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7041696..24fd76c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -175,8 +175,7 @@ jobs: fail-on-incorrect-version: true proof_ci: - if: ${{ github.event.pull_request }} || ${{ github.event.workflow }} - 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 From d418d2ad2ebedee4a67e634bc3bc7c47bd2e18d1 Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Mon, 29 Jan 2024 10:49:28 -0500 Subject: [PATCH 03/12] Fix broken link in CBMC proofs --- test/cbmc/proofs/MQTTAgentCommand_Connect/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_Disconnect/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_Ping/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_ProcessLoop/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_Publish/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_Subscribe/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_Terminate/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_Unsubscribe/README.md | 2 +- test/cbmc/proofs/MQTTAgent_CancelAll/README.md | 2 +- test/cbmc/proofs/MQTTAgent_CommandLoop/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Connect/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Disconnect/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Init/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Ping/README.md | 2 +- test/cbmc/proofs/MQTTAgent_ProcessLoop/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Publish/README.md | 2 +- test/cbmc/proofs/MQTTAgent_ResumeSession/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Subscribe/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Terminate/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Unsubscribe/README.md | 2 +- 20 files changed, 20 insertions(+), 20 deletions(-) diff --git a/test/cbmc/proofs/MQTTAgentCommand_Connect/README.md b/test/cbmc/proofs/MQTTAgentCommand_Connect/README.md index e2f6973..7ceb697 100644 --- a/test/cbmc/proofs/MQTTAgentCommand_Connect/README.md +++ b/test/cbmc/proofs/MQTTAgentCommand_Connect/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_Disconnect/README.md b/test/cbmc/proofs/MQTTAgentCommand_Disconnect/README.md index 47234ab..1bf3a68 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 e0e17ac..52257f9 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 a820f5e..ac91521 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 65f20fd..0167584 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 544b175..51dd272 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 08ce900..2a4f0a8 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 52169b0..622fb35 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 20cd58a..5389ebf 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 f53c950..f705145 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 2d0f157..4aec4c0 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 ae284f0..c475302 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 51894d0..d87341b 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 23a470d..96bfb4f 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 4bedb1c..bad3f32 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 3656baf..c2bf23f 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 b9242a7..13ca565 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 0d4ad1f..dbde539 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 d2c9617..ab4f476 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 25311f6..ef0aceb 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. From d527914d974874896295066d6389981873449eb0 Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Mon, 29 Jan 2024 10:51:01 -0500 Subject: [PATCH 04/12] Add the path to the manifest file --- manifest.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/manifest.yml b/manifest.yml index 57b8a77..c4cb79d 100644 --- a/manifest.yml +++ b/manifest.yml @@ -2,10 +2,11 @@ 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 From 411bb1f32e52f238217689b36d5ccf79a0d886ac Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Mon, 29 Jan 2024 10:52:06 -0500 Subject: [PATCH 05/12] Ignore the coreMQTT source files in the coverage check --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 24fd76c..c87b741 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -56,7 +56,7 @@ jobs: 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*' + lcov --rc lcov_branch_coverage=1 -r build/coverage.info -o build/coverage.info '*test*' '*CMakeCCompilerId*' '*mocks*' 'coreMQTT/*' echo "::endgroup::" lcov --rc lcov_branch_coverage=1 --list build/coverage.info From 876025d8955b7e4d6f321c7682df7f046c148ed7 Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Mon, 29 Jan 2024 10:55:29 -0500 Subject: [PATCH 06/12] Add CMock to the manifest --- manifest.yml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/manifest.yml b/manifest.yml index c4cb79d..615e692 100644 --- a/manifest.yml +++ b/manifest.yml @@ -10,3 +10,10 @@ dependencies: type: "git" url: "https://github.com/FreeRTOS/coreMQTT/" path: source/dependency/coreMQTT + + - name: "CMock" + version: "3b443e5" + repository: + type: "git" + url: " https://github.com/ThrowTheSwitch/CMock.git" + path: "test/unit-test/CMock" From df8049b992294a7c217764530ab31708c9f8f8ca Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Mon, 29 Jan 2024 10:56:10 -0500 Subject: [PATCH 07/12] Exclude 'dependency' instead of 'coreMQTT' as that match didn't work --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c87b741..4238665 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -56,7 +56,7 @@ jobs: 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*' 'coreMQTT/*' + 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 From 25d13458b19c3f072e1009e1ee691028e708d3ed Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Mon, 29 Jan 2024 10:58:46 -0500 Subject: [PATCH 08/12] Recurse submodules when doing doxygen as coreMQTT is needed for the doxygen output --- .github/workflows/ci.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4238665..883310b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -81,6 +81,8 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v3 + with: + submodules: recursive - name: Run doxygen build uses: FreeRTOS/CI-CD-Github-Actions/doxygen@main with: From 1404d613b44338239736572e80f3c1d67e1c1e7d Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Mon, 29 Jan 2024 10:59:45 -0500 Subject: [PATCH 09/12] Apply formatting changes --- source/core_mqtt_agent.c | 16 ++++++++-------- .../proofs/MQTTAgentCommand_Connect/README.md | 2 +- test/cbmc/sources/mqtt_agent_cbmc_state.c | 1 + test/cbmc/stubs/core_mqtt_stubs.c | 1 + 4 files changed, 11 insertions(+), 9 deletions(-) diff --git a/source/core_mqtt_agent.c b/source/core_mqtt_agent.c index 91db4f8..f9ec26b 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 7ceb697..6fa14ad 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. ------------- diff --git a/test/cbmc/sources/mqtt_agent_cbmc_state.c b/test/cbmc/sources/mqtt_agent_cbmc_state.c index de3548d..da6931a 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 ff7197d..6c617c4 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 ); From 161f4229c76bc189467fc8c49f6cc52a7be6f353 Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Mon, 29 Jan 2024 11:07:56 -0500 Subject: [PATCH 10/12] Remove trailing slash in CBMC proof url --- test/cbmc/proofs/MQTTAgentCommand_Connect/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_Disconnect/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_Ping/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_ProcessLoop/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_Publish/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_Subscribe/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_Terminate/README.md | 2 +- test/cbmc/proofs/MQTTAgentCommand_Unsubscribe/README.md | 2 +- test/cbmc/proofs/MQTTAgent_CancelAll/README.md | 2 +- test/cbmc/proofs/MQTTAgent_CommandLoop/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Connect/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Disconnect/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Init/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Ping/README.md | 2 +- test/cbmc/proofs/MQTTAgent_ProcessLoop/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Publish/README.md | 2 +- test/cbmc/proofs/MQTTAgent_ResumeSession/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Subscribe/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Terminate/README.md | 2 +- test/cbmc/proofs/MQTTAgent_Unsubscribe/README.md | 2 +- 20 files changed, 20 insertions(+), 20 deletions(-) diff --git a/test/cbmc/proofs/MQTTAgentCommand_Connect/README.md b/test/cbmc/proofs/MQTTAgentCommand_Connect/README.md index 6fa14ad..089ce89 100644 --- a/test/cbmc/proofs/MQTTAgentCommand_Connect/README.md +++ b/test/cbmc/proofs/MQTTAgentCommand_Connect/README.md @@ -14,7 +14,7 @@ To run the proof. * Run `make`. * Open html/index.html in a web browser. -To use [`arpa`](https://awslabs.github.io/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 1bf3a68..05d61a0 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://awslabs.github.io/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 52257f9..4111d84 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://awslabs.github.io/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 ac91521..b75344d 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://awslabs.github.io/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 0167584..e1bb74b 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://awslabs.github.io/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 51dd272..cc45719 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://awslabs.github.io/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 2a4f0a8..6f8225e 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://awslabs.github.io/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 622fb35..e2d9121 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://awslabs.github.io/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 5389ebf..63c69dc 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://awslabs.github.io/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 f705145..3f0a8ca 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://awslabs.github.io/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 4aec4c0..bee6f50 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://awslabs.github.io/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 c475302..06971a0 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://awslabs.github.io/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 d87341b..034c966 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://awslabs.github.io/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 96bfb4f..36ec0d2 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://awslabs.github.io/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 bad3f32..0d2a25f 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://awslabs.github.io/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 c2bf23f..6c252a1 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://awslabs.github.io/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 13ca565..07e5459 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://awslabs.github.io/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 dbde539..ee8f16c 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://awslabs.github.io/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 ab4f476..8355450 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://awslabs.github.io/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 ef0aceb..1b53e66 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://awslabs.github.io/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. From 5dc2451257f1a5596c11739f1dc540b07143209a Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Mon, 29 Jan 2024 14:12:28 -0500 Subject: [PATCH 11/12] Use the github hosted MQTT doxygen to see if that fixes the issue --- docs/doxygen/config.doxyfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/doxygen/config.doxyfile b/docs/doxygen/config.doxyfile index 6d3b59d..decc91d 100644 --- a/docs/doxygen/config.doxyfile +++ b/docs/doxygen/config.doxyfile @@ -2368,7 +2368,7 @@ SKIP_FUNCTION_MACROS = YES # the path). If a tag file is not located in the directory in which doxygen is # run, you must also specify the path to the tagfile here. -TAGFILES = source/dependency/coreMQTT/docs/doxygen/output/mqtt.tag=https://freertos.org/Documentation/api-ref/coreMQTT/docs/doxygen/output/html +TAGFILES = source/dependency/coreMQTT/docs/doxygen/output/mqtt.tag=https://freertos.github.io/coreMQTT/v2.1.0/index.html # When a file name is specified after GENERATE_TAGFILE, doxygen will create a # tag file that is based on the input files it reads. See section "Linking to From b34d8050df72f200b10b0b1d2609796b6d50a091 Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Mon, 29 Jan 2024 14:42:39 -0500 Subject: [PATCH 12/12] Add the removed step to the workflow to download the tag, revert the doxyfile change --- .github/workflows/ci.yml | 15 +++++++++++++-- docs/doxygen/config.doxyfile | 2 +- 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 883310b..cc4fd6c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -81,8 +81,19 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v3 - with: - submodules: recursive + + - 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: diff --git a/docs/doxygen/config.doxyfile b/docs/doxygen/config.doxyfile index decc91d..6d3b59d 100644 --- a/docs/doxygen/config.doxyfile +++ b/docs/doxygen/config.doxyfile @@ -2368,7 +2368,7 @@ SKIP_FUNCTION_MACROS = YES # the path). If a tag file is not located in the directory in which doxygen is # run, you must also specify the path to the tagfile here. -TAGFILES = source/dependency/coreMQTT/docs/doxygen/output/mqtt.tag=https://freertos.github.io/coreMQTT/v2.1.0/index.html +TAGFILES = source/dependency/coreMQTT/docs/doxygen/output/mqtt.tag=https://freertos.org/Documentation/api-ref/coreMQTT/docs/doxygen/output/html # When a file name is specified after GENERATE_TAGFILE, doxygen will create a # tag file that is based on the input files it reads. See section "Linking to