Polysapce code prover C justifications
30 views (last 30 days)
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.