Polyspace Code Verification
Coding Standards Report for Project: polyspace
Report Author: ctreille
Polyspace Code Verification: Coding Standards Report for Project: polyspace
by Report Author: ctreille
Published 15-Jun-2020 15:30:23
Verification Author(s): Polyspace
Polyspace Version(s): Polyspace Code Prover 10.3 (R2020b)
Project Version(s): 1.0
Result Folder(s):
C:\qualkits_R2020b\iec\codeprover\tests\code-prover-results\reporting\template-codingstandards\OR-414-6-codingstandards_7
Table of Contents
Chapter 1. Appendix 1 - Configuration Settings ....................................................................................................................................................................................... 1
Polyspace Settings ............................................................................................................................................................................................................................... 1
Analysis Assumptions ................................................................................................................................................................................................................. 1
Files with compilation errors (files partially analyzed) .................................................................................................................................................................... 2
Chapter 2. Appendix 2 - Definitions ............................................................................................................................................................................................................ 3
................................................................................................................................................................................................................................................................. 3
i
Chapter 1. Appendix 1 - Configuration Settings
Polyspace Settings
Option Value
-author Polyspace
-compiler generic
-date 15/06/2020
-I C:\qualkits_R2020b\iec\codeprover\tests\options-api\lib
-lang CPP
-O2 -O2
-prog polyspace
-results-dir C:\qualkits_R2020b\iec\codeprover\tests\code-prover-results\reporting\template-codingstandards\OR-414-6-codingstandards_7
-target i386
-to pass2
-verif-version 1.0
Analysis Assumptions
Assumption Issuer
External arrays of unspecified size can be safely accessed at any index Product
Nonfinite floats (infinities and NaNs) are not considered Product
Computations involving unsigned integers do not overflow Product
Results of floating-point arithmetic are rounded following the IEE754 rule: round to nearest, ties to even Product
Structure fields are not volatile unless the entire structure is volatile-qualified Product
Stack pointers can be safely dereferenced even outside the pointed variable's scope Product
External pointers cannot be null. They point to allocated data of sufficient size for safe dereference Product
Absolute addresses can be safely dereferenced Product
1
Files with compilation errors (files partially analyzed)
Table 1.1. Files with compilation errors (files partially analyzed)
File
C:\qualkits_R2020b\iec\codeprover\tests\reporting\template-codingstandards\OR-414-6-codingstandards_7.cpp
2
Chapter 2. Appendix 2 - Definitions
Table 2.1. Abbreviations
Abbreviation Definition
Col Column
Jus Justified
SQO Software Quality Objectives
NA Not Available