1
0
mirror of https://github.com/FreeRTOS/coreMQTT synced 2025-06-25 04:52:33 +08:00
Dakshit Babbar 8ec72d6ef7
Add CBMC Proofs for the new APIs (#315)
Description
-----------
This PR:
Adds CBMC proofs for the new APIs added for publish retransmits in #308 

Test Steps
-----------
Proofs run without any errors or warnings

Checklist:
----------
- [x] I have tested my changes. No regression in existing tests.
- [x] I have modified and/or added unit-tests to cover the code changes
in this Pull Request.

Related Issue
-----------
<!-- If any, please provide issue ID. -->
By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

---------

Co-authored-by: DakshitBabbar <dakshba@amazon.com>
Co-authored-by: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
2025-03-05 16:49:34 +05:30
..

Static code analysis for coreMQTT Library

This directory is made for the purpose of statically testing the MISRA C:2012 compliance of coreMQTT Library using Synopsys Coverity static analysis tool. To that end, this directory provides a configuration file to use when building a binary for the tool to analyze.

Note

For generating the report as outlined below, we have used Coverity version 2021.12.

For details regarding the suppressed violations in the report (which can be generated using the instructions described below), please see the MISRA.md file.

Getting Started

Prerequisites

You can run this on a platform supported by Coverity. The list and other details can be found here. To compile and run the Coverity target successfully, you must have the following:

  1. CMake version > 3.13.0 (You can check whether you have this by typing cmake --version)
  2. GCC compiler
    • You can see the downloading and installation instructions here.
  3. Download the repo and include the submodules using the following commands.
    • git clone --recurse-submodules git@github.com:FreeRTOS/coreMQTT.git ./coreMQTT
    • cd ./coreMQTT
    • git submodule update --checkout --init --recursive

To build and run coverity:

Go to the root directory of the library and run the following commands in terminal:

  1. Create a local directory for the configuration files
mkdir covConfig
  1. Update the compiler configuration in Coverity
cov-configure --config covConfig/coverity.xml --compiler cc --comptype gcc --template
  1. Create the build files using CMake in a build directory
cmake -B build -S test
  1. Go to the build directory and copy the coverity configuration file
cd build/
  1. Build the static analysis target
cov-build --config ../covConfig/coverity.xml --emit-complementary-info --dir cov-out make coverity_analysis
  1. Go to the Coverity output directory (cov-out) and begin Coverity static analysis
cd cov-out/
cov-analyze --dir . --coding-standard-config ../../tools/coverity/misra.config --tu-pattern "file('.*/source/.*')"
  1. Format the errors in HTML format so that it is more readable while removing the test and build directory from the report
cov-format-errors --dir . --file "source" --exclude-files '(/build/|/test/)' --html-output html-out;
  1. Format the errors in JSON format to perform a jq query to get a simplified list of any exceptions. NOTE: A blank output means there are no defects that aren't being suppressed by the config or inline comments.
cov-format-errors --dir . --file "source" --exclude-files '(/build/|/test/)' --json-output-v2 defects.json;
echo -e "\n-------------------------Non-Suppresed Deviations, if any, Listed Below-------------------------\n";
jq '.issues[] | .events[] | .eventTag ' defects.json | sort | uniq -c | sort -nr;
 echo -e "\n-------------------------Non-Suppresed Deviations, if any, Listed Above-------------------------\n";

For your convenience the commands above are below to be copy/pasted into a UNIX command friendly terminal.

mkdir covConfig
cov-configure --config covConfig/coverity.xml --compiler cc --comptype gcc --template
cmake -B build -S test;
cd build/;
cov-build --config ../covConfig/coverity.xml --emit-complementary-info --dir cov-out make coverity_analysis
cd cov-out/
cov-analyze --dir . --coding-standard-config ../../tools/coverity/misra.config --tu-pattern "file('.*/source/.*')";
cov-format-errors --dir . --file "source" --exclude-files '(/build/|/test/)' --html-output html-out;
cov-format-errors --dir . --file "source" --exclude-files '(/build/|/test/)' --json-output-v2 defects.json;
echo -e "\n-------------------------Non-Suppresed Deviations, if any, Listed Below-------------------------\n";
jq '.issues[] | .events[] | .eventTag ' defects.json | sort | uniq -c | sort -nr;
echo -e "\n-------------------------Non-Suppresed Deviations, if any, Listed Above-------------------------\n";
cd ../../;

You should now have the HTML formatted violations list in a directory named build/cov-out/html-output. With the current configuration and the provided project, you should not see any deviations.