Polysapce code prover C justifications

30 views (last 30 days)
hrishikesh rajurkar
hrishikesh rajurkar on 22 Feb 2021
Edited: Anirban on 24 Feb 2021
Hello Members,
I am running polyspace code prover R2019B for C with configuration as source code : c version :c11 compiler:gnu7.x target : x86_64
check for misra c :2012 , where for some findings i am trying to justify but polyspace is not taking those justification in generated report.
The jsutification formats i have tried are <code segmeny>; /* polyspace <MISRA-C: 9.1 :Low:Justified>"Value upated in preceding function call"*/
<code_segment>; /* polyspace MISRA-C:D4.11[Justified:Low]"Due to if check amount of memory to copied is within range" */
<code_segment>; /* Polyspace MISRA-C2012:D4.1 [Justified : Low] "Pointer not outside range"*/
<code_segment>; /* Polyspace MISRA-C-2012:D4-1 [Justified : Low] "Pointer not outside range"*/
here code_segment is single line of code for which issue is reported
But it is taking none of these.
Please let me know how to proceed.

Accepted Answer

Anirban on 22 Feb 2021
To justify MISRA C:2012 results, the term after polyspace should be either MISRA-C3 or MISRA2012 .
Anirban on 24 Feb 2021
a. By 'report', do you mean the PDF or Word reports or do you mean just the results list in the Polyspace user interface? To hide results that are justified in code from the list in the Polyspace user interface, on the Showing menu at the top, check the box titled Hide results justified in code. The results justified in code will disappear from view. See more details in Address Results Through Bug Fixes or Justifications.
About the PDF or Word reports, those are typically meant for certification, so all results are shown (along with justifications). However, there is a provision to create a filtered report. Once you have justified results like the above in the Polyspace user interface, when generating a report (Reporting > Run Report), you can choose to display only the results that are not hidden. See more details in Generate Reports. The report covers will clearly indicate that the report is filtered.
b. Your suggested format works. You can compress them slightly into one comment as:
<code_segment>; /* Polyspace MISRA2012:D4-1 [Justified : Low] "Pointer not outside range" Polyspace MISRA2012:D4-11 [Justified : Low] "Some Different justification"*/
Each mention of 'Polyspace' starts a new justification.

Sign in to comment.

More Answers (0)

Community Treasure Hunt

Find the treasures in MATLAB Central and discover how the community can help you!

Start Hunting!

Translated by