Polysapce code prover C justifications

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.

regards

Hrishikesh

Answer 1

[Anirban]

To justify MISRA C:2012 results, the term after polyspace should be either MISRA-C3 or MISRA2012 .

See Annotate Code and Hide Known or Acceptable Results.

[hrishikesh rajurkar]

Hi Anirban,

Thanks for the answer, now it is taking the justification, two more subquestions

a. I am observing in polyspace report eventhough the justification is accepted by polyspace, it is not affecting total number of misra violtions reported . In report , it is showing status as justified but total number of violations is same.

b. for a single line if multiple justifications for different rules are present what is the format?

<code_segment>; /* Polyspace MISRA2012:D4-1 [Justified : Low] "Pointer not outside range"*/ /* Polyspace MISRA2012:D4-11 [Justified : Low] "Some Different justification"*/

regards

Hrishikesh

[Anirban]

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.