PolySpace
Reference
®
Products for C++ 7
How to Contact The MathWorks
www.mathworks.
comp.soft-sys.matlab Newsgroup
www.mathworks.com/contact_TS.html T echnical Support
suggest@mathworks.com Product enhancement suggestions
bugs@mathwo
doc@mathworks.com Documentation error reports
service@mathworks.com Order status, license renewals, passcodes
info@mathwo
com
rks.com
rks.com
Web
Bug reports
Sales, prici
ng, and general information
508-647-7000 (Phone)
508-647-7001 (Fax)
The MathWorks, Inc.
3 Apple Hill Drive
Natick, MA 01760-2098
For contact information about worldwide offices, see the MathWorks Web site.
®
PolySpace
© COPYRIGHT 1999–20 10 by The MathWorks, Inc.
The software described in this document is furnished under a license agreement. The software may be used
or copied only under the terms of the license agreement. No part of this manual may be photocopied or
reproduced in any form without prior written consent from The MathW orks, Inc.
FEDERAL ACQUISITION: This provision applies to all acquisitions of the Program and Documentation
by, for, or through the federal government of the United States. By accepting delivery of the Program
or Documentation, the government hereby agrees that this software or documentation qualifies as
commercial computer software or commercial computer software documentation as such terms are used
or defined in FAR 12.212, DFARS Part 227.72, and DFARS 252.227-7014. Accordingly, the terms and
conditions of this Agreement and only those rights specified in this Agreement, shall pertain to and govern
theuse,modification,reproduction,release,performance,display,anddisclosureoftheProgramand
Documentation by the federal government (or other entity acquiring for or through the federal government)
and shall supersede any conflicting contractual terms or conditions. If this License fails to meet the
government’s needs or is inconsistent in any respect with federal procurement law, the government agrees
to return the Program and Docu mentation, unused, to The MathWorks, Inc.
Trademarks
MATLAB and Simulink are registered trademarks of The MathWorks, Inc. See
www.mathworks.com/trademarks for a list of additional trademarks. Other product or brand
names may be trademarks or registered trademarks of their respective holders.
Patents
The MathWorks products are protected by one or more U.S. patents. Please see
www.mathworks.com/patents for more information.
Revision History
March 2009 Online Only Revised for Version 7.0 (Release 2009a)
September 2009 Online Only Revised for Version 7.1 (Release 2009b)
March 2010 Online Only Revised for Version 7.2 (Release 2010a)
Products for C++ Reference
Options Description
1
Overview ......................................... 1-2
Contents
Sources/Includes
-results-dir Results_Directory
-sources files or -sources-list-file file_name
-I directory
General
Overview
-prog Session identifier
-date Date
-author Author
-verif-version Version
-keep-all-files
-continue-with-existing-host (Deprecated)
-allow-unsupported-linux (Deprecated)
Report Generation
Targets/Compilers
-target TargetProcessorType
GENERIC ADVANCE D TARGET OPTIONS
-OS-target OperatingS ystemTarget
-D compiler-flag
-U compiler-flag
-include file1[,file2[,...]]
-post-preprocessing-command "command"
-post-analysis-command <file_name> or "command"
........................................... 1-6
........................................ 1-6
.................................. 1-3
....................... 1-3
............. 1-3
....................................... 1-5
............................. 1-6
....................................... 1-7
.................................... 1-7
.............................. 1-7
..................................... 1-8
.............. 1-8
................ 1-9
................................. 1-9
................................. 1-12
........................ 1-12
................... 1-19
................................... 1-19
................................... 1-20
............................. 1-20
............. 1-21
........... 1-13
..... 1-22
Compliance with Standards
-dos
............................................. 1-24
Embedded Assembler
-wchar-t-is-unsigned-long
-size-t-is-unsigned-long
-no-extern-C
...................................... 1-26
.............................. 1-25
............................. 1-26
........................ 1-24
........................... 1-26
iii
-no-stl-stubs ...................................... 1-27
-dialect DialectName
-wchar-t-is
-for-loop-index-scope
-ignore-pragma-pack
Visual Specific Options
Coding Rules Checker
-ignore-constant-overflows
-allow-undef-variables
-allow-negative-operand-in-shift
-Wall
....................................... 1-28
............................................ 1-36
............................... 1-27
............................... 1-28
............................... 1-29
............................. 1-30
.............................. 1-31
.......................... 1-35
.............................. 1-35
..................... 1-36
PolySpace Inner Settings
-unit-by-unit
-unit-by-unit-common-source filename
-main sub_program_name
Generate a Main Using a Given Class
-main-generator-calls
General options for the generation of mains
-data-range-specifications file_name
-no-automatic-stubbing
-ignore-float-rounding
-detect-unsigned-overflows
-enum-type-definition
-machine-architecture
-max-processes
-extra-flags option-extra-flag
-cpp-extra-flags flag
-il-extra-flags flag
Precision/Scaling
-quick (Deprecated)
-O(0-3)
-from verification-phase
-to verification-phase
-context-sensitivity "proc1[,p r oc2 [ ,.. .]] "
-context-sensitivity-auto
-path-sensitivity-delta number
-k-limiting number
-inline "proc1[,proc2[,...]]"
-respect-types-in-globals
-respect-types-in-fields
-less-range-information
..................................... 1-37
.................................... 1-51
................................. 1-52
.................................. 1-54
.......................................... 1-55
........................... 1-37
.......................... 1-38
.............................. 1-42
............................. 1-47
.............................. 1-47
.......................... 1-49
.............................. 1-50
.............................. 1-50
........................ 1-52
............................... 1-52
................................ 1-54
............................ 1-56
.............................. 1-57
............................ 1-58
....................... 1-59
................................ 1-59
........................... 1-60
............................ 1-61
............................. 1-61
............................. 1-62
................ 1-38
................. 1-39
............ 1-43
.................. 1-46
................ 1-58
iv Contents
-no-pointer-information ............................. 1-63
Tuning Precision and Scaling Parameters
............. 1-64
MultiTasking (PolySpace Server for C/C++ Only)
-entry-points str1[,str2[,...]]
-critical-section-[begin or end] "proc1:cs1[,proc2:cs2]"
-temporal-exclusions-file file_name
Specific Batch Options
-server server_name_or_ip[:port_number]
-sources-list-file file_name
-v | -version
-h[elp]
...................................... 1-70
........................................... 1-70
......................... 1-66
................... 1-67
............................. 1-69
.............. 1-69
.......................... 1-70
Check Descriptions
2
Check Categories .................................. 2-2
Acronyms associated to C++ specific constructions:
Acronym Not Related to C++ Constructions (Also Used for
C Code):
Colored Source Code for C++
Function Returns a value: FRV
Non Null this-pointer: NNT
Positive Array Size: CPP
Incorrect typeid Argument: CPP
Incorrect dynamic_cast on Pointer: C PP
Incorrect dynamic_cast on Reference: CPP
Invalid Pointer to Member: OOP
Call of Pure Virtual Function: OOP
Incorrect Type for this-pointer: OOP
PotentialCallto:INF
Non-Initialized Variable: NIV/NIVL
Non-Initialized Pointer: NIP
User Assertion Failure: ASRT
Overflows and Underflows
Scalar or Float Division by zero: ZDV
Shift Amount is Outside its Bounds: SHF
....................................... 2-7
....................... 2-10
...................... 2-11
......................... 2-12
........................... 2-14
..................... 2-15
............... 2-16
............. 2-18
..................... 2-19
................... 2-20
.................. 2-21
.............................. 2-24
.................. 2-26
........................ 2-27
....................... 2-28
.......................... 2-30
................. 2-34
.............. 2-35
...... 2-2
..... 1-66
.... 1-66
v
3
Left Operand of Left Shift is Negative: SHF ............ 2-36
POW (Deprecated)
Array Index is Outside its Bounds: O BA I
Function Pointer Must Point to a Valid Function: COR
Wrong Number of Arguments: COR
Wrong Type of Argument: COR
PointerisOutsideitsBounds:IDP
Function throws: EXC
Call to Throws: EXC
Destructor or Delete Throws: EXC
Main, Tasks or C Library Function Throws: EXC
Exception Raised is Not Specified in the Throw List:
EXC
.......................................... 2-58
Throw During Catch Parameter Construction: EXC
Continue Execution in __except: EXC
Unreachable Code: UNR
Non Terminations: Calls and Loops
................................. 2-38
.............. 2-38
... 2-39
.................. 2-40
...................... 2-41
................... 2-42
............................. 2-50
............................... 2-52
................... 2-54
....... 2-56
..... 2-60
................. 2-62
........................... 2-63
.................. 2-65
Approximations Used During Verification
vi Contents
Why PolySpace Verification Uses Approximations .... 3-2
What is Static Verification
Exhaustiveness
Approximations Made by PolySpace Verification
Volatile Variables
Structures with Volatile Fields
Absolute Addre sses
Pointer Comparison
Left Shift on Negative Variables
Bitfields
Shared Variables
Trigonometric Function s
Unions
Constant Pointer
......................................... 3-6
.......................................... 3-7
................................... 3-3
................................. 3-4
................................ 3-5
.................................. 3-6
.................................. 3-8
.......................... 3-2
..... 3-4
...................... 3-4
............................... 3-5
..................... 3-5
............................ 3-7
Options Description
• “Overview” on page 1-2
• “Sources/Includes” on page 1-3
• “General” on page 1-6
• “Targets/Compilers” on page 1-12
• “Compliance with Standards” on page 1-24
• “PolySpace Inner Settings” on page 1-37
• “Precision/Scaling” on page 1-54
1
• “MultiTasking (PolySpace Server for C/C++ Only)” on page 1-66
• “Specific Batch Options” on page 1-69
1 Options Description
Overview
This chapter describes all options available within PolyS pace®software. All of
these options with the exception of the multitasking options are accessible
through the graphical user interface of the PolySpace Launcher.
They can also be accessed with the associated batch command
polyspace-cpp.
1-2
Sources/Includes
In this section...
“-results-dir Results_Directory” on page 1-3
“-sources files or -sources-list-file file_name” on page 1-3
“-I directory” on page 1-5
-results-dir Results_Directory
This option specifies the directory in which PolySpace will write the results
of the verification. Note that although relative directories may be specified,
particular care should be tak en with their use especially where the tool is to
be launched remotely over a network, and/or where a project configuration file
is to be copied using the "Save as" option.
Default:
Sources/Includes
Shell Script: The directory i n which tool is launched.
From Graphical User Interface: C:\PolySpace_Results
Example Shell Script Entry:
polyspace-cpp -results-dir RESULTS ...
export RESULTS=results_`date +%d%B_%HH%M_%A`
polyspace-cpp -results-dir `pwd`/$RESULTS ...
-sources files or -sources-list-file file_name
-sources "file1[ file2[ ...]]" (Linux
or
-sources "file1[,file2[, ...]]" (Windows
or
®
and Solaris™)
®
, Linux and Solaris)
1-3
1 Options Description
-sources-list-file file_name (not a graphical option)
List of source files to be analyzed, double-quoted and separated by commas.
Note that UNIX
®
standard wild cards are available to specify a number of files.
Note The specified files must have valid extensions. The extensions are not
case-sensitive:
*.(c|C|cc|cpp|cPp|CPP|cxx|CxX|CXX)
Defaults:
sources/*.(c|C|cc|cpp|cPp|CPP|cxx|CxX|CXX)
Example Shell Script Entry under linux or solaris (files are separated
with a white space):
polyspace-cpp -sources "my_directory/*.cpp"
polyspace-cpp -sources "my_directory/file1.cc other_dir/file2.cpp"
Example Shell Script Entry under windows (files are separated with a
comma):
polyspace-cpp -sources "my_directory/file1.cpp,other_dir/file2.cc"
Using -sources-list-file, each file name needtobegivenwithanabsolutepath.
Moreover, the syntax of the file is the following:
1-4
• Onefilebyline.
• Each file name is given with its absolute path.
Note This option is only available in batch mode.
Example Shell Script Entry for -sources-list-file:
polyspace-cpp -sources-list-file "C:\Analysis\files.txt"
polyspace-cpp -sources-list-file "/home/poly/files.txt"
-I directory
This option is us
compiling C++ so
the option can b
Default:
Sources/Includes
ed to specify the name of a directory to be included when
urces. Only one directory may be specified for each –I, but
eusedmultipletimes.
• When no direct
it exists) is
• If several in
implicitly
Example She
polyspace
is equival
polyspac
Example
polyspa
is equi
valent to
polysp
automatically included
clude-dir are mentioned, the ./sources directory (if it exists), is
added at the end of the "-I" list
ll Script Entry-1:
-cpp -I /com1/inc -I /com1/sys/inc
ent to
e-cpp -I /com1/inc -I /com1/sys/inc -I ./sources
Shell Script Entry-2:
ce-cpp
ace-cpp -I ./sources
ory is specified using this option, the ./sources directory (if
1-5
1 Options Description
General
In this section...
“Overview” on page 1-6
“-prog Session identifier” on page 1-6
“-date Date” on page 1-7
“-author Author” on page 1-7
“-verif-version Version” on page 1-7
“-keep-all-files” on page 1-8
“-continue-with-existing-host (Deprecated)” on page 1-8
“-allow-unsupported-linux (Deprecated)” on page 1-9
“Report Generation” on page 1-9
Overview
This section collates all options relating to the identification of the verification,
including the destination directory for the results and sources.
1-6
-prog S ession identifier
This option specifies the application name, using only the characters which
are valid for Unix file names. This information is labelled in the GUI as the
Session Identifier.
Default:
Shell Script: polyspace
GUI: New_Project
Example shell script entry:
polyspace-cpp -prog myApp ...
-date Date
This optio n spec
This informatio
alternative de
Default:
fault date formats, via the Edit/Preferences window.
General
ifies a date stamp for the verification in dd/mm/yyyy format.
n is labelled in the GUI as the Date.TheGUIalsoallows
Day of launchi
Example shel
polyspace-
-author Au
This optio
Default:
the name o
Example
polyspa
-verif
Speci
ident
the Ve
Defa
nisusedtospecifythenameoftheauthoroftheverification.
shell script entry:
-version Version
fies the version identifier of the verification. This option can be used to
ify d ifferent verifications. This information is identified in the GUI as
rsion.
ult:
ng the v erification
lscriptentry:
cpp -date "02/01/2002"...
thor
f the author is the result of the whoami command
ce-cpp -author "John Tester"
1.0.
mple shell script entry:
Exa
yspace-cpp -verif-version 1.3 ...
pol
1-7
1 Options Description
-keep-all-files
When this option is set, all intermediate results and associated working files
are retained. Consequently, it is possible to restart PolySpace verification
from the end of any complete pass (provided the source code remains entirely
unchanged). If this option is not used, you must restart the verification from
scratch.
By default, intermediate results and associated working files are erased when
theyarenolongerneededbythesoftware.
This option is applicable only to client verifications. Intermediate results are
always removed before results are downloaded from the PolySpace serve r.
Note To cleanup intermediate files at a later time, you can s ele ct
Tools > Clean Results in the Launcher.
This options deletes the preliminary results files from the results directory.
1-8
Default:
Disabled.
Example shell script entry:
polyspace-cpp -keep-all-files
-continue-with-existing-host (Deprecated)
Note This option is deprecated in R2010a and later releases, and no
longer exists in the user interface. PolySpace verification now continues
regardless of the system configuration. The software still checks the hardware
configuration, and issues a warning if it does not satisfy requirements.
When this option is set, the verification will continue even if the system is
under specified or its configuration is not as preferred by PolySpace softw are.
Verified system parameters include the amount of RAM, the amount of swap
space, and the ratio of RAM to swap.
-allow-unsupported-linux (Deprecated)
Note This option is deprecated in R2010a and later releases, and no longer
exists in the user interface. PolySpace verification now continues regardless
of the Linux distribution. If the Linux distribution is not officially supported,
the software displays a warning in the log file.
This option specifies that PolySpace verification will be launched on an
unsupported OS Linux distribution.
PolySpace software supports the Li nu x distributions listed in “Hardware and
Software Requirements” in the PolySpace Installation G uide.
Report Generation
When this option is selected, PolySpace software creates a verification report,
using the following options:
General
• “-report-template Report_Template_Name” on page 1-9
• “-report-output-format Output_Format” on page 1-10
• “-report-output-name Name” on page 1-10
-report-template Report_Template_Name
Generates a verification report, using the specified report template name.
The report is generated at the end of the verification proces s, before any
post-analysis-command is executed.
Default:
C:\PolySpace\PolySpace_Common\ReportGenerator\templates\Developer.rpt
Example Shell Script Entry:
1-9
1 Options Description
polyspace-cpp -report-template c:/polyspace/my_template
-report-output-format Output_Format
Specify the output format fo r the report specified by the report-template
option. The argument is not case sensitive.
Valid options are:
• HTML
• PDF
• RTF
• WORD
• XML
Note WORD format is not available on UNIX platforms, RTF format is used
instead.
1-10
Default:
If y ou do not specify an output format, RTF is used by default.
Example Shell Script Entry:
polyspace-cpp -report-template my_template report-output-format
pdf
-report-output-name Name
Specify the name of the file that is generated for the verification report.
Default:
If you do not specify a name, the following name is used by default:
-Prog_TemplateName.Format
where Prog is the argument of prog option, TemplateName is the nam e of the
report template specified by the
file extensio n for the format specified by the
-report-template option, and Format is the
report-output-format option.
Example Shell Script Entry:
polyspace-cpp -report-template my_template report-output-name
Airbag_V3.rtf
General
1-11
1 Options Description
Targets/Compilers
-target TargetProcessorType
This option specifies t he target processor type, and by doing so informs
PolySpace of the size of fundamental data types and of the endianess of the
target machine.
In this section...
“-target TargetProcessorType” on page 1-12
“GENERIC ADVANCED TARGET OPTIONS” on page 1-13
“-OS-target OperatingSystemTarget” on page 1-19
“-D compiler-flag” on page 1-19
“-U compiler-flag” on page 1-20
“-include file1[,file2[,...]]” on page 1-20
“-post-preprocessing-command "command"” on page 1-21
“-post-analysis-command <file_name> or "command"” on page 1-22
1-12
Possible v alues are: sparc, m68k, power pc, i386, c-167, mcpu, or PST Generic
target.
mcpu is a reconfigurable Micro Controller/Processor Unit target. One or more
generic targets can also be specified and saved. In addition, you can analyze
code intended for an unlisted processor type using one of the listed processor
types, if they share common data properties. Refer to “Setting Up a Target” in
the PolyS pace Products for C++ User’s Guidefor more details.
For information on specifying a generic target, or modifying the mcpu target,
see “GENERIC ADVANCED TARGET OPTIONS” on page 1-13.
Note The generic target option is incompatible with any v isual dialect.
Default:
Targets/Compilers
sparc
Example shell script entry:
polyspace-cpp -target m68k ...
GENERIC ADVANCED TARGET OPTIONS
The Generic target options dialog box opens w hen you select an mcpu target,
or a generic target.
This dialog box allows you to specify a generic "Micro Controller/Processor
Unit" or mcpu target name. Initially, it is necessary to use the GUI to specify
thenameofanewmcpu target – say, “MyTarget”.
Note The generic target option is incompatible with any v isual dialect.
That new target is added to the -target options list. The new target’s default
characteristics are as follows, using the type [size, alignment] format.
• char [8, 8], char [16,16]
• short [16, 16]
• int [16, 16]
• long [32, 32], long long [32, 32]
• float [32, 32], double [32, 32], long double [32, 32]
• pointer [16, 16]
• char is signed
• little-endian
When using the command line, MyTarget is specified with all the options
for modification:
polyspace-cpp -target MyTarget
1-13
1 Options Description
For example, a specific target uses 8 bit alignment (see also -align), for which
the command line would read:
polyspace-cpp -target mcpu -align 8
-little-endian
This option is only available when a -mcpu generic ta rge t has be en chosen.
The endianness defines the byte order within a word (and the word order
within a long integer). Little-endian architectures are Less Significant byte
First (LSF), for example: i386.
For a little endian target, the less significant byte of a short integer (for
example 0x00FF) is stored at the first byte (0xFF) and the most significant
byte (0x00) at the second byte.
Example shell script entry:
polyspace-c -target mcpu -little-endian
1-14
-big-endian
This option is only available when a -mcpu generic ta rge t has be en chosen.
The endianness defines the byte order within a word (and the word order
within a long integer). Big-endian architectures are Most Significant byte
First (MSF), for example: SPARC, m68k.
For a big endian target, the most significant byte of a short integer (for
example 0x00FF) is stored at the first byte (0x00) and the less significant
byte (0xFF) at the second byte.
Example shell script entry:
polyspace-c -target mcpu -big-endian
-default-sign-of-char [signed|unsigned]
This option is available for all targets. It allows a char to be defined as
"signed", "unsigned", or left to assume the mcpu target’s default behavior
Targets/Compilers
Default mode:
Thesignofcharislefttoassumethetarget’sdefaultbehavior. Bydefaultall
targets are considered as signed except for powerpc targets.
Signed:
Disregards the target’s default char d e finition, and specifies that a "signed
char" should be used.
Unsigned:
Disregards the target’s default char definition, and specifies that a "unsigned
char" should be used.
Example Shell Script Entry
polyspace-cpp -default-sign-of-char unsigned -target mcpu ...
-char-is-16bits
This option is available only when you select a mcpu generic target.
The default configuration of a generic target defines a char as 8 bits. This
option changes it to 16 bits, regardless of sign.
the minimum alignm ent of objects is also set to 16 bits and so, incompatible
with the options
Setting the char type to 16 bits has consequences on the following:
• computation of size of for objects
• detection of underflow and overflow on chars
Without the option char for mcpu are 8 bits
Example shell script entry:
polyspace-cpp -target mcpu -char-is-16bits
-short-is-8 bits and -align 8.
1-15
1 Options Description
-short-is-8bits
This option is only available when a generic target has been chosen.
The default configuration of a generic target d efines a short as 16 bits. This
option changes it to 8 bits, irrespective of sign.
It sets a short type as 8-bit without specific alignment. That has consequences
for the following:
• computationofsizeofobjects referencing short type
• detection of short underflow/overflow
Example shell script entry
polyspace-cpp -target mcpu -short-is-8bits
-int-is-32bits
This option is available with a generic target has been chosen.
1-16
The default configuration of a generic target defi n es an int as 16 bits. This
option changes it to 32 bits, irrespective of sign. Its alignment, when an int
is used as struct member or array component, is also set to 32 bits. See also
-align option.
Example shell script entry
polyspace-cpp -target mcpu -int-is-32bits
-long-long-is-64bits
This option is only available when a generic target has been chosen.
The default configuration of a generic target defines a long long as 32 bits.
This option changes it to 64 bits, irrespective of sign. When a long long is
used as struct member or array component, its alignment is also set to 64
bits. See also -align option.
Example shell script entry
Targets/Compilers
polyspace-cpp -target mcpu -long-long-is-64bits
-double-is-64bits
This option is available when either a generic target has been chosen.
The default configuration of a generic target defines a double as 32 bits. This
option, changes both double and long double to 64 bits. When a double or
long double is used as a struct member or array component, its alignment
is set to 4 bytes.
Seealso-alignoption.
Defining the double type as a 64 bit double precision float impacts the
following:
- Computation of sizeofobjects referencing double type
- Detection of floating point underflow/overflow
Example
int main(void)
{
struct S {char x; double f;};
double x;
unsigned s1, s2;
s1 = sizeof (double);
s2 = sizeof(struct S);
x = 3.402823466E+38; /* IEEE 32 bits float point maximum value */
x=x*2;
return 0;
}
Using the default configuration of sharc21x62, C PolySpace assumes that a
value of 1 is assigned to s1, 2 is assigned to s2, and there is a consequential
float overflow in the mul t iplication x * 2. Using the –d ou bl e-is-64bits option,
a value of 2 is assigned to s1, and no overflow occurs in the multiplication
(because the result is in the range of the 64-bit floating point type)
Example shell script entry
1-17
1 Options Description
polyspace-cpp -target mcpu -double-is-64bits
-pointer-is-32bits
This option is only available when a generic target has been chosen.
The default configuration of a generic target defines a pointer as 16 bits. This
option changes it to 32 bits. When a pointer is used as struct member or array
component, its alignment is also set also to 32 bits (see -align option).
Example shell script entry
polyspace-cpp -target mcpu -pointer-is-32bits
-align [8|16|32]
This option is available with an mcpu generic target and some other specific
targets. It is used to set the largest alignment of all data objects to 4/2/1
byte(s), meaning a 32, 16 or 8 bit boundary respectively.
1-18
The d efault alignment of a generic target is 32 bits. This means that when
objects with a size of more than 4 bytes are used as struct members or array
components, they are aligned at 4 byte boundaries.
Example shell script entry with a 32 bits default alignment
polyspace-cpp -target mcpu
-align 16. Ifthe-align16optionisused,whenobjectswithasizeofmore
than 2 bytes are used as struct members or array components, they are
aligned at 2 bytes boundaries.
Example shell script entry with a 16 bits specific alignment:
polyspace-cpp -target mcpu -align 16
-align 8. If the -align 8 option is used, when objects with a size of more
than 1 byte are used as struct members or array components, are aligned
at 1 byte boundaries. Consequently the storage assigned to the arrays and
structures is strictly determined by thesizeoftheindividualdataobjects
without m ember and end padding.
Targets/Compilers
Example shell script entry with a 8 bits specific alignment:
polyspace-cpp -target mcpu -align 8
-OS-target OperatingSystemTarget
This option specifies the operating system target for PolySpace stubs.
Possible val ue s are ’Solaris’, ’Linux’, ’VxWorks’, ’Visual’ and
’no-predefined-OS’.
This information allows the appropriate system definitions to be used during
preprocessing in order to analyze the included files properly. -OS-target
no-predefined-OS may be used in conjunction with -include and/or -D to give
all of the system preprocessor flags to be used at execution time. Details of
these may be found by executing the compiler for the project in verbose mode.
Default:
Solaris
Note Onlythe’Linux’includefilesareprovided with PolySpace software
(see the include folder in the installation directory). Projects developed for use
with other operating systems may be analyzed by using the corresponding
include files for that OS. For instance, in order to analyze a VxWorks
®
project
it is necessary to use the option -I <<path_to_the_VxWorks_include_folder>>
Example shell script entry:
polyspace-cpp -OS-target linux
polyspace-cpp -OS-target no-predefined-OS -D GCC_MAJOR=2 /
-include /complete_path/inc/gn.h ...
-D compiler-flag
This option is used to define macro compiler flags to be used during
compilation phase.
1-19
1 Options Description
Only one flag can be used with each –D as for compilers, but the option can be
used several times as shown in the example below.
Default:
Some defines are applied by default, depending on your -OS-target option.
Example Shell Script Entry:
polyspace-cpp -D HAVE_MYLIB -D USE_COM1 ...
-U compiler-flag
This option is used to undefine a macro compiler flags
Asforcompilers,onlyoneflagcanbeusedwitheach–U,buttheoptioncanbe
used several times as shown in the example below.
Default:
1-20
Some undefines may be set by default, depending on your -OS-target option.
Example Shell Script Entry:
polyspace-cpp -U HAVE_MYLIB -U USE_COM1 ...
-include file1[,file2[,...]]
This optio n is used to specify files to be included by each C++ file involved in
the verification.
Default:
No file is universally included by default, but directives such as "#include
<include_file.h>" are acted upon.
Example Shell Script Entry:
polyspace-cpp -include `pwd`/sources/a_file.h -include
/inc/inc_file.h ...
Targets/Compilers
polyspace-cpp -include /the_complete_path/my_defines.h ...
-post-preprocessing-command "command"
When this option is used, the specified script file or command is run just
after the pre-processing phase on each source file. The script executes on
each preprocessed c files. The command should be designed to process the
standard output from pre-processing and produce its results in accordance
with that standard output.
Default:
No command.
Example Shell Script Entry – file name:
To replace the keyword “Volatile” with “Import”, you can type the following
command on a Linux workstation:
polyspace-cpp -post-preprocessing-command `pwd`/replace_keywords
where replace_keywords is the following script :
#!/usr/bin/perl
my $TOOLS_VERSION = "V1_4_1";
binmode STDOUT;
# Process every line from STDIN until EOF
while ($line = <STDIN>)
{
# Change Volatile to Import
$line =~ s/Volatile/Import/;
print $line;
}
1-21
1 Options Description
Note If you are running PolySpace software version 5.1 (r2008a) or later
on a Windows system, you cannot use Cygwin shell scripts. Since Cygwin
is no longer included with PolySpace software, all files must be executable
by Windows. To support scripting, the PolySpace installation now includes
Perl. You can access Perl in
%POLYSPACE_C%\Verifier\tools\perl\win32\bin\perl.exe
To run the Perl script provided in the previous example on a Windows
workstation, you must use the option
the absolute path to the Perl script, for example:
%POLYSPACE_C%\Verifier\bin\polyspace-cpp.exe
-post-preprocessing-command
%POLYSPACE_C%\Verifier\tools\perl\win32\bin\perl.exe
<absolute_path>\replace_keywords
-post-preprocessing-command with
1-22
-post-analysis-command <file_name> or "command"
When this option is used, the specified script file or command is executed
once the verification has comple ted.
The script or command is executed in the results directory of the verification.
Execution occurs after the last part of the verification. The last part of is
determined by the–to option.
Note Depending on the archite cture used (notably when performing a server
verification), the script can be executed on the client side or the serve r side.
Default:
No command.
Example Shell Script Entry – file name:
Targets/Compilers
This example shows how to send an email to tip the client side off that his
verification has been ended. This example supposes that the mailx command
is available on the machine. So the command looks like:
polyspace-cpp -post-analysis-command `pwd`/end_email
where end_email is an appropriate Perl script.
Note If you are running PolySpace software version 5.1 (r2008a) or later
on a Windows system, you cannot use Cygwin shell scripts. Since Cygwin
is no longer included with PolySpace software, all files must be executable
by Windows. To support scripting, the PolySpace installation now includes
Perl. You can access Perl in
%POLYSPACE_C%\Verifier\tools\perl\win32\bin\perl.exe
To run the Perl script provided in the previous example on a Windows
workstation, you must use the option
-post-preprocessing-command with
the absolute path to the Perl script, for example:
%POLYSPACE_C%\Verifier\bin\polyspace-cpp.exe
-post-analysis-command
%POLYSPACE_C%\Verifier\tools\perl\win32\bin\perl.exe
<absolute_path>\end_emails
1-23
1 Options Description
Compliance with Standards
In this section...
“-dos” on page 1-24
“Embedded Assembler” on page 1-25
“-wchar-t-is-unsigned-long” on page 1-26
“-size-t-is-unsigned-long” on page 1-26
“-no-extern-C” on page 1-26
“-no-stl-stubs” on page 1-27
“-dialect D ialectNam e” on page 1-27
“-wchar-t-is” on page 1-28
“-for-loop-index-scope” on page 1-28
“-ignore-pragma-pack” on page 1-29
“Visual Specific Options” on page 1 -3 0
1-24
“Coding Rules Checke r” on page 1-31
“-ignore-constant-overflows” on page 1-35
“-allow-undef-variables” on page 1-35
“-allow-negative-operand-in-shift” on page 1-36
“-Wall” on page 1-36
-dos
This option must be used when the contents of the include or source
directory comes from a DOS or Windows file system. It deals with upper/lower
case sensitivity and control characters issues.
Concerned files are:
• header files: all include dir specified (-I option)
Compliance with Standards
• source files: all sources files selected for the verification (-sources option)
#include "..\mY_TEst.h"^M
#include "..\mY_other_FILE.H"^M
into
#include "../my_test.h"
#include "../my_other_file.h"
Default:
disabled by default
Example Shell Script Entry:
polyspace-cpp -I /usr/include -dos -I ./my_copied_include_dir -D test=1
Embedded Assembler
PolySpace stops the execution when detecting assembler code and displays
an error message. It can continue the execution if it is requested by the user
with the option –discard-asm.
PolySpace ignores the assembler code by assuming that the assembler code
does not have any side effect on global variables. Delimiters for asse mbler
code to ignore can be recognized by PolySpace following C++ standard
specified asm declarations: __asm and __asm__.
-discard-asm
This option instructs the PolySpace verification to discard assembler code. If
this option is used, the assembler code should be modelled in c.
Default:
Embedded assembler is treated as an error.
1-25
1 Options Description
Example Shell Script Entry:
polyspace-cpp -discard-asm ...
-wchar-t-is-unsigned-long
This option forces the “underlying type” as defined in the C++ standard
to be unsigned long.
For example, sizeof(L’W’) will have the value of sizeof(unsigned long) and
thewchar_tfieldwillbealignedinthesamewayastheunsignedlongfield.
Note that wchar_t will remain a different type from unsigned long unless
“-wchar-t-is typedef” is set or implied by the current dialect. The default
underlying type of wchar_t is unsigned short.
Example Shell Script Entry:
polyspace-cpp -wchar-t-is-unsigned-long ...
1-26
-size-t-is-unsigned-long
Indicates the expected typedef of size_t to the software; forces the size_t type
to be unsigned long. The default type of size_t is unsigned int.
Example Shell Script Entry:
-size-t-is-unsigned-long ...
polyspace-cpp
-no-extern-C
Some functions may be declared inside an extern “C” { } bloc in some files and
not in others. Then, their linkage is not the same and it causes a link error
according to the ANSI standard.
Applying this option will cause PolySpace to ignore this error.
This permissive option may not solve all the extern C linkage errors.
Example Shell Script Entry:
polyspace-cpp -no-extern-C ...
-no-stl-stubs
PolySpace provi
(STL). This impl
applications.
de an efficient implementation of part of the Standard library
In that case some linking errors could arise.
Compliance with Standards
ementation may not be compatible with includes files of the
With this opti
Example Shell
polyspace-c
-dialect Di
Specifies t
default, c
visual7.1
visual6 a
compiler
and subs
If the di
the -OS-
If the d
-disca
visua
All Vi
-no-s
rd-asm
l8
sual2005.NETgivenincludefilescancompilebothwiththe
tl-stubs
on Poly Space does n ot use this implementation of the STL.
Script Entry:
pp -no-stl-stubs ...
alectName
he dialect in which the code is written. Possible values are:
front2
,andvisual8.
ctivates dialect associated with code used for Microsoft Visual 6.0
and visual activates dialect associated with Microsoft Visual 7.1
equent.
alect is visual (
target option must be set to
ialect is visual, the options
dialect activates support for Visual 2005 .NET specific com p il er.
, cfront3, iso, gnu, visual, visual6, visual7.0,
visual, visual6, visual7.0, visual7.1 and visual8)
Visual.
-dos, -OS-target Visual and
are set by default.
option and without it (recommended).
Note
iso o
For
sta
De
If you select the
r
default, some JSF++ coding rules may not be completely checked.
example, AV Rule 8: “All code shall conform to ISO/IEC 14882:2002(E)
ndard C++.”
fault:
-jsf-coding-rules option and a dialect other than
1-27
1 Options Description
default
Example Shell Script Entry:
polyspace-cpp -dialect visual8 ...
-wchar-t-is
This option forces wchar_t to be treated as a keyword as per the C++ standard
or as a typedef as with Microsoft Visual C++ 6.0/7.x dialects.
Possible values are ’keyword’ or ’typedef’:
• typedef is the default behavior w hen using -dialect option associated to
visual6, visual7.0 and visual7.1.
• keyword is the default behavior for all others dialects including visual8.
This option allows the default behavior implied by the PolySpace dialect
option to be overridden.
1-28
This option is equivalent to the Visual C++ /Zc:wchar and /Zc:wchar- options.
Default:
default (depends on -dialect value).
Example in shell script:
polyspace-cpp wchar-t-is typedef
-for-loop-index-scope
This option changes the scope of the index variable declared within a for loop.
Example:
for (int index=0; ...){};
index++; // index variable is usable (out) or not (in)
at this point
Compliance with Standards
Possible values are ’in’ and ’out’:
• outisthedefaultforthe-dialectoption associated with values cfront2,
crfront3, visual6, visual7 and visual 7.1.
• in is the default for all other dialects, including visual8.
The C++ ANSI standard specifies the index be treated as ’in’.
This option allows the default behavior implied by the PolySpace dialect
option to be overridden.
This option is equivalent to the Visual C++ options
Zc:forScope-
.
/Zc:forScopeand
Default:
default (depends on –dialect value)
Example in shell script:
polyspace-cpp for-loop-index-scope in
-ignore-pragma-pack
C++ #pragma directives specify packing alignment for structure, union, and
class members. The -ignore-pragma-pack option a llows these directives to be
ignored in order to prevent link errors.
PolySpace will stop the execution and display an error message if this option
is used in non visual mode or without dialect gnu (without -OS-target visual
or –dialect visual*). See also “Link messages” in the PolySpace Products
for C++ User’s Guide.
Example Shell Script Entry:
polyspace-cpp dialect visual ignore-pragma-pack ...
1-29
1 Options Description
Visual Specific Options
• “-import-dir directory” on page 1-30
• “-pack-alignme n t -v alue value” on page 1-30
• “-support-FX-option-results” on page 1-30
-import-dir directory
One directory to be included by #importdirective. This option must be used
with -OS-target visual or -dialect visual* (6, 7.0, 7.1 and 8). It gives the
location of *.tlh files generated by a Visual Studio compiler when encounter
#import directive on *.tlb files.
Example Shell Script Entry:
polyspace-cpp -dialect visual8 -import-dir /com1/inc ...
-pack-alignment-value value
Visual C++ /Zp option specifies the default packing alignment for a project.
Option -pack-alignment-value transfers the default alignment value to
PolySpace verification.
1-30
Theargumentvaluemustbe: 1,2,4,8,or16. Verificationwillhaltand
display an error message with a bad value or if this option is used in no n
visual mode (-OS-target visual or -dialect visual* (6, 7.0 or 7.1)).
Default:
8
Example Shell Script Entry:
polyspace-cpp dialect visual pack-alignment-value 4 ...
-support-FX-option-results
Visual C++ /FX option allows the partial translation of sources making use
of managed extensions to Visual C++ sources without managed extensions.
Compliance with Standards
Theses extensions are currently not taken into account by PolySpace and can
be considered as a limitation to analyze this kind of code.
Using /FX, the translated files are generated in place of the original ones in
the project, but the names are changed from foo.ext to foo.mrg.ext.
Option – support-FX-option-results allows the verification of a project
containing translated sources obtained by compilation of a Visual project
using the /FX Visual option. Managed files need to be located in the same
directory as the original ones and PolySpace will verify managed files instead
of the original ones without intrusion, and will permit you to remove part of
thelimitationsduetospecificextensions.
PolySpace will stop the execution and display an error message if this option
is used in non visual mode (-OS-target visual or -dialect visual* (6, 7.0 or 7.1)).
Example Shell Script Entry:
polyspace-cpp dialect visual - support-FX-option-results
Coding Rules Checker
• “Check JSF C++ rules ” on page 1-31
• “-jsf-coding-rules [all-rules | file_name]” on page 1-32
• “Check MISRA C++ rules” on page 1-33
• “-misra-cpp [all-rules | file_name]” on page 1-33
• “-includes-to-ignore "dir_or_file_path1[,dir_or_file_ pa t h 2[ ,.. .] ]"” on page
1-34
Check JSF C++ rules
Specifies that PolySpace software checks for compliance with the Joint Strike
Fighter Air Vehicle C++ coding standards (JSF++:2005).
The results are included in the log file of the verification.
For more information, see “Checking JSF++ Coding Rules”.
1-31
1 Options Description
-jsf-coding-rules [all-rules | file_name]
Specifies which JSF++ coding rules to check.
• Keyword all-rules – Checks all available JSF++ rules using the default
configuration. Any violation of JSF++ rules is considered a warning.
• Option file_name – The name of an ASCII text file containing a list of
JSF++ rules to check.
Note If you specify -jsf-coding-rules,the-wall option is disabled.
Note If your project uses a dialect other than ISO, some JSF++ coding rules
may not be completely checked. For example, AV Rule 8: “All code shall
conform to ISO/IEC 14882:2002(E) standard C++.”
Format of the file:
1-32
<rule number> off|error|warning
# is considered a comment.
Example:
# JSF-CPP rules configuration file
1 off # disable AV Rule number 1
2 off # Not implemented
3 off # disable AV Rule 3
8 error # violation AV Rule 8 is error
9 warning # violation AV Rule 9 is only a warning
# End of file
Default:
Disabled
Example shell script entry:
polyspace-cpp -jsf-coding-rules all-rules
Compliance with Standards
polyspace-cpp -jsf-coding-rules jsf.txt
Check MISRA C++ rules
Specifies that PolySpace software checks for compliance with the MISRA
C++ coding standards (MISRA C++:2008).
The results are included in the log file of the verification.
For more information, see “Checking MISRA C++ Coding Rules”.
®
-misra-cpp [all-rules | file_name]
Specifies which MISRA C++ coding rules to check.
• Keyword all-rules – Checks all available MISRA C++ rules using the default
configuration. Any violation of MISRA C++ rules is considered a warning.
• Option file_name – Specifies the name of an ASCII text file containing a
list of MISRA C++ rules to check.
Note If you specify -misra-cpp,the-wall option is disabled.
Format of the file:
<rule number> off|error|warning
# is considered a comment.
Example:
# MISRA-C++ rules configuration file
# Generated by PolySpace
0-1-1 warning
0-1-2 warning
0-1-7 warning
0-1-8 off
0-1-9 off
0-1-10 warning
1-33
1 Options Description
0-1-11 off
0-1-12 off
1-0-1 error
1-0-2 off # Not implemented
1-0-3 off # Not implemented
2-2-1 off # Not implemented
2-3-1 warning
2-5-1 warning
2-7-1 warning
# End of file
Default:
Disabled
Example shell script entry:
polyspace-cpp -misra-cpp all-rules
1-34
polyspace-cpp -misra-cpp misra.txt
-includes-to-ignore "dir_or_file_path1[,dir_or_file_path2[,...]]"
This option prevents the coding rules checker from checking a given list of
files or directories (all files and subdirectories under selected directory). This
option is useful if you use headers that do not conform w ith JSF++ or MISRA
C++ standards. A warning is displayed if one of the files does not exist.
This option is enabled only when you specify
-misra-cpp.
Example shell script entry :
polyspace-cpp -jsf-coding-rules jsf.txt includes-to-ignore
"c:\usr\include"
-jsf-coding-rules or
Compliance with Standards
-ignore-constant-overflows
This option specifies that the verification should be permissive with regards
to overflowing computations on constants. Notethatitdeviatesfromthe
ANSI C standard.
For example,
char x = 0xff;
causes an overflow according to the standard, but if it is analyzed using this
option it becomes effectively the same as
char x = -1;
With this second example, a red overflow will result irrespective of the use
of the option.
char x = (rn d?0xFF:0xFE);
Default:
char x = 0xff; causes an overflow
Example Shell Script Entry:
polyspace-cpp -ignore-constant-overflows ...
-allow-undef-variables
When this option is used, PolySpace will continue in case of linkage errors
due to undefined global variables. For instance when this option is used,
PolySpace will tolerate a variable always being declared as extern
Default:
Undefined variables causes PolySpace to stop.
Example Shell Script Entry:
polyspace-cpp -allow-undef-variables ...
1-35
1 Options Description
-allow-negative-operand-in-shift
This option allows a shift operation on a negative number.
According to the ANSI standard, such a shift operation on a negative number
is illegal – for example,
-2 << 2
With this option in use, PolySpace considers the operation to be valid. In the
previous example, the result would be
-2 << 2 = -8
Default:
A shift operation on a negative number causes a red error.
Example Shell Script Entry:
polyspace-cpp -allow-negative-operand-in-shift ...
1-36
-Wall
Force the C++ compliance phase to print all warnings.
Note If you specify -jsf-coding-rules,thisoptionisdisabled.
Default:
By default, only warnings about compliance across different files are printed.
Example Shell Script Entry:
polyspace-cpp -Wall ..
PolySpace Inner Settings
In this section...
“-unit-by-unit” on page 1-37
“-unit-by-unit-common-source filename”onpage1-38
“-main sub_program_name” on page 1-38
“Generate a Main Using a Given Class” on page 1-39
“-main-generator-calls” on page 1-42
“General options for the generation of mains” on page 1-43
“-data-range-specifications file_name” on page 1-46
“-no-automatic-stubbing” on page 1-47
“-ignore-float-rounding” on page 1-47
“-detect-unsigned-overflows” on page 1-49
“-enum-type-definition” on page 1-50
PolySpace Inner Settings
“-machine-architecture” on page 1-50
“-max-processes” on page 1-51
“-extra-flags option-extra-flag” on page 1-52
“-cpp-extra-flags flag” on page 1-52
“-il-extra-flags flag” on page 1-52
-unit-by-unit
This option creates a separate verification job for each source file in the
project.
Each file is compiled, sent to the PolySpace Server, and v erified in dividually.
Verification results can be viewed for the entire project, or fo r individual units.
This option is only available for server verifications. It is notcompatiblewith
multitasking options such as
Default:
-entry-points.
1-37
1 Options Description
Not selected
Example Shell Script Entry:
polyspace-cpp -unit-by-unit
-unit-by-unit-common-source filename
Specifies a list of files to include with each unit verification. These files are
compiled once, and then linked to each unit before verification. Functions
not included in this list are stubbed.
Default:
None
Example Shell Script Entry:
polyspace-cpp -unit-by-unit-common-source
c:/polyspace/function.cpp
1-38
-main sub_program_name
The option specifies the qualified name of the main subprogram when a
visual –OS-target is selected. This procedure will be analyzed after class
elaboration, and before tasks in case of a multitask application or in case of
the -entry-points usage.
Possible values are:
main, _tmain, wmain, _tWinMain, wWinMain, WinMain and DllMain.
However, if the main subprogram does not exist and the option
-main-generator is not set, PolySpace w ill stop the verification with an error
message.
Default:
main
PolySpace Inner Settings
Example Shell script entry:
polyspace-cpp -main WinMain OS-target visual
Generate a Main Using a Given Class
• “-class-analyzer” on page 1-39
• “-class-only” on page 1-40
• “-class-analyzer-calls” on page 1-40
• “-no-constructors-init-check” on page 1-41
-class-analyzer
PolySpaceforC++isaclassanalyzer. If a main program is present in the
setoffilesthatyousubmitforverification then the verification proceeds
with that main program. Otherwise, you can choose not to provide a main
program and select a single class instead.
If MyclassName does not exist in the application, the verification will come to
a h alt. All public and protected function members declared within the class,
whethertheyarecalledwithinthecodeornot,willbeanalyzedseparately
andcalledbyageneratedmain.
This generated main is not code compliant but is visible in the graphical
user interface within the
_polyspace_main.cpp file. Notethatitinitializes
all global variables to random (see “How the Class Analyzer Works”in the
PolySpace Products for C++ User’s Guide).
Note This option cannot be used with the option
-function-called-before-main.
Example shell script entry:
polyspace-cpp class-analyzer MyClass
polyspace-cpp class-analyzer MyNamespace::MyClass
1-39
1 Options Description
-class-only
This option can only be used with the option –class-analyzer. If the
-class-analyzer option is not used, verification stops and displays an error
message. With the option –class-only, only functions associated to MyClass
are v erified. All functions out of class scope a re automatically stubbed even
though they are defined in the source code.
Default:
disable
Example Shell Script Entry:
polyspace-cpp class-analyzer MyClass class-only...
-class-analyzer-calls
Specifies which functions are called by the generated main.
1-40
This option can only be used with the option –class-analyzer. If the
-class-analyzer option is not used, verification stops and displays an error
message.
There are three options:
• Default – The generated main calls all public and protected function
members declared within the class, whether called in the code or not. Every
eligible function is called directly by the generated main.
• Unused – The generated main calls only those functions not called by
another eligible function. Members inherited from a base class are not
verified.
• Inherited – The generated main calls the functions of the named class as
well as functions inherited from the base class that are not called within
the analyzed class. Inherited methods are called in the child context,
meaning that the generated main does not make explicit calls to the
parent’s constructor and destructor.
PolySpace Inner Settings
Note If the hierarchy contains the same class more than once, only the
first instance of the class is analyzed, and the software displays a warning
message.
Eligible functions are:
• Public and protected methods of analyzed class
• Existing constructors of analyzed class
• Destructor of analyzed class
• Existing copy constructors of analyzed class
Default:
Default
Example Shell Script Entry:
polyspace-cpp class-analyzer MyClass class-analyzer-calls
unused ...
-no-constructors-init-check
By default, PolySpace checks for member i nitializatio n just after object
construction and initialization with
using
-class-analyzer.
This option can only be u sed with
-class-analyzer is not used, verification stops and displays an error
message.
Without this option, in the generated main in
youwillfindsomeaddedcodecheckslikeonthesimpleexamplebelowusing
-class-analyzer Aoptions:
class A {
public: int i ; int *j ; int k; int l;
A() : i(0), j(0), k(0) { ; }
-function-called-before-main when
class-analyzer.Iftheoption
__polyspace_main.cpp file,
1-41
1 Options Description
r
A(int a) : i(a), k(0) { ; }
void foo() {
i = 1; i++;
j = (int *) 0x0100; j++;
l = 1; l++;}
};
In __polyspace_main.cpp after a call to the constructor(s) and function
called before main:
check_NIV( __polyspace__A__this->i ); // green NIV
check_NIP( __polyspace__A__this->j ); // orange NIP
check_NIV( __polyspace__A__this->k );/* member has been detected as neve
// grey NIV
check_NIV( __polyspace__A__this->l ); // red NIV
• i is always initialized, read and written in foo — green NIV
j is initialized in one constructor only, read and written in foo — orange
•
NIP
1-42
•
k is always initialized, but never read and written outside the constructors
—grey
•
l is never initialized in the constructors — red NIV
When this option is applied, no further check of member variables’
initialization is made.
Default:
Check is made f or member scalars, floats and pointer member variables.
Example Shell Script Entry:
polyspace-cpp class-analyzer MyClass no-constructors-init-check
...
-main-generator-calls
This option is used with the -main-ge nerator option, to specify the functions
to be called.
PolySpace Inner Settings
Note that this option is protected by a license.
Eligible functions:
Every function declared outside a class and defined in the source code to
analyze, is considered as eligible when using the option.
The list of functions contains a list of short name (name without signature)
separated by comas. If the name of a function from the list is associated to
a function not defined in the source code, PolySpace stops and displays an
error message. If the name of a function from the list is ambiguous, all the
functions with the same short name are called. If a function from the list does
not belong or is not eligible, PolySpace stops and displays an error message.
This error message is put in the log file.
Default values:
•
none – No function is called. This can be used with a multitasking
application without a main, for instance.
•
unused (default) – Call all functions not already called within the co de .
Inline functions will not be called by the generated main.
•
all – all functions except inline will be called by the generated main.
custom – Only functions present in the list are called from the main. Inline
•
functions can be specified in the list and will be called by the generated
main.
An inline (static or extern) function is not called by the generated main
program with values all or unused. An inline function can only be called with
custom value: -main-generator-calls custom=my_inlined_func.
Example:
polyspace-cpp -main-generator -main-generator-calls
custom=function_1,function_2
General options for the generation of mains
• “-function-called-before-main” on page 1-44
1-43
1 Options Description
• “-main-generator-writes-variables” on page 1-45
-function-called-before-main
This option is used with the main generator option –main-generator-calls to
specify a fun c tion which will be called before all selected functions in the main.
Note This option cannot be used with the option class-analyzer.
Eligible functions:
Every function or method defined in the source code to analyze is considered
as eligible when using the option.
If the function or method is not overloaded, simply specify the name of the
function. If the function or method is overloaded, you must specify the full
prototype, including the type of argument (but not the name of argument).
1-44
If the function is not defined in the source code, the verification stops and
displays an error message.
Note If the function name you provide is ambiguous (there is another
functionofthesamenameinanotherclass)theverificationstopsanddisplays
an error message listing the specific names of all possible functions. You can
avoid this error by copying the correct name from the error message and
enclosing it with double quotes.
Unit-by-unit verification:
When performing unit-by-unit verification (using use the option
-unit-by-unit) the behavior of -function-called-before-main changes
depending on the type of init function you specify.
When you set the option
mode:
-function-called-before-main in unit-by-unit
PolySpace Inner Settings
• If the init function is an out of class function, it is called at the beginning
of the generated main (before the "if random" block of classes).
• If the
init function is a method (function member of a class), it is called
after all const ructor calls of the corresponding class. If several classes are
present in the unit, the software displays a warning explaining that the
function called before main will be called only with the concerned class.
Example:
polyspace-cpp -main-generator-calls unused
-function-called-before-main MyFunction
-main-generator-writes-variables
This option is used with the main generator options –class-analyzer and
–main-generator-calls to dictate how the generated main will initialize global
variables.
Settings available:
• uninit – main generator writes random on no t initialized global variables.
• none –noglobalvariablewillbewrittenbythemain.
• public – e very variable except static and const variables are assigned a
“random” value, representing the full range of possible values
• all – every variable is assigned a “rand om ” value, representing the full
rangeofpossiblevalues
• custom – only variables prese n t in the list are assigned a “random” value,
representing the full range of possible values
Example
polyspace-cpp class-analyzer MyClass
-main-generator-writes-variables uninit
polyspace-cpp -main-generator -main-generator-writes-variables
custom=variable_a,variable_b
1-45
1 Options Description
-data-range-specifications file_name
This option permits the setting of specific data ranges for a list of given
global variables.
For more information, see “Specifying Data Ranges for Variables and
Functions (Contextual Verification)”in the PolySpace Products for C++ User’s
Guide.
File format:
The file filename contains a list of global varia bl es with the below format:
variable_name val_min val_max <init|permanent|globalassert>
Variables scope:
Variables concern external linkage, const variables and not necessary a
defined variable (i.e. could be e xtern with option -allow-undef-variables).
1-46
Note Only one mode can be applied to a global va riable.
No checks are added with this option except for globalassert mode.
Some warning can be displayed in log file concerning variables when format
or type is not in the scope.
Default:
Disable.
Example shell script entry:
polyspace-c -data-range-specifications range.txt ...
PolySpace Inner Settings
-no-automatic-
By default, Poly
used, the list of
stopped.
Benefits:
This option ma
• The entire co
alargepiece
not complet
• Manual stub
verificati
Default:
All funct
ions are stubbed automatically
-ignore
Without
standar
which d
perfor
this option, PolySpace rounds floats according to the IEEE 754
d: simple precision on 32-bits targets and double precision on target
efine double as 6 4-bits. With the option, exact computation is
med.
Space automatically stubs all functions. When this option is
functionstobestubbedisdisplayed and the verification is
ybeusedwhere
de is to be provided, which may be the case when analyzing
of code. When the verification stops, it means the code is
e.
bing is preferred to improve the selectivity and speed of the
on.
-float-rounding
stubbing
Exampl
e
1
2 void ifr(float f)
3{
4 double a = 1.27;
5 if ((double)1.27F == a) {
6 assert (1);
7 f=1.0F*f;
8 // reached when -ignore-float-rounding is used or not
9}
10 else {
11 assert (1);
1-47
1 Options Description
12 f = 1.0F * f;
13 // reached when compiled under Visual and when
-ignore-floatrounding is not used
14 }
15 }
Using this option can lead to different results compared to the "real life"
(compiler and target dependent): Some paths will be reachable or not for
PolySpace while they are not (or are) depending of the compiler and target. So
it can potentially give approximate results (green should be unproven). This
option has an impact on OVFL checks on floats.
However, this option allows reducing the number of unproven checks because
of the “delta” approximation.
For example:
• FLT_MAX (with option set) = 3.40282347e+38F
• FLT_MAX (following IEEE 754 standard) = 3.40282347e+38F ± Δ
1-48
1
2 void ifr(float f)
3{
4 double a = 1.27;
5 if ((double)1.27F == a) {
6 assert (1);
7 f = 1.0F * f; // Overflow never occurs because f <= FLT_MAX.
8 // reached when -ignore-float-rounding is used
9}
10 else {
11 assert (1);
12 f = 1.0F * f; // OVFL could occur when f = (FLT_MAX + D)
13 // reached when -ignore-float-rounding is not used
14 }
15 }
Default:
IEEE 754 round ing under 32 bits and 64 bits.
PolySpace Inner Settings
Example Shell Script Entry:
polyspace-cpp -ignore-float-rounding ...
-detect-unsigned-overflows
When this option is sel ected, verification is more strict with overflowing
computations on unsigned integers than the ANSI
The ANSI C standard states that promotion occurs for logic, bitw ise and
arithmetic operators. For
char, short,andint types, variables are implicitly
cast into integers before the operation. Then, after the operation, the
variables are downcast into the original type.
Consider the examples below.
Example 1
Using this option, the following example generates an error:
®
C standard requires.
unsigned char x;
x = 255;
x=x+1; //overflow due to this option
Without this option, however, the example does not generate an error.
unsigned char x;
x = 255;
x=x+1; // turns x into 0 (wrap around)
Example 2
Using this option, the following example generates an error:
unsigned char Y=1;
Y=~Y; //overflow because of type promotion
In this example:
1 Y is coded as an unsigned char: 000000001
1-49
1 Options Description
2 Y is promoted to an integer: 00000000 00000000 00000000 00000001
3 The operation "~" is performed, making Y: 11111111 11111111 11111111
11111110
4 The i nteger is downcast to an unsigned char, causing an overflow.
Example Shell Script Entry:
polyspace-cpp -detect-unsigned-overflows ...
-enum-type-definition
Allows the verification to use different base types to represent an enumerated
type, depending on the enumerator values and the selected definition.
When using this option, each enum type is represented by the smallest
integral type that can hold all its enumeration values.
Possible values are:
1-50
•
defined-by-standard – Uses the first type that can hold all of the
enumerator values from the following list:
signed long, unsigned long, signed long long, unsigned long long
• auto-signed-first - Uses the first type that can hold all of the enumerator
values from the follo wing list:
, unsigned short, signed int, unsigned int, signed long,
short
unsigned long, signed long long, unsigned long long.
auto-unsigned-first - Uses the first type that can hold all of the
•
enumerator values from the following lists:
signed char, unsigned char, signed
signed int, unsigned int,
- If enumerator values are all positive: unsigned char, unsigned short,
unsigned int, unsigned long, unsigned long long.
- If one or more enumerator values are negative: signed char, signed
, signed int, signed long, signed long long.
short
-machine-architecture
This option specifies whether verification runs in 32 or 64-bit mode.
PolySpace Inner Settings
Note You should only use the option -machine-architecture 64 for
verifications that fail due to insufficient memory in 32 bit mode. Otherwise,
you should always run in 32–bit mode.
Available options are:
•
-machine-architecture auto – Verification a lways runs in 32-bit mode.
-machine-architecture 32 – Verification always runs in 32-bit mode.
•
-machine-architecture 64 – Verification always runs in 64-bit mode.
•
Default:
auto
Example Shell Script Entry:
polyspace-cpp -machine-architecture auto
-max-processes
This option specifies the maximum number of processe s that can run
simultaneously on a multi-core system. The valid range is 1 to 128.
Note To disable parallel p rocessing, set: -max-processes 1.
Default:
4
Example Shell Script Entry:
polyspace-cpp -max-processes 1
1-51
1 Options Description
-extra-flags option-extra-flag
This option specifies an expert option to be added to the analyzer. Each word
of the option (even the p aramete rs) must be preceded by -extra-flags.
These flags will be given to you by PolySpace Support as necessary for your
verifications.
Default:
No extra flags.
Example Shell Script Entry:
polyspace-cpp -extra-flags -param1 -extra-flags -param2
-cpp-extra-flags flag
ItspecifiesanexpertoptiontobeaddedtoaPolySpaceC++verification. Each
word of the option (even the parameters) must be preceded by -cpp-extra-flags.
1-52
These flags will be given to you by PolySp ace support as necessary.
Default:
no extra flags.
Example Shell Script Entry:
polyspace-cpp -cpp-extra-flags -stubbed-new-may-return-null
-il-extra-flags flag
ItspecifiesanexpertoptiontobeaddedtoaPolySpaceC++verification. Each
word of the option (even the parameters) must be preceded by -il-extra-flags.
These flags will be given to you by PolySp ace support as necessary.
Default:
no extra flags.
Example Shell Script Entry:
polyspace-cpp -il-extra-flags flag
PolySpace Inner Settings
1-53
1 Options Description
Precision/Scaling
In this section...
“-quick (Deprecated)” on page 1-54
“-O(0-3)” on page 1-55
“-from verification-phase” on page 1-56
“-to verification-phase” on page 1-57
“-context-sensitivity "proc1[,proc2[,...]]"” on page 1-58
“-context-sensitivity-auto” on page 1-58
“-path-sensitivity-delta number” on page 1-59
“-k-limiting number” on page 1-59
“-inline "proc1[,proc2[,...]]"” on page 1-60
“-respect-types-in-globals” on page 1-61
“-respect-types-in-fields” on page 1-61
1-54
“-less-range-information” on page 1-62
“-no-pointer-information” on page 1-63
“Tuning P recision and Scaling Parameters” on page 1-64
-quick (Deprecated)
Note This option is deprecated in R2009a and later releases.
quick mode is obsolete and has been replaced with verification PASS0.
PASS0 takes somewhat longer to run, but the results are more complete.
The limitations of
no variable dictionary) no longer apply. Unlike
provides full navigation in the Viewer.
This option is used to select a very fast mode for PolySpace .
quick mode,(noNTLorNTCchecks,nofloatchecks,
quick mode, PASS0 also
Precision/Scaling
Benefits
This option allows results to be generated very quickly. These are suitable
for initial verification of red and gray errors only, as orange checks are too
plentiful to be relevant using this option.
Limitations
• No NTL or NTC are displayed (non termination of loop/call)
• The variable dictionary is not available
• No check is performed on floats
• The call tree is available but navigation is not possible
• Orange checks are too plentiful to be relevant
-O(0-3)
This option specifies the precision lev el to be used. It provides higher
selectivity in exchan ge for more verification time, therefore making results
review more efficient and hence making bugs in the code easier to isolate. It
does so by specifying the algorithms used to model the program state space
during verification.
The MathWorks recommends you begin with the lowest precision level. Red
errors and gray code can then be addressed before relaunching PolySpace
verification using higher precision levels.
Benefits:
• A higher precision level contributes to a higher selectivity rate, making
results review more efficient and hence making bugs in the cod e easier to
isolate.
• A higher precision level also means higher verification time
- -O0 corresponds to static interval verification.
- -O1 corresponds to complex polyhedron model of domain values.
- -O2 corresponds to more complex algorithms to closely model domain
values (a mixed approach with integer lattices and complex polyhedrons).
1-55
1 Options Description
- -O3 is only suitable for code smaller than 1000 lines of code. For such
codes, the resulting selectivity might reach high values such as 98%,
resulting in a very long verification time,suchasanhourper1000lines
of code.
Default:
-O2
Example Shell Script Entry:
polyspace-cpp -O1 -to pass4 ...
-from verification-phase
This o ption specifies the verification phase to start from. It can only be used
on an existing verification, possibly to elaborate on the results that you have
already obtained.
1-56
For example, if a verification has been completed -to pass1, PolySpace can be
restarted -from pass1 and hence save on verification time.
The option is usually used in a verification after one run with the -to option,
although it can also be used to recover after p ow er failure.
Possible values are as described in the -to verification-phase section, with the
addition of the scratch option.
Note
• This option can only be used for client verifications. All server verifications
start from scratch.
• Unless the scratch option is used, this option can be used only if the
previous verification was launched using the option -keep-all-files .
• This option cannot be used if you modify the source code between
verifications.
Precision/Scaling
Default :
From
scratch
Example Shell Script Entry :
polyspace-cpp -from c-to-il ...
-to verification-phase
This option specifies the verification phase after which the verification will
stop.
Benefits:
This option provides improved selectivity, making results review more
efficient and making bugs in the code easier to isolate.
• A higher integration level contributes to a higher selectivity rate, leading
to "finding more bugs" with the code.
• A higher integration level also means longer verification time
Possible values:
•
cpp-compliance or “C++ source compliance checking”(Reachesthe
compilation phase)
•
cpp-normalize or “C++ source normalization” (Reaches the
normalization phase)
•
cpp-link or “C++ Link” (Reaches the link phase)
cpp-to-il or “C++ to Intermediate Language” (Reaches the
•
transformation to intermediate language)
•
pass0 or “Software Safety Analysis level 0”
pass1 or "Software Safety Analysis level 1"
•
pass2 or "Software Safety Analysis level 2"
•
pass3 or "Software Safety Analysis level 3"
•
1-57
1 Options Description
• pass4 or "Software Safety Analysis level 4"
other (stop verification after level 20)
•
Note If you use -to other then PolySpace w ill continue until you stop it
manually (via "PolySpace Install Directory"/bin/kill-rte-kernel "Results
directory"/"log file name") or stops until it has reached pass20.
Default:
pass4
Example Shell Script Entry:
polyspace-cpp -to "Software Safety Analysis level 3"...
polyspace-cpp -to pass0 ...
1-58
-context-sensitivity " proc1[,proc2[,...]]"
This option allows the precise verification of a procedure with regards to the
discrete calls to it in the analyzed code.
Each check inside the procedure is split into several sub-checks depending
on the context of call. Therefore if a check is red for one call to the procedure
and green for another, both colors will be revealed.
This option is esp ecially useful is a problem function is called from a m ultitude
of places.
-context-sensitivity-auto
This option is similar to the -context-sensitivity option, except that the system
automatically chooses the procedures to be considered.
Usually, the ten functions which are the most called are automatically
selected.
Precision/Scaling
-path-sensitiv
This option is us
aparticularpas
information w i
specified. Tha
Consider two v
without this o
• alevel1anal
or 2 in the (wi
• a level 1 ana
1+2 analysi
• thesameap
with poten
Gains usi
• (+) highe
• (-) This
even big
• (-) This
ed to improve interprocedural verification precision within
s(see-topass1, pass2, pass3 or pass4). The propagation of
thin procedures is done earlier than usual when this option is
t resu l ts in improved selectivity and a longer verification time.
erifications, one with this option set to 1 (with), and one
ption (without)
ysis in (with) (pass1) will provide results equivalent to level 1
thout) analysis
lysis in (with) can last x times more than a cumulated level
s from (without). "x" might be exponential.
plies to level 2 in (with) equivalent to level 3 or 4 in (without),
tially exponential analysis time for (a)
ng the option
st sele ctiv ity obtained in level 2. no need to wait until level 4
parameter increases exponentially the analysis time and might be
ger than a cumulated analysis in level 1+2+3+4
option can only be used with less than 1000 lines of code
ity-delta number
Defaul
0
Examp
poly
-k-l
Thi
dur
Th
t:
le Shell Script Entry:
space-cpp -path-sensitivity-delta 1 ...
imiting number
s is a scaling option to limit the depth of verification into nested structures
ing pointer verification (see Tuning Precision and Scaling Parameters).
is option is only available for PolySpace C and C++.
1-59
1 Options Description
Default:
Thereisnofixedlimit.
Example Shell Script Entry:
polyspace-cpp -k-limiting 1 ...
In this example above, verification will be precise to only one level of nesting.
-inline "proc1[,proc2[,...]]"
A scaling option that creates a clone of a each specified proce dure for each
call to it.
Cloned procedures follow a naming convention:
procedure1_pst_inlined_nb
1-60
where nb is a unique number giving the total number of inlined procedures.
Inlining allows the number of aliases inagivenproceduretobereduced,
and it may also improve precision.
It can also allow you to more easily locate run-time errors that relate the copy
or set of a large structure to a smaller one (NTC, for instance).
Restrictions :
• Extensive use of this option may duplicate toomuchcodeandmayleadto
other scaling problems. Carefully choose procedures to inline.
• This option should be used in response to the inlining hints provided
by the alias verification (the log file can sometimes provide this kind of
information).
• This option should not be used on main, task entry points and critical
section entry points.
• When using this option with a method of a class, all ov erlo ad of the method
will apply to the inline.
Precision/Scaling
Example Shell Script Entry:
polyspace-cpp inline myclass::myfunc …
-respect-types-in-globals
This is a scaling option, designed to help process complex code. When it is
applied, PolySpace assumes that global variables not declared as containing
pointers are never used for holding pointer values. This option should only
be used with Type-safe code , when it does not cause a loss of precision. See
also -respect-types-in-fields.
In the follow i ng example, we will lose precision using the
–respect-types-in-globals option:
int x;
void t1(void) {
int y;
int *tmp = &x;
*tmp = (int)&y;
y=0;
*(int*)x = 1; // x contains address of y
assert (y == 0); // green with the option
}
PolySpace will not take care that x contains the address of y resulting a
green assert.
Default:
PolySpace assumes that global variables may contain pointer values.
Example Shell Script Entry:
polyspace-cpp -respect-types-in-globals ...
-respect-types-in-fields
This is a scaling option, designed to help process complex code. When it is
applied, PolySpace assumes that structure fields not declared as containing
1-61
1 Options Description
pointers are never used for holding pointer values. This option should only
be used with Type-safe code , when it does not cause a loss of precision. See
also -respect-types-in-globals .
In the following example, we will lose p r ecision using option
respect-types-in-fields option:
struct {
unsigned x;
int f1;
int *z[2];
}S1;
void funct2(void) {
int *tmp;
int y;
((int**)&S1)[0] = &y; /* S1.x points on y */
tmp = (int*)S1.x;
y=0;
*tmp = 1; /* write 1 into y */
assert(y==0);
}
1-62
PolySpace will not take care that S1.x contains the address of y resulting a
green assert.
Default:
PolySpace assumes that structure fields may contain pointer values.
Example Shell Script Entry:
polyspace-cpp -respect-types-in-fields ...
-less-range-information
Limits the amount of range information displayed in verification results.
When you select this option, the software pro vide s range information on
assignments, but not on reads and operators.
Precision/Scaling
In addition, selecting this option enables the no-pointer-information
option. See “-no-pointer-information” o n page 1-63.
Computing range information for reads and operators may take a long time.
Selecting this option can reduce verification time significantly. Consider the
following example:
x=y+z;
If you do not select this option (the default), the software displays range
information when y ou place the cursor over
x, y, z,or+. However, if you
select this opti on , the software displays range information only when you
place the cursor over
x.
Default:
Disabled.
Example Shell Script Entry :
polyspace-cpp -less-range-information
-no-pointer-information
Stops the display of pointer information in verification results.
When you select this option, the software does n ot provide pointer information
through tooltips. As computing pointer information may take a long time,
selecting this option can significantly reduce verification time.
Consider the following example:
x=*p;
If you do not select this option (the default), the software displays pointer
information when you place the cursor on
software does not display pointer information.
Default:
p or *. If you select this option, the
1-63
1 Options Description
Disabled.
Example Shell Script Entry :
polyspace-cpp -no-pointer-information
Tuning Precision and Scaling Parameters
Precision versus Time of Verification
There is a compromise to be made to balance the time required to obtain
results, and the precision o f those results. Conseque n tly, launching PolySpace
with the following options will allow the time taken for verification to be
reduced but will compromise the precision of the results. It is suggested
that the parameters should be used in the sequence shown - that is, if the
first suggestion does not increase the speed of verification sufficiently then
introduce the second, and so on.
1-64
• switch from -O2 to a lower precision;
• set the -respect-types-in-globals and -respect-types-in-fields options;
• set the -k-limiting option to 2, then 1, or 0;
• stub manually missing functions which write into their arguments.
Precision versus Code Size
PolySpace can make approximations when computing the possible values
of the variables, at any point in the program. Such an approximation will
always use a superset of the actual possible values.
For instance, in a relatively small application, Poly S pace might retain very
detailed information about the data at a particular point in the code, so that
for example the variable VAR can take the values { -2; 1; 2; 10; 15; 16; 17; 25
}. If VAR is used to divide, the division is green (because 0 is not a possible
value). If the program being analyzed is large, P olySpace would simplify the
internal data representation by using a less precise approximation, such
as [-2; 2] U {10} U [15 ; 17] U {25} . Here, the same division appears as an
orange check.
Precision/Scaling
If the complexity of the internal data becomes even greater later in the
verification, PolySpace might further simplify the VAR range to (say) [-2; 20].
This phenomenon leads to the increase or the number of orange warnings
when the size of the program becomes large.
Note The amount of simplification applied to the data representations also
depends on the required precision level (O0, O2), PolySpace will adjust the
level of simplification:
•
-O0: shorter computation time. You only need to focus o n red and gray
checks.
• -
O2: less orange warnings.
-O3: less orange warnings and bigger computation time.
•
1-65
1 Options Description
MultiTasking (PolySpace Server for C/C++ Only)
In this section...
“-entry-points str1[,str2[,...]]” on page 1-66
“-critical-section-[begin or end] "proc1:cs1[,proc2:cs2]"” on page 1-66
“-temporal-exclusions-file file_name” on page 1-67
Note Concurrency options are not compatible with -main-generator options.
-entry-points str1[,str2[,...]]
This option is used to specify the tasks/entry points to be analyzed by
PolySpace, using a Comma-separated list with no spaces.
These entry points must not take parameters. If the task entry points are
functions with parameters they should b e encapsulated in functions with no
parameters, with parameters passed through global variables instead.
1-66
Format:
• All tasks must have the prototype “
• It is possible to declare a member function as an entry point of a verification,
only and only if the function is declared “
Example Shell Script Entry:
polyspace-cpp -entry-points class::task_name,taskname,proc1,proc2
void any_name() .
static void task_name()”.
-critical-section-[begin or end] "proc1:cs1[,proc2:cs2]"
-critical-section-begin "proc1:cs1[,proc2:cs2]"
and
-critical-section-end "proc3:cs1[,proc4:cs2]"
MultiTasking (PolySpace Server for C /C++ Only)
These options specify the procedures beginning and ending critical sections,
respectively. Each uses a list enclosed within double speech marks, with
list entries separated by commas, and no spaces. Entries in the lists take
the f orm of the procedure name followed by the name of the critical section ,
with a colon separating them.
These critical sections can be used to model protection of shared resources,
or to model interruption enabling and disabling.
Limitation:
• Name of procedure accept only void any_ name() as prototype.
• The beginning and the end of the critical section need to be defined in same
block of code.
Default:
no critical sections.
Example Shell Script Entry:
polyspace-cpp -critical-section-begin "start_my_semaphore:cs" \
-critical-section-end "end_my_semaphore:cs"
-temporal-exclusions-file file_name
This option specifies the name of a file. That file lists the sets of tasks which
neverexecuteatthesametime(temporalexclusion).
Theformatofthisfileis:
• one line for each group of temporally excluded tasks,
• on each line, tasks are separated by spaces.
Default:
No temporal exclusions.
1-67
1 Options Description
Example Task Specification file
File named ’exclusions’ (say) in the ’sources’ directory and containing:
task1_group1 task2_group1
task1_group2 task2_group2 task3_group2
Example Shell Script Entry :
polyspace-cpp -temporal-exclusions-file sources/exclusions \
-entry-points task1_group1,task2_group1,task1_group2,\
task2_group2,task3_group2 ...
1-68
Specific Batch Options
In this section...
“-server server_name_or_ip[:port_number]” on page 1-69
“-sources-list-file file_name” on page 1-70
“-v | -version” on page 1-70
“-h[elp]” on page 1-70
-server server_name_or_ip[:port_number]
Using polyspace-remote[-desktop]-[ada] [ server [name or IP
address][:<port number>]]
referenced PolySpace server.
Note If the option –server is not specified, the default se rve r referenced in
the
PolySpace-Launcher.prf configuration file will be used as server.
Specific Batch Options
allows you to send a verification to a specific or
When a –server option is associated to the batch launching command, the
name or IP address and a port number need to be specified. If the port number
does not exist, the 12427 value will be used by default.
Note polyspace-remote- accepts all other options.
Option Example Shell Script Entry:
polyspace-remote-desktop-cpp server 192.168.1.124:12400
polyspace-remote-cpp
polyspace-remote-cpp server Bergeron
1-69
1 Options Description
-sources-list-file file_name
This option is only available in batch mode. The syntax of file_name is the
following:
• Onefileperline.
• Each file name includes its absolute or relative path.
Example Shell Script Entry for -sources-list-file:
polyspace-cpp -sources-list-file "C:\Analysis\files.txt"
polyspace-cpp -sources-list-file "/home/poly/files.txt"
-v | -version
Display the PolySpace version number.
Example Shell Script Entry:
1-70
polyspace-cpp v
It will show a result similar to:
PolySpace r2008a
Copyright (c) 1999-2008 The Mathworks Inc.
-h[elp]
Display in the shell window a simple help in a textual format giving
information on a ll options.
Example Shell Script Entry:
polyspace-cpp h
Check Descriptions
• “Check Categories” on page 2-2
• “Colored Source Code for C++” on page 2-10
2
2 Check Descriptions
Check Categories
This section presents all categories of checks that PolySpace software verifies.
These checks are classified into acronyms. E ach acronym represents one or
more verifications made by PolySpace software. The list of acronyms, checks
and ass ociated colored messages are listed in the following tables.
In this section...
“Acronyms associated to C++ specific constructions:” on page 2-2
“Acronym Not Related to C++ Constructions (Also Used for C Code):” on
page 2-7
Acronyms associated to C++ specific constructions:
Category
function
value
non null
this-pointer
C++ related
instructions
returns a
Acronym
FRV
NNT
CPP
CPP
CPP
CPP dynamic_cast on reference
INF
Green Gray
function
this-po
array size is strictly p ositive Unreachable check: array
type
dynamic_cast on pointer is
correct
is correct
Informative check: f is
implicitly called
returns a value
inter [of f] is not null
id argument is correct
Unreachable check:
function returns a value
Unreachable check:
this-pointer [of f] is not
null
size is strictly positive
achable check: typeid
Unre
ment is correct
argu
Unreachable check:
dynamic_cast on pointer is
correct
Unreachable check:
dynamic_cast on reference
is correct
Informative check: implicit
call of f is unreachable
2-2
Check Categories
Category
Display of errors
that relate to
Object Oriented
Programming and
inheritance
Acronym
Green Gray
OOP callofvirtualfunction[f]is
not pure
OOP this-pointer type [of f] is
correct
INF
Informative check: f is
called if this-pointer is of
type T
OOP pointer to member function
points to a valid member
function
OOP
INF
Informative check: f is
potentially called through
pointertomemberfunction
INF
Informative check: f is
called during construction
of T
Unreachable check: call of
pure virtual function [f]
Unreachable check:
this-pointer type [of f]
is correct
Informative check: call of
f depending on this type is
unreachable
Unreachable check: pointer
to member function points
to a valid member function
Unreachable check: call to
no function Information
Informative check:
potentialcalltofthrough
pointer to member function
is unreachable
Informative check: call of f
during construction of T is
unreachable
Display of errors
that relate to
exception handling
INF
Informative check: f is
called during destruction of
T
EXC exception raised as specified
in the throw list
EXC
catch parameter
construction does not
throw
EXC
dynamic initialization does
not throw
Informative check: call of
f during destruction of T is
unreachable
Unreachable check:
exception raised as specified
in the throw list
Unreachable check: catch
parameter construction
does not throw
Unreachable check:
dynamic initialization
does not throw
2-3
2 Check Descriptions
Category
Category
function returns a
value
Acronym
EXC
EXC main, task or C library
EXC call [to f] does not throw
EXC function does not throw
EXC
EXC
Acronym
FRV
Green Gray
destructor or delete does not
throw
function does not throw
expression value is not
EXCEPTION_CONTINUE_
EXECUTION
Red
Error: function does not
return a value
Unreachable check:
destructor or delete does not
throw
Unreachable check: main,
task or C library function
does not throw
Unreachable check: call [to
f] does not throw
Unreachable check:
function does not throw
Unreachable check:
expression value is not
EXCEPTION_CONTINUE_
EXECUTION
Unreachable check: throw
is not allowed with option
-no-exception
Orange
Warning: function may not
return a value
2-4
non null
this-pointer
NNT
Error: this-pointer [of f] is
null
Warning: this-pointer [of f]
may be null
Check Categories
Category
C++ related
instructions
Display of errors
that relate to
Object Oriented
Programming and
inheritance
Acronym
CPP
Red
Error: array size is not
strictly positive
CPP
Error: incorrect typeid
argument
CPP
Error: incorrect
dynamic_cast on pointer
(verification continues using
a null pointer)
CPP
Error: incorrect dynamic
cast on reference
INF
OOP Error: call of pure virtual
function [f]
OOP
Error: incorrect this-pointer
type [of f]
INF
OOP
Error: pointer to member
function is null or points to
an invalid member function
Orange
Warning: array size may not
be strictly positive
Warning: typeid argument
may be incorrect
Warning: dynamic_cast on
pointer may be incorrect
Warning: dynamic_cast on
reference may be incorrect
Warning: call of virtual
function [f] may be pure
Warning: this-pointer type
of [f] may be incorrect
Warning: pointer to member
function may be null or
point to an invalid member
function
OOP Internal PolySpace error:
please contact support
INF
INF
INF
2-5
2 Check Descriptions
Category
Display of errors
that relate to
exception handling
Acronym
EXC
EXC
EXC
EXC
EXC Error: main, task or C
EXC Error: call [to f] throws
EXC Error: function throws
EXC
Red
Error: exception raised is
not specified in the throw
list
Error: throw during catch
parameter construction
Error: throw during
dynamic initialization
Error: throw during
destructor or delete
library function throws
(verification jumps to
enclosing handler)
(verification jumps to
enclosing handler)
Error: expression value is
EXCEPTION_CONTINUE_
EXECUTION (lim itation)
Orange
Warning: exception raised
may not be specified in the
throw list
Warning: poss ible throw
during catch parameter
construction
Warning: possible
throw during dynamic
initialization
Warning: poss ible throw
during destructor or delete
Warning: main, task or C
library function may throw
Warning: call [to f] may
throw
Warning: function may
throw
Warning: expression
value may be
EXCEPTION_CONTINUE_
EXECUTION (lim itation)
2-6
EXC
Error: throw is not allowed
with option -no-exception
Check Categories
Acronym Not Rela
Used for C Code):
Category
Out of bound array
index
Zero division
Non-initia
variable
scalar or f
overflows
Illegal d
pointer
Correct
conditi
Shiftamountoutof
bounds
lized
loat
ereference
ness
on
ted to C++ Constructions (Also
Acronym
OBAI Array index is within its
ZDV
NIV
local/other
OVFL
IDP
COR
COR
COR
COR
SHF Scalar shift amount is
Green Gray
bounds
[local] var
Referenc
object
Function pointer must point
to a valid function
within its bounds
iable is initialized
ereferstoavalid
Unreachable check: out of
bounds array index error
Unreachable check:
Unreachabl
Unreachable check: variable
overflow error
Unreachable check: invalid
reference
Unreachable check:
Function pointer must
point to a valid func tion
Unreachable check: shift
error
echeck:
Non initialized
pointer
user assertion
failures
non termination of
call
non termination of
loop
Unreachable check
SHF
P
NI
ASRT User assertion is verified
NTC
NTL
UNR
Reference is initialized
Unreachable check:
non-initialized reference
nreachable check: user
U
assertion error
Unreachable code
2-7
2 Check Descriptions
Category
Out of bound array
index
Zero division
Non-initialized
variable
scalar or float
overflows
Illegal dereference
pointer
Correctness
condition
Shiftamountoutof
bounds
Acronym
OBAI Out of bound array Array index may be outside
ZDV
NIV
local/other
OVFL
IDP
COR
COR wrong type for argument of
COR wrong number of arguments
COR Array conversion must not
SHF Scalar shift amount is
Red
[scalar | float] division by
zero occurs
[local] variable is not
initialized
Reference refers to an
invalid object
Function pointer must point
to a valid function
extend range
outside its bounds
Orange
its bounds
[scalar | float] division by
zero may occur
[local] variable may not
initialized
Reference may not refer to
avalidobject
Function pointer may point
to a valid function
call to function
for call to function
Non initialized
pointer
user assertion
failures
non termination of
call
2-8
SHF Left operand of left shift is
negative
NIP
ASRT User assertion fails User assertion may fail
NTC [f] call never terminates
Reference is not initialized
Reference may be
non-initialized
Check Categories
Category
non termination of
loop
Unreachable check
Acronym
NTL
UNR
Red
non terminatio n of loo p
Orange
2-9
2 Check Descriptions
Colored Source Code for C++
In this section...
“Function Returns a value: FRV” on page 2-11
“Non Null this-pointer: NNT” on page 2-12
“Positive Array Size: CPP” on page 2-14
“Incorrect typeid Argument: CPP” on page 2-15
“Incorrect dynamic_cast on Pointer: CPP” on page 2-16
“Incorrect dynamic_cast on Reference: CPP” on page 2-18
“Invalid Pointer to Member: OOP” on page 2-19
“Call of Pure Virtual Function: OOP” on page 2-20
“Incorrect T ype for this-pointer: OOP” on page 2-21
“Potential Call to: INF” on page 2-24
“Non-Initialized Variable: NIV/NIVL” on page 2-26
2-10
“Non-Initialized Pointer: NIP” on page 2-27
“User Assertion Failure: ASRT” on page 2-28
“Overflows and Underflows” on page 2-30
“ScalarorFloatDivisionbyzero: ZDV”onpage2-34
“Shift Amount is Outside its Bounds: SHF” on page 2-35
“Left O perand of Left Shift is Negative: SHF” on page 2-36
“POW (Deprecated)” on page 2-38
“Array Index is Outside its Bounds: OBAI” on page 2-38
“Function Pointer Must Point to a Valid Function: COR” on page 2 -39
“Wrong Number of Arguments: C OR ” on page 2-40
“Wrong Type of Argument: COR” on page 2-41
“Pointer is Outside its Bounds: IDP” on page 2-42
“Function throws: EXC” on page 2-50
“Call to Throws: EXC” on page 2-52
Colored Source Code for C++
In this section...
“Destructor or Delete Throws: EXC” on page 2-54
“Main, Tasks or C Library Function Throws: EXC” on page 2-56
“Exception Raised is Not Specified in the Throw List: EXC” on page 2-58
“Throw Du ring Catch Parameter Construction: EXC” on page 2-60
“Continue Execution in __except: EXC” on page 2-62
“Unreachable Code: UNR” on page 2-63
“Non Terminations: Calls and Loops” on page 2-65
Function Returns a value: FRV
Check to establish whether on every value-returning function there is no
flowing off the end the function.
C++ Example
1 static volatile int rand;
2
3 class function {
4 public:
5 function() { rep =0;}
6 int reply(int msg) { // FRV Verified: [function returns
a value]
7if(msg > 0) return rep;
8};
9
10 int reply2(int msg) { // FRV ERROR: [function does not
return a value]
11 if (msg > 0) return rep;
12 };
13
14 int reply3(int msg) { // FRV Warning: [function may not
return a value]
15 if (msg > 0) return rep;
16 };
17
2-11
2 Check Descriptions
18 protected:
19 int rep ;
20 };
21
22 void main (void){
23
24 int ans;
25 function f;
26
27 if (rand)
28 ans = f.reply(1);
29
30 else if (rand)
31 ans = f.reply2(0); // NTC ERROR: propagation of FRV ERROR
32 else
33 f.reply3(rand);
34 }
2-12
Explanation
Variables are often initialized using the return value of functions. However it
may occur that, as in the above example, the return value is not initialized for
all input parameter values (which should always be the case). In this case,
the target variable will not be properly initialized with a valid return.
Non Null this-pointer: NNT
This check verifies that the this pointer is null during call of a member
function.
C++ Example
1#include <new>
2 static volatile int random_int =0;
3
4 class Company
5{
6 public:
7 Company(int numbClients):numberClients(numbClients){};
Colored Source Code for C++
8 void newClients (int numb) {
9 numberClients = numberClients + numb;
10 }
11 protected:
12 int numberClients;
13 };
14
15 void main (void)
16 {
17 Company *Tech = 0;
18
19 if (random_int)
20 Tech->newClients(2); // NNT ERROR: [this-pointer of
newClients is null]
21
22 Company *newTech = new Company(2);
23 newTech->newClients(1); // NNT Verified: [this-pointer
of newClients is not null]
24
25 }
26
Explanation
Polyspace verifies that all functions, virtual or not virtual, by a direct calling,
and through pointer calling are never called with a null this-pointer.
In the above example, a pointer to a Company object is declared and initialized
to null. When the newClients member function of the Company classiscalled
(line 20), PolySpace detects that theclassobjectisanullpointer.
On the new allocation at line 22, as standard new operator returns an
initialized pointer or raises an exception, the this-pointer is considered as
correctly allocated at line 23.
2-13
2 Check Descriptions
Positive Array Size: CPP
This check verifies that the array size isalwaysanon-negativevalue. Inthe
following example, the array is defined with a negative value by a function
call.
C++ Example
1 static volat
2 static volat
3
4 class Licen
5 public:
6 Licence(i
7 void initA
8 protecte
9 int numbe
10 int (*ar
11 };
12
13 Licenc
14 array =
size is n
15 initA
16 }
17
18 void
19 for (
20 arra
21 }
22 };
23
24 vo
25 {
26 if
27 Li
pro
28 }
id main (void)
pagation of PAS ERROR
d:
ray)[2];
e::Licence(int nUser) : numberUser(nUser) {
new int [numberUser][2]; // PAS ERROR: [array
ot strictly positive]
rray();
Licence::initArray() {
int i = 0; i < numberUser; i++){
y[i][2]=0;
(random_int && random_user != 0)
cence FirmUnknown (-random_user); // NTC ERROR:
ile int random_int =1;
ile unsigned short int random_user;
ce {
nt nUser);
rray();
rUser;
2-14
Colored Source Code for C++
Explanation
The property, the non-negative value of an array size, is checked at line
14, where the array is defined with the [numberUser][1] dimension.
Unfortunately the numberUser variable is always negative as an opposite
of an unsigned short int type. PolySpace detects a red error and displays a
message.
Incorrect typeid Argument: CPP
Check to establish whether a typeid argument is not a null pointer dereference.
This check only occurs using typeid function declared in stl library <typeinfo>.
C++ Example
1 #include <typeinfo>
2
3 static volatile int random_int=1;
4
5 class Form
6{
7 public:
8 Form (){};
9 virtual void trace(){};
10 };
11
12 class Circle : public Form
13 {
14 public:
15 Circle():Form(){};
16 void trace(){};
17 };
18
19
20 int main ()
21 {
22
23 Form* pForm = 0 ;
24 Circle *pCircle = new Circle();
25
2-15
2 Check Descriptions
26 if (random_int)
27 return (typeid(Form) == typeid(*pForm)); // CPP ERROR:
[incorrect typeid argument]
28 if (random_int)
29 return (typeid(Form) == typeid(*pCircle)); // CPP Verified:
[typeid argument is correct]
30 }
31
32
33
34
Explanation
In this example, the pForm variable is a pointer to a Form object and
initialized to a null pointer. Using the typeid standard function, an exception
is raised. In fact here, the typeid parameter of an expression obtained by
applying the unary "*" operator is a null pointer leading to this red error.
2-16
At line 29, *pCircle is not null and typeid can be applied.
Incorrect dynamic_cast on Pointer: CPP
Check to establish when only valid pointer casts are performed through
dynamic_cast operator. +
C++ Example
1 #include <new>
2 static volatile int random = 1;
3
4 class Object {
5 protected:
6 static Object* obj;
7 public:
8 virtual ~Object() {}
9};
10
11 class Item : Object {
Colored Source Code for C++
12 private:
13 static Item* item;
14 public:
15 Item();
16 };
17
18 Object* Object::obj = new Object;
19
20 Item::Item() {
21 if (obj != 0) {
22 item = dynamic_cast<Item*>(obj); // CPP ERROR: [incorrect
dynamic_cast on pointer (verification continue using a null pointer)]
23 if (item == 0) { // here analyzed and reachable code
24 item = this;
25 }
26 }
27 }
28
29 void main()
30 {
31 Item *first= new Item();
32 }
Explanation
Only the dynamic casting between a subclass and its upclass is auth ori zed .
So, the casting of Object object to a Item object is an error on dynamic_cast at
line 21, because Object is not a subclass of Item.
Behavior follows ANSI C++ standard, in sense that even if dynamic_cast
is forbidden, verification continue using null p ointer. So at line 22, item is
considered as null and assigned to this at line 23.
Note This is only check where we can have another color after a red.
It is not the case for a dynamic_cast on a reference.
2-17
2 Check Descriptions
Incorrect dynamic_cast on Reference: CPP
Check to establish when only v alid reference casts are performed through
dynamic_cast operator.
C++ Example
1 #include <new>
2 static volatile int random =1;
3 class Object {
4 protected:
5 static Object* obj;
6 public:
7 virtual ~Object() {}
8};
9
10 class Item : public Object {
11 private:
12 static Item* item;
13 public:
14 Item& get_item();
15 Item& other_item();
16 };
17
18 Object* Object::obj = new Object;
19
20 Item& Item::get_item() {
21 Item& ref = dynamic_cast<Item&>(*Object::obj);
// CPP ERROR: [incorrect dynamic_cast on reference]
22 *item = ref;
// unreachable code
23 }
24
25 void main ()
26 {
27 Item * first= new Item();
28 if (random)
29 first->get_item();
// NTC ERROR: propagation of dynamic_cast reference error
30 Object &refo = dynamic_cast<Object&>(first->other_item());
2-18
Colored Source Code for C++
// CPP Verified: [dynamic_cast on reference is correct]
31 }
Explanation
Only the dynamic casting between a subclass and its upclass is auth ori zed .
So, the casting of reference Object object to a reference Item object is an error
on dynamic_cast at line 20, because Object is not a subclass of Item.
The verification stops at line 20 and the error is propagated to a NTC error at
line 28. The behavior is different with a dynamic_cast on a pointer.
Invalid Pointer to Mem ber: OOP
PolySpace checks that the pointer to a function member is invalid or null.
C++ Example
1
2 class A{
3 public:
4 void f() {
5}
6};
7
int main() {
8
9
10 void (A::*pf)(void) = &A::f;
11 int (A::*pf2)(void) = (int (A::*)(void))&A::f;
12
13 volatile int random;
14 A a;
15
16 if (random){
17 int res = (a.*pf2)() ; // RED OOP ERROR [pf2 points to A::f \
that does not return a value]
18 res++;
19 }
20
2-19
2 Check Descriptions
21 pf = 0;
22 if (random){
23 (a.*pf)() ; // Red OOP ERROR [pf pointer is null]
24 }
25 }
Explanation
When a function pointer operates on a null pointer to a m ember value, the
behavior is undefined. In the above example, the pf pointer is declared and
initialized to a null member function. When the function is called (at line 23)
a red error is raised. In addition, the pf2 pointer points to
A::f, that does not
return a value, raising another red error at line 17.
Call of Pure Virtual Function: OOP
This check detects a pure virtual function call.
C++ Example
2-20
1
2 class Form
3{
4 public:
5Form(Form* f){};
6 Form(Form* f, char* title){
7 f->draw(); // OOP Error: [call to pure virtual \
function draw()]
8};
9 virtual void draw() = 0;
10 };
11
12 class Rectangle : public Form
13 {
14 public:
15 Rectangle(): Form (this, "Rectangle"){} ;
16 void draw();
17 };
18
19 void Rectangle::draw () {
Colored Source Code for C++
20 Form::draw(); // Draw the rectangle
21 };
22
23 void main (void)
24 {
25 Rectangle Rect1;
26 Rect1.draw();
27 }
Explanation
The effect of making a virtual call to a pure virtual function directly or
indirectly for the object being created (or destroyed) from such a constructor
(or destructor) is undefined (see Standard ANSI ISO/IEC 1998 pp. 199).
One Rectangle object is declared: Rect1 calls the constructor (line 15), and so
the Form constructor (line 6) whose the draw() function member is called.
Unfortunately, this function is a pure virtual function. PolySpace points
out a warning at line 7.
Incorrect Type for this-pointer: OOP
Check to verify that a member function is associated to the right instance of
a class.
Three principal causes lead to an incorrect this-pointer type:
• An out of bounds pointer access
• A non initialized variable member
• An inadequate cast.
Thefollowingexampleshowsthethreepossiblecases.
C++ Example
1 #include <new>
2
3 int get_random_value(void);
2-21
2 Check Descriptions
4
5 struct A {
6 virtual int f();
7};
8
9 struct C {
10 virtual int h() { return 7; }
11 };
12
13 void f(void) {
14 struct T {
15 int m_j;
16 C m_field;
17 T() : m_j(m_field.h()) {} // OOP ERROR (initialisation): \
[incorrect this-pointer type of T]
18 } badInit;
19 int r;
20
21
22 r = badInit.m_j;
23 }
24
25 class Bad
26 {
27 public:
28 int i;
29 void f();
30 Bad() : i(0) {}
31 };
32
33
34 class Good
35 {
36 public:
37 virtual void g() {}
38 void h() {}
39 static void k() {}
40 };
41
42 int main()
2-22
Colored Source Code for C++
43 {
44
45 A* a = new A;
46 Good *ptr = (Good *)(void *)(new Bad);
47
48 a->f(); // OOP Verified: [this-pointer type of \
A is correct]
49
50 if (get_random_value()) {
51 C* c = new C;
52 ++c;
53 c->h(); // OOP ERROR (out of bounds): \
[incorrect this-pointer type of C]
54 }
55
56 if (get_random_value()) ptr->g(); // OOP ERROR (cast): \
[incorrect this-pointer type of Bad]
57 if (get_random_value()) ptr->h(); // OOP ERROR (cast): \
[incorrect this-pointer type of Bad]
58
59 ptr->k(); // correct call to a static function
60
61 f();
62
63 }
Explanation
At line 17 of the exam ple, PolySpace identifies a this-pointer type problem
(OOP category), because of an initialization missing for member field m_field.
At line 53 of the example, PolySpace points out that even if the function
member h is part of the c Class, we are outside the structure. It could be
compared to IDP for simple class.
Finally, lines 56 and 57 show another this-pointer problems: function
members g and h are not part of the Bad Class. Good does not inherited from
Bad. Note that there is no problem with static function member k because it
is only syntaxic.
2-23
2 Check Descriptions
Potential Call t
[potential call
of PolySpace dur
to] are informative checks that help to understand reasoning
o: INF
ing function calls, constructions and destructions of objects
through
C++ Example
1 #include <iostream>
2 static volatile int random_int = 1 ;
3
4 typedef enum { AOP, UTC, GET } valueKind;
5
6 class SubVal {
7 valueKind val;
8 void init();
9 public:
10 SubVal(valueKind v);
11 virtual ~SubVal() {} // INF informative: \
[operator_delete(void*) is implicitly called]
12
13 virtual void log(const char* msg);
14 valueKind getVal() {return val;};
15 void undef();
16 };
17
18 SubVal::SubVal(valueKind v) : val(v){
19 init();
20 }
21
22 void SubVal::init() {
23 log("SubVal creation"); // INF informative: \
[SubVal::log(const_char*) is called during construction of SubVal]
24 }
25
26 void SubVal::log(const char* msg) {
27 cout << msg;
28 }
29
30 void SubVal::undef() {
2-24
Loading...