Leverage Semantic Analysis of Polyspace Tools to Automatically Justify MISRA Violations
By Ram Cherukuri, Stefan David
MISRA standard is a widely adopted coding standard across industries. It has become a commonplace best practice among embedded software development and quality assurance groups. A lot of these groups have a strict adherence policy to at least a subset of applicable rules—if not all of the coding rules. Such a compliance policy would require a review process to address the violations of the coding rules, and this process can often be resource intensive.
A systematic MISRA compliance process would include a static analysis tool that can detect coding rule violations. This could be in the form of making changes to the code in order to comply with the coding rules or reviewing the violations to justify them appropriately. Then there would be a process to handle the deviations (MISRA standard requires a process to justify the deviations). This could be in the form of modifying the code to comply with the coding rules or to justify the deviation.
Once you have identified the coding rule violations, you can manually analyze the violations and choose to fix the issue or provide a justification. The justification is essentially for documenting that the coding rule violation would not have any side effects. Hence, it can be quite resource intensive depending on a few factors such as:
- Are you developing new code or tweaking legacy code? The latter can be a nightmare.
- At what stage of the development process are you checking for compliance? It gets more expensive the later it is in the development process.
- Who is running the analysis and who is reviewing the results? This is related to the compliance question above. It is effective if the developers run the analysis and address the issues instead of the QA group running an analysis at the end and sending a report to the developers to address the issues. In our discussions with customers, we found that it is difficult for QA teams to validate the justifications to the MISRA violations provided by the developers.
But what if you could reduce these challenges—the time and effort required to address such violations? How, do you ask? What if you can have access to detailed information on the operations that violate certain MISRA rules and that prove those particular operations to be safe for all possible runtime scenarios and, therefore, have no side effects (spirit of the underlying MISRA rule)?
Well, this is possible with the Polyspace static analysis solution, and it’s only possible because of the ability of Polyspace Code Prover to formally prove. The ability to prove that a particular operation is safe and reliable for every possible path of execution—for every possible control and data flow possible through your program—implies that even if an operation violates a certain coding rule, there is no work needed to make any changes to the code or to go back and forth between teams on how to justify. You simply point to the proof from the Code Prover verification as your justification.
Let’s look at some example code here, where we are adding two integer types of different underlying sizes (int 32 and unsigned int 16), which would result in implicit conversion and, therefore, would violate MISRA rule 10.1. But, as you can see in the image below, the addition operation cannot result in an overflow (side effect). Therefore, there is no work to be done except for capturing the justification in your report.
This is possible only for a subset of MISRA rules that maps to the underlying runtime checks verified by Polyspace Code Prover. This process has enabled some of our customers to reduce their effort by as much as 20% in conservative terms. If you are interested in finding out more about this topic or finding the list of MISRA rules that maps to the various checks, you can contact the authors.
Ask the Expert
Puneet Lal Polyspace Static Analysis Notes Contact Expert