MATLAB: Polysapce code prover C justifications

Question

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

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.