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 New 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
Option Descriptions
1
PolySpace Analysis Options Overview ............... 1-2
Contents
General Options
General Options Overview
Session identifier (-prog)
Date (-date)
Author (-author)
Project Version (-verif-version)
Keep all preliminary results files (-keep-all-files)
Report Generation
Report template name (report-template)
Output format (-report-output-format)
Report name (-report-output-name)
-results-dir Results Directory
-sources "files" or -sources-list-file file_name
-I directory
-continue-with-red-error (Deprecated)
-continue-with-existing-host (Deprecated)
-allow-unsupported-linux (Deprecated)
Target/Compiler Options
Overview
-target TargetProcessorType
GENERIC ADVANCE D TARGET OPTIONS
-OS-target OperatingS ystem T arg etFo rPolySp ace S tub s
-D compiler-flag
-U compiler-flag
-include file_name
-post-preprocessing-command <file_name> or
"command"
-post-analysis-command <file_name> or "command"
................................... 1-3
.......................... 1-4
............................ 1-4
...................................... 1-4
.................................. 1-5
....................... 1-5
................................. 1-7
............... 1-7
................ 1-8
................... 1-8
........................ 1-9
........... 1-10
....................................... 1-11
................. 1-12
.............. 1-12
................ 1-13
........................... 1-14
........................................ 1-14
........................ 1-14
........... 1-15
................................... 1-22
................................... 1-23
................................. 1-23
..................................... 1-24
........ 1-6
... 1-22
..... 1-25
Compliance with Standards Option s
-dos
............................................. 1-27
................ 1-27
iii
Embedded Assembler .............................. 1-28
Strictness during verification launching
Permissiveness during verification launching
MISRA-C 2004 Rules
-dialect [iar|keil]
-sfr-types
........................................ 1-36
.............................. 1-33
.................................. 1-35
............... 1-29
.......... 1-30
PolySpace Inner Settings Options
-unit-by-unit
-unit-by-unit-common-source filename
MAIN GENERATOR OPTIONS (-main-generator) for
PolySpace Software
Stubbing
Assumptions
Automatic Orange Tester
-machine-architecture
-max-processes
Others
Precision/Scaling Options
-quick (Deprecated)
-O(0-3)
-modules-precision mod1:O(0-3)[,mod2:O(0-3)[,...]]
-from verification-phase
-to verification-phase
-context-sensitivity "proc1[,p r oc2 [ ,.. .]] "
-context-sensitivity-auto
-path-sensitivity-delta number
-retype-pointer
-retype-int-pointer
-k-limiting number
-no-fold
-respect-types-in-globals
-respect-types-in-fields
-inline "proc1[,proc2[,...]]"
-lightweight-thread-model
-less-range-information
-no-pointer-information
..................................... 1-37
.............................. 1-38
......................................... 1-42
..................................... 1-44
........................... 1-52
.............................. 1-53
.................................... 1-54
.......................................... 1-55
.......................... 1-57
................................ 1-58
.......................................... 1-58
............................ 1-60
.............................. 1-61
............................ 1-62
.................................... 1-63
................................. 1-64
................................ 1-66
.......................................... 1-66
............................ 1-66
............................. 1-67
........................... 1-68
.......................... 1-69
............................. 1-69
............................. 1-70
................... 1-37
................ 1-38
................ 1-62
....................... 1-62
....... 1-59
iv Contents
Multitasking Options (PolySpace
Product Only)
-entry-points str1[,str2[,...]]
-critical-section-[begin or end] "proc1:cs1[,proc2:cs2]"
................................... 1-72
®
Server for C/C++
......................... 1-72
.... 1-72
-temporal-exclusions-file file_name ................... 1-73
Batch Options
-server server_name_or_ip[:port_number]
-sources-list-file file_name
-v | -version
-h[elp]
........................................... 1-76
..................................... 1-75
.............. 1-75
.......................... 1-75
...................................... 1-76
Check Descriptions
2
Colored Source Code for C ......................... 2-2
Illegal Pointer Access to Variable or Structure Field:
IDP
........................................... 2-3
Array C onve rsio n Must Not Extend R ange: COR
Array Index Within Bounds: OBAI
Initialized Return Value: IRV
Non-Initialized Variables: NIV/NIVL
Non-Initialized Pointer: NIP
POW (Deprecated)
User Assertion: ASRT
Scalar and Float Overflows: OVFL
Scalar and Float Underflows: UNFL (Deprecated)
Float Underflows and Overflows: UOVFL (Deprecated)
Scalar or Float Division by Zero: ZDV
Shift Amount in 0..31 (0..63):SHF
Left Operand of Left Shift is Negative: SHF
Function Pointer Must Point to a Valid Function: COR
Wrong Type for Argument: COR
Wrong Number of Arguments: COR
Wrong Return Type of a Function Pointer: COR
Wrong Return Type for Arithmetic Functions: COR
Pointer Within Bounds: IDP
Non Termination of Call or Loop
Unreachable Code: UNR
Inspection Points
................................. 2-8
.............................. 2-8
........................... 2-44
.................................. 2-46
................... 2-5
....................... 2-6
................. 2-7
........................ 2-8
................... 2-10
................. 2-14
.................... 2-15
..................... 2-18
.................. 2-18
........................ 2-21
..................... 2-34
........ 2-4
....... 2-14
............ 2-16
........ 2-19
.. 2-14
... 2-16
..... 2-20
v
Approximations Used During Verification
3
Why PolySpace Verification Uses Approximations .... 3-2
What is Static Verification
Exhaustiveness
................................... 3-3
.......................... 3-2
Approximations Made by PolySpace Verification
Volatile Variables
Structures with Volatile Fields
Absolute Addre sses
Pointer Comparison
Shared Variables
Trigonometric Function s
Unions
Constant Pointer
.......................................... 3-6
................................. 3-4
...................... 3-4
................................ 3-5
............................... 3-5
.................................. 3-5
............................ 3-6
.................................. 3-7
Examples
4
Complete Examples ................................ 4-2
Simple C Example
Apache Example
cxref Example
T31 Example
Dishwasher1 Example
Satellite Example
................................. 4-2
.................................. 4-2
.................................... 4-3
..................................... 4-3
............................. 4-3
................................. 4-4
..... 3-4
vi Contents
Option Descriptions
• “PolySpace Analysis Options Overview” on page 1-2
• “General Options” on page 1-3
• “Target/Compiler Options” on page 1-14
• “Compliance with Standards Options” on page 1-27
• “PolySpace Inner Settings Options” on page 1-37
• “Precision/Scaling Options” on page 1-57
®
• “Multitasking Options (PolySpace
page 1-72
Server for C/C++ Product Only)” on
1
• “Batch Options” on page 1-75
1 Option Descriptions
PolySpace Analysis Options Overview
The analysis options in the upper-right section of the Launcher window
include identification information and parameters that PolySpace
uses during the verifica tion process.
PolySpac
display t
side of t
Note Ea
set fro
descri
e software groups the analysis options into various categories. To
he parameters for a specific category, expand the category on the left
he dialog box.
ch of the parameters in the Analysis options window can also be
m the command line using the
ption includes the corresponding command line information.
polyspace-c command. Each parameter
®
software
1-2
General Options
In this section...
“General Options Overview” on page 1-4
“Session identifier (-prog)” on page 1-4
“Date (-date)” on page 1-4
General Options
“Author (-author)” on page 1-5
“Project Version (-verif-version)” on page 1-5
“Keep all preliminary results files (-keep-all-files)” on page 1-6
“Report Generation” on page 1-7
“Report template name (report-template)” on page 1-7
“Output format (-report-output-format)” on page 1-8
“Report name (-report-output-name)” on page 1-8
“-results-dir Results Directory” on page 1-9
“-sources "files" or -sources-list-file file_name” on page 1-10
“-I directory” on page 1-11
“-continue-with-red-error (Deprecated)” on page 1-12
“-continue-with-existing-host (Deprecated)” on page 1-12
“-allow-unsupported-linux (Deprecated)” on page 1-13
1-3
1 Option Descriptions
General Options
This General sec
verification, i
tion contains options relating to the identification of the
ncluding the destination directory for the results and sources.
Session ident
Specify a name
for the project.
Overview
ifier (-prog)
Settings
Default: New
• The Session
• Use only cha
_Project
identifier cannot contain spaces.
racters that are valid for UNIX file names.
Command-Line Information
r:
Paramete
Value: any valid value
Example:
-prog
polyspace-c -prog myApp ...
Date (-date)
Specify a date stamp for the verification.
1-4
Settin
Default: Date the verification is launched
By default, the date stamp uses the
gs
dd/mm/yyyy format.
Tip
YoucanspecifyanalternativedateformatbyselectingEdit > Preferences
> Miscellaneous in the Launcher.
Command-Line Information
Parameter: -date
Value: any valid value
Example:
polyspace-c -date "02/01/2002"...
Author (-author)
Specify the name of the person performing the verification.
Settings
Default: username of the current user.
Note The default username is obtained with the whoami command.
Command-Line Information
General Options
Parameter: -author
Value: any valid value
Example:
polyspace-c -author "John Tester"
Project Version (-verif-version)
Specify a version identifier for the ve r if ication.
Settings
Default: 1.0
Tip
Thisoptioncanbeusedtoidentify different verifications.
1-5
1 Option Descriptions
Command-Line Information
Parameter: -verif-version
Value: any valid value
Example:
polyspace-c -verif-version 1.3
Keep all preliminary results files (-keep-all-files)
Specify whether to retain all intermediate results and associated working files.
Settings
Default: Off
On
Retain all intermediate results and associated working files. You can
restart a verification from the end of any complete pass if the source
code remains unchanged.
Off
Erase all intermediate results and associated working files. If you want
to restart a verification, do so from the beginning.
1-6
Tips
• When you select this option you can restart PolySpa ce 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.
• This option is applicable only to client verifications. Intermediate results
are always removed before results are downloaded from the PolySpace
server.
• To cleanup intermediate files at a later time, you can select Tools > Clean
Results in the Launcher. This option deletes the preliminary result files
from the results folder.
General Options
Command-Line Information
Parameter: -keep-all-files
Example: polyspace-c -keep-all-files
Report Generation
Specify whether to create verification report using report generation options
Settings
Default: Off
On
Create report.
Off
No report created.
Report template n ame (report-template)
Specify report template for generating verification report.
Settings
Default:
C:\PolySpace\PolySpace_Common\ReportGenerator\templates\Developer.rpt
• Report generated at the end of the verification process, before e xecution
of any
post-analysis-command.
Command-Line Information
Parameter: report-template
Type: string
Value: any valid script file name
Example:
c:/polyspace/my_template
polyspace-c -report-template
1-7
1 Option Descriptions
Output format (-repor t-output-format)
Specify output format of report
Settings
Default: RTF
RTF
Generate an .rtf format report.
HTML
Generate an .html format report.
PDF
Generate a .pdf format report.
Word
Generate a .doc format report.
Word is not available on UNIX
XML
Generate and .xml format report.
Note WORD format is not available on UNIX platforms, RTF format is used
instead.
®
platforms. RTF is used instead.
Command-Line Information
Parameter: report-output-format
Type: string
Value:
Default: RTF
Shell script example:
polyspace-c -report-template my_template report-output-format pdf
RTF | HTML | PDF | Word | XML
Report name (-report-output-name)
Specify name of verification report file
1-8
Settings
Default: Prog_TemplateName.Format where:
•
Prog is the argument of the prog option
TemplateName is the name of the report template specified by the
•
report-template option
Format is the file extension for the format specified by the
•
report-output-format option.
Command-Line Information
Parameter: report-output-name
Type: string
Value: any valid value
Default:
Shell script example:
Prog_TemplateName.Format
General Options
polyspace-c -report-template my_template report-output-name Airbag_V3.rtf
-results-dir Results Directory
This option specifies the directory in which PolySpace software will write the
results of the verification. Note that although relative directories may be
specified, particular care should be taken with their use especially where
the tool is to be launched remotely over a network, and/or w here a project
configuration file is to be copied using the "Save as" option.
Default:
Shell Script: The directory in which tool is launched.
From Graphical User Interface: C:\PolySpace_Results
Example Shell Script Entry:
polyspace-c -results-dir RESULTS ...
export RESULTS=results_`date +%d%B_%HH%M_%A`
polyspace-c -results-dir `pwd`/$RESULTS ...
1-9
1 Option Descriptions
-sources "files" or -sources-list-file file_name
Specifies a list of source files to be verified.
The list of source files must be double-quoted and separated by commas.
•
-sources "file1[ file2[ ...]]" (Linux
-sources "file1[,file2[, ...]]" (Windows
•
-sources-list-file file_name (not a graphical option)
•
®
and Solaris™)
®
, Linux and Solaris)
Note UNIX standard w ild cards are available to specify a number of files.
The source files are compiled in the order in which they are specified.
Note If y ou do not specify any files, the software verifies all files in the
source directory in alphabetical order.
Note The specified files must have valid extensions:
*.(c|C|cc|cpp|CPP|cxx|CXX)
Defaults:
sources/*.(c|C|cc|cpp|CPP|cxx|CXX)
1-10
Example Shell Script Entry under linux or solaris (files are separated
with a white space):
polyspace-c -sources "my_directory/*.cpp" ...
polyspace-c -sources "my_directory/file1.cc other_dir/file2.cpp"
...
Example Shell Script Entry under windows (files are separated with a
comma):
General Options
polyspace-c -sources "my_directory/file1.cpp,other_dir/file2.cc"
...
Using -sources-list-file,eachfilename need to be given with an absolute
path. Moreover, the sy ntax of the file is the following:
• 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-c -sources-list-file "C:\Analysis\files.txt"
polyspace-c -sources-list-file "/home/poly/files.txt"
-I directory
This option is used to specify the name of a directory to be included when
compiling C sources. Only one directory may be specified for each –I, but the
option can be used multiple times.
Default:
• When no directory is s pecified using this option, the ./sources directory (if
it exists) is automatically included
• If several include-dir are mentioned, the ./sources directory (if it exists), is
implicitly added at the end of the "-I" list
Example Shell Script Entry-1:
polyspace-c -I /com1/inc -I /com1/sys/inc
is equivalent to
polyspace-c -I /com1/inc -I /com1/sys/inc -I ./sources
1-11
1 Option Descriptions
Example Shell Script Entry-2:
polyspace-c
is equivalent to
polyspace-c -I ./sources
-continue-with-red-error (Deprecated)
Note This option is deprecated in R2009a and later releases, and no longer
exists in the user interface. Verification now continues to the next integration
pass even if a red errors is encountered.
This option allows PolySpace verification t o continue even if one of these
red errors is encountered. In most cases, this will mean that the dynamic
behavior of the code beyond the point where red errors are identified will be
undefined, unless the red code is actually inaccessible.
1-12
-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.
General Options
-allow-unsuppo
Note This option
exists in the us
of the Linux dis
the software d
This option s
unsupported
PolySpace s
Software Re
oftware supports the Linux distributions listed in “Hardware and
quirements” in the PolySpace Installation Guide.
is deprecated in R2010a and later releases, and no longer
er i nte rface. P ol yS pace verification now continues regardless
tribution. If the Linux distribution is no t officially supported,
isplays a wa rning in the log file.
pecifies that PolySpace verification will be launched on an
OS Linux distribution.
rted-linux (Deprecated)
1-13
1 Option Descriptions
Target/Compiler Options
In this section...
“Overview” on page 1-14
“-target TargetProcessorType” on page 1-14
“GENERIC ADVANCED TARGET OPTIONS” on page 1-15
“-OS-target OperatingSystemTargetForPolySpaceStubs” on page 1-22
“-D compiler-flag” on page 1-22
“-U compiler-flag” on page 1-23
“-include file_name” on page 1-23
“-post-preprocessing-command <file_name> or "command"” on page 1-24
“-post-analysis-command <file_name> or "command"” on page 1-25
Overview
This sectio n allows details of the target processor and operating system to be
specified. Header files should not be entered here; instead, include directories
should be added using the relevant field under the Compile flag op t ion s .
1-14
-target TargetProcessorType
This option specifies the target processor type, and in doing so informs the
verification of the size of fundamental data types and of the endianess of the
target machine.
Possible values are:
sharc21x61, necv850, hc08, hc12, mpc5xx, c18,andmcpu (Advanced).
mcpu is a reconfigurable Micro Controller/Processor Unit target. You can
configure one or more generic targets. Also code which is to be run on an
unlisted processor type can be analyzed using one of the other processor types
listed, if the data properties which a re relevant to PolySpace verification are
common. For more information, see “Setting Up Project for Generic Target
Processors” in the PolySpace Products for C User’s Guide.
sparc, m68k, powerpc, i386, c-167, tms320c3x,
Target/Compiler Options
Instructions on the specification of a generic target and on the modification
of the mcpu target are available in “GENERIC ADVANCED TARGET
OPTIONS” on page 1-15.
Default:
sparc
Example shell script entry:
polyspace-c -target m68k ...
GENERIC ADVANCED TARGET OPTIONS
The Generic target options dialog box is only available when you select a
mcpu target.
Allows the specification of a generic "Micro Controller/Processor Unit" or
mcpu target name. Initially, it is necessary to use the GUI to specify the name
of a new mcputarget – say, “MyTarget”.
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 [8,8], 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:
1-15
1 Option Descriptions
polyspace-c -target MyTarget
For example, a specific target uses 8 bit alignment (see also -align ), for which
the command line would read:
polyspace-c -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:
1-16
polyspace-c -target mcpu -little-endian
-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
Target/Compiler Options
-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
• default mode – Thesignofcharislefttoassumethetarget’sdefault
behavior. By default all targets are considered as signed except for hc08
and powerpc targets.
• signed – Disregards the target’s default char definition, 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-c -default-sign-of-char unsigned -target mcpu ...
-char-is-16bits
This option is only available when a -mcpu generic ta rge t has be en chosen.
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 o p t ions -short-is-8bits and -align 8.
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-c -target mcpu -char-is-16bits
1-17
1 Option Descriptions
-short-is-8bits
This option is only available when a mcpu 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, regardless 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-c -target mcpu -short-is-8bits
-int-is-32bits
This option is available with a mcpu generic target, hc08, hc12 and mpc5xx
target has been chosen.
1-18
The default configuration of a generic target defi n es an int as 16 bits. This
option changes it to 3 2 bits, regardless 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-c -target mcpu -int-is-32bits
-long-long-is-64bits
This option is only available when a mcpu 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, regardless of sign. When a long long is used
as struct member or array component, its alignment is also set to 64 bits.
Seealso-alignoption.
Example shell script entry
Target/Compiler Options
polyspace-c -target mcpu -long-long-is-64bits
-double-is-64bits
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
This option is available for the following targets:
• mcpu generic target
• sharc21x61
• hc08
• hc12
• mpc5xx
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;
}
1-19
1 Option Descriptions
Using the default configuration of sharc21x62, PolySpace verification
assumes that a value of 1 is assigned to s1, 2 is assigned to s2, and there
is a consequential float overflow in the multiplication x * 2. Usin g the
–double-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
polyspace-c -target mcpu -double-is-64bits
-pointer-is-32bits
This option is only available when a mcpu 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
1-20
polyspace-c -target mcpu -pointer-is-32bits
-align [8|16|32]
This option is available with a mcpu generic target and some other specific
targets (with hc08, hc12 or mpc5xx available values are 16 and 32). 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.
-align 32 (Default). The default alignment of a generic target is 3 2 bits.
This means that when objects with a sizeofmorethan4bytesareusedas
struct members or array components, they are aligned at 4 byte boundaries.
Example shell script entry with a 32 bits default alignment
polyspace-c -target mcpu
-align 16. If the -align 16 option is used, when objects with a size of
more than 2 bytes are used as struct members or array components, they
are aligned at 2 bytes boundaries.
Target/Compiler Options
Example shell script entry with a 16 bits specific alignment:
polyspace-c -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.
Example shell script entry with a 8 bits specific alignment:
polyspace-c -target mcpu -align 8
-logical-signed-right-shift
In the Graphical User Interface, the user can choose between arithmetical
and logical computation.
• - Arithmetic: the sign bit remains:
(-4) >> 1 = -2
(-7) >> 1 = -4
7>>1=3
• - Logical: 0replacesthesignbit
(-4) >> 1 = (-4U) >> 1 = 2147483646
(-7) >> 1 = (-7U) >> 1 = 2147483644
7>>1=3
Example shell script entry
When using the command line, a r ithmetic is the default computation mod e.
When this option is set, logical computation will be performed.
polyspace-c -logical-signed-right-shift
1-21
1 Option Descriptions
-OS-target
OperatingSystemTargetForPolySpaceStubs
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 or/and -D to give
all of the system preprocessor flags to be used at executio n time. Details
of these may be found by executing the compiler for the project in verbose
mode. They are also listed in this document - search for keyword "OS-target
option"
Default:
Solaris
1-22
Note Only the Linux include files are provided 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
it is necessary to use the option -I <<path_to_the_VxWorks_include_folder>>
Example shell script entry:
polyspace-c -OS-target linux
polyspace-c -OS-target no-predefined-OS -D GCC_MAJOR=2 /
-include /complete_path/inc/gn.h ...
®
project
-D compiler-flag
This option is used to define macro compiler flags to be used during
compilation phase.
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.
Target/Compiler Options
Default:
Some defines are applied by default, depending on your -OS-target option.
Example Shell Script Entry:
polyspace-c -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:
Some undefines may be set by default, depending on your -OS-target option.
Example Shell Script Entry:
polyspace-c -U HAVE_MYLIB -U USE_COM1 ...
-include file_name
This option 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-c -include `pwd`/sources/a_file.h -include
/inc/inc_file.h ...
polyspace-c -include /the_complete_path/my_defines.h ...
1-23
1 Option Descriptions
-post-preprocessing-command <file_name> or
"command"
When this option is used, the specified script file or command is run just
after the preprocessing phase on each source file. T he script executes on
each preprocessed c file. The command should be designed to process the
standard output from preprocessing and produce its results in accordance
with that standard output.
Note You can find each preprocessed file in the results directory in the
zipped file ci.zip located in <results/ALL/SRC/MACROS. The extension of
the preprocessed file is .ci.
It is important to preserve the number of lines in the preprocessed .ci file.
Adding a line or removing one could result in some unpredictable behavior on
the location of checks and MACROS in the PolySpace viewer.
Default:
1-24
No command.
Example Shell Script Entry – file name:
To replace the keyword “Volatile” by “Import”, you can type the following
command on a Linux workstation:
polyspace-c -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/;
Target/Compiler Options
print $line;
}
Note If you are running PolySpace software version 5.1 (r2008a) or later on
a Windows system, you cannot use Cygw in™ 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-c.exe
-post-preprocessing-command
%POLYSPACE_C%\Verifier\tools\perl\win32\bin\perl.exe
<absolute_path>\replace_keywords
-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 of the architecture used (notably when using remote
launcher), the script can be executed on the client side or the server side.
Default:
No command.
1-25
1 Option Descriptions
Example Shell Script Entry – file name:
This example shows how to send an email to tip the client side off that his
verification has been ended. So the command looks like:
polyspace-c -post-analysis-command `pwd`/end_emails
where end_emails 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
1-26
To run the Perl script provided in the previous example on a Windows
workstation, you must use this option with the absolute path to the Perl
script, for example:
%POLYSPACE_C%\Verifier\bin\polyspace-c.exe -post-analysis-command
%POLYSPACE_C%\Verifier\tools\perl\win32\bin\perl.exe
<absolute_path>\end_emails
Compliance with Standards Options
In this section...
“-dos” on page 1-27
“Embedded Assembler” on page 1-28
“Strictness during ver if ication launching” on page 1-29
“Permissiveness during verification launching” on page 1-30
“MISRA-C 2004 Rules” on page 1-33
“-dialect [iar|keil]” on page 1-35
“-sfr-types” on page 1-36
-dos
Compliance with Standards Options
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)
• 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:
1-27
1 Option Descriptions
disabled by default
Example Shell Script Entry:
polyspace-c -I /usr/include -dos -I ./my_copied_include_dir -D test=1
Embedded Assembler
• “-discard-asm” on page 1-28
• “Pragmas asm” on page 1-28
-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:
1-28
Embedded assembler is treated as an error.
Example Shell Script Entry:
polyspace-c -discard-asm ...
Pragmas asm
-asm-begin "mark1[mark2[...]] "
and
-asm-end "mark1[mark2[...]]"
Theseoptionsareusedtoallowcompilerspecific asm functions to be excluded
from the verification, with the offending co de block delimited by two #pragma
directives.
Consider the following example.
#pragma asm_begin_1
Compliance with Standards Options
int foo_1(void) { /* asm code to be ignored by PolySpace */ }
#pragma asm_end_1
#pragma asm_begin_2
void foo_2(void) { /* asm code to be ignored by PolySpace */ }
#pragma asm_end_2
Where "asm_begin_1" and "asm_begin_2" marks the beginning of asm
sections which will be discarded and “
asm_end_1”, respectively "asm_end_2"
mark the end of those sections.
Also refer to the -discard-asm option with regards to the following code:
asm int foo_1(void) { /* asm code to be ignored by PolySpace */ }
asm void foo_2(void) { /* asmcode to be ignored by PolySpace */ }
Note The asm-begin and asm-end options must be used together.
Example Shell Script Entry:
polyspace-c -discard-asm -asm-begin "asm_begin_1,asm_begin_2"
-asm-end "asm_end_1,asm_end_2"
…
Strictness during verification launching
• “-strict” on page 1-29
• “-wall” on page 1-30
-strict
This option selects the Strict mode of PolySpace verification. It is equivalent
to using the -Wall and -no-automatic-stubbingoptions simultaneously.
This option is not compatible with -asm-begin and -asm-end options.
1-29
1 Option Descriptions
-wall
When this option is used, the C compliance phase will print all warnings.
For example, with this option, a warning will raise in the log file during
compilation phase when trying to write into a const variable: “warning:
assignment of read-only member <var>”
Default:
By default, only wa rn in gs about compliance across different files
are printed.
Example Shell Script Entry:
polyspace-c -Wall ...
Permissiveness during verification launching
• “-permissive”onpage1-30
1-30
• “-permissive-link” on page 1-31
• “-allow-non-int-bitfield” on page 1-31
• “-allow-undef-variables” on page 1-31
• “-ignore-constant-overflows” on page 1-32
• “-allow-unnamed-fields” on page 1-32
• “-allow-negative-operand-in-shift” on page 1-33
-permissive
This option selects the PolySpace permissive mode, which is eq uivalent
to the simultaneous use of -allow-non-int-bitfield, -allow-undef-variables,
-ignore-constant-overflows, -discard-asm, -permissive-stubber,
-continue-with-red-error, and -permissive-link.
Compliance with Standards Options
-permissive-link
When this option is used, PolySpace verification acceptsintegraltype
conflicts between declarations and definitions on arguments or/and returning
functions.
It has an effect only
• when the size of a conflicting integral type is not greater tha n int, or
• conflicts occur between a pointer type and an integral type of same size.
Default:
By default, P olySpace verification does not accept any conflicts between
declarations and definitions.
-allow-non-int-bitfield
This option allows the user to define types of bitfields other than those
specified by ANSI
int types only.
®
C. The standard accepts bitfields of signed and unsigned
Default:
Bitfields must be signed or unsigned int.
Example Shell Script Entry :
polyspace-c -allow-non-int-bitfield ...
-allow-undef-variables
When this option is used, PolySpace verification will continue in case of
linkage errors due to undefined global variables. For instance when this
option is used, PolySpace verification will tolerate a variable always being
declared as extern
Default:
Undefined variables causes PolySpace verification to stop.
1-31
1 Option Descriptions
Example Shell Script Entry:
polyspace-c -allow-undef-variables ...
-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 regardless of the use
of the option.
1-32
char x = (rn d?0xFF:0xFE);
Default:
char x = 0xff; causes an overflow
Example Shell Script Entry:
polyspace-c -ignore-constant-overflows ...
-allow-unnamed-fields
When this option is used, PolySpace verification will continue in case of
compilation errors due to unnamed fields in structures. For instance when
this option is used, PolySpace verification will tolerate a structure where
fieldsareunnamedsincetherearenoduplicatenames. Withtheoption,
the following source code is tolerate:
struct {
Compliance with Standards Options
union { int x; int y;}
union {int z; int w;}
}s;
s.x = 2; s.z = 2;
Default:
Unnamed fields cause PolySpace to stop.
Example Shell Script Entry:
polyspace-c -allow-unnamed-fields ...
-allow-negative-operand-in-shift
This option permits a shift operation on a negative number.
According to the ANSI C standard, such a shift operation on a negative
number is illegal – for example,
-2 << 2
With this option in use, PolySpace verification considers the operation to b e
valid. In the 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-c -allow-negative-operand-in-shift ...
MISRA-C 2004 Rules
• “ -misra2 [all-rules | file_name]” on page 1-34
1-33
1 Option Descriptions
• “-includes-to-ignore "dir_or_file_path1[,dir_or_file_ pa t h 2[ ,.. .] ]"” on page
1-34
-misra2 [all-rules | file_name]
This option permits to check set of coding rules in conformity to
MISRA-C:2004. All MISRA checks are included in the log file of the
verification.
• Keyword all-rules: It checks all available MISRA C
®
rules. It implies
theuseofthedefaultconfiguration: any violation of MISRA C rules is
considered as a warning.
• Option filename: it is the name of an absolute ASCII file containing a list
of MISRA
®
rules to check.
Format of the file:
<rule number> off|error|warning
# is considered as comments.
Example:
# MISRA configuration file for project C89
10.5 off # disable misra rule number 10.5
17.2 error # violation misra rule 17.2 as an error
17.3 warning # non-respect to misra rule 17.3 is a only a warning
Default:
disable
Example shell script entry:
polyspace-c -misra2 all-rules ...
1-34
polyspace-c -misra2 misra.txt
-includes-to-ignore "dir_or_file_path1[,dir_or_file_path2[,...]]"
This option prevents MISRA rules checking in a given list of files or directories
(all files and subdirectories under selected directory). This option is useful
Compliance with Standards Options
when non-MISRA C conforming include headers are used. A warning is
displayed if one of the parameter does no t exist.
This option is authorized only when -misra2 is used.
Example shell script entry :
polyspace-c -misra2 misra.txt includes-to-ignore
"c:\usr\include"
-dialect [iar|keil]
When this option is used, PolySpace ve rification will take into account some
non Target Support Package™ syntax and semantic associated to a chosen
dialect between IAR and Keil. It refers to the well known compilers of the
company IAR (www.iar.com) and Keil (www.keil.com).
Using this o pti on , PolySpace verification will tolerate s om e new structure
types as keyword of the language such sfr, sbit, bit etc. These structures and
associated semantics are part of the compilerthathaveintegrateditwiththe
ANSI C language as an extension.
Example of source code with keil dialect:
unsigned char bdata Status[4];
sfr AU = 0xF0;
sbit OCmd = Status[0]^2;
s^2 = 1; s^6 = 0;
Example with iar dialect:
unsigned char bdata Status[4];
sfr OCmd @ 0x4FFE;
OCmd.2 = 1; s.6 = 0;
Example Shell Script Entry:
polyspace-c dialect keil
1-35
1 Option Descriptions
-sfr-types
Associated to the option -dialect, if the code uses specific sfr type keyword, it
is mandatory to declare using –sfr-types option. It giv es the name of the sfr
type and its size in bits. The syntax is:
-sfr-types <sfr_name>=<size_in_bits>,
where <sfr_name> could be any name, but m ost of the time we encounter sfr,
sfr16 and sfr32 . <size in bits> could be one of the values 8, 16 and 32.
Default:
No dialect used.
Example Shell Script Entry:
polyspace-c dialect iar sfr-types sfr=8,sfr32=32,sfrb=16
1-36
PolySpace Inner Settings Options
In this section...
“-unit-by-unit” on page 1-37
“-unit-by-unit-common-source filename”onpage1-38
“MAIN GENERATOR OPTIONS (-main-generator) for PolySpace Software”
on page 1-38
“Stubbing” on page 1-42
“Assumptions” on page 1-44
“Automatic Orange Tester” on page 1-52
“-machine-architecture” on page 1-53
“-max-processes” on page 1-54
“Others” on page 1-55
PolySpace®Inner Settings Options
-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.
Note Unit by unit verification is available only for server verifications. It is
not compatible with m ultitasking options such as
Default:
Not selected
Example Shell Script Entry:
polyspace-c -unit-by-unit
-entry-points.
1-37
1 Option Descriptions
-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-c -unit-by-unit-common-source
c:/polyspace/function.c
MAIN GENERATOR OPTIONS (-main-generator) for
PolySpace Software
This same option can be used for both PolySpace®Client™ for C/C++ and
PolySpace
two:
®
Server™ for C/C++, but the default behavior differs between the
1-38
• Using PolySpace Server the user has the choice as to whether to activate
the option.
• Using PolySpace Client the option is activated by default.
This section describes:
• “PolySpace
• “PolySpace
• “-main-generator (detailed options)” on page 1-39
• “-main-generator-writes-variables [ none | public | all | custom=v1,v2,.]”
on page 1-40
• “-function-called-before-main function_name” on page 1-40
• “-main-generator-calls [ none | unused | all | custom=f1,f2,...]” on page
1-41
®
Client for C/C++ default behavior” on page 1-39
®
Server for C/C++ default behavior” on page 1-39
PolySpace®Inner Settings Options
PolySpace Client for C/C++ default behavior
There is no need to ascertain whether the code for verification contains a
"main" or not. That is automatically checked by the PolySpace Client for
C/C++ product:
• If a main exists in the set of file(s), then the verification proceeds with
that main.
• Otherwise, the tool generates a main with default options:
-main-generator-writes-variables public and -main-generator-calls unused.
PolySpace Server for C/C++ default behavior
By default, if no main is found in a PolySpace Server for C/C++ verification,
then it will stop. This behavior can help isolate files missing from the
verification.
ItisalsopossibletoallowthePolySpaceServerforC/C++producttoascertain
whetherornotamainisavailable.
• If an available main is found, the verification proceeds as usual.
• Otherwise, the tool generates a main with the assumption of verifying a
library. The options used are -main-generator-writes-variables none and
-main-generator-calls none.
-main-generator (detailed options)
This option initiates the default behavior for PolySpace Launcher. The
generated main has three distinct default behaviors.
• It first initializes any variables identified by the option
-main-generator-writes-variables. The default setting for this option is
-main-generator-writes-variables public.
• It then calls a function which could be considered an initialization function
with the option -function-called-before-main.
• It then calls any functions identified by the option -main-generator-calls.
The d efault setting for this option is -main-generator-calls unused.
1-39
1 Option Descriptions
What follows are s eparate descriptions of the above options that include all of
the possible settings.
-main-generator-writes-variables [ none | public | all |
custom=v1,v2,.]
This option is use d with the -main-generator option to dictate how the
generated main w ill initialize global variables.
Settings available:
•
-none — no global variable will be written by the main.
-public — every variable except static and const variables are assigned a
•
“random” value, representing the full range of possible values
•
-all — every variable except const variables are assigned a “random”
value, representing the full range of possible values
•
-custom — only variables present in the list are assigned a “random” value,
representing the full range of possible values
1-40
Example
polyspace-c -main-generator -main-generator-writes-variables none
polyspace-c -main-generator -main-generator-writes-variables
custom=variable_a,variable_b
-function-called-before-main function_name
It is possible to specify an initialization function that will be called on startup
after the initialization of the global variables and before the main loop when
using the -main-generator option.
The skeleton of the generated main looks like:
1 Initialization of global variables
2 Call the specified function fname
3 main loop with a call to all the specified functions depending on option
-main-generator-calls
PolySpace®Inner Settings Options
Example shell script entry:
polyspace-c -main-generator function-called-before-main
MyInitFunction
-main-generator-calls [ none | unused | all | custom=f1,f2,...]
The generated main will call functions according to this option. It is used with
the -main-generator option, to specify the functions to be called.
Possible values:
•
none — no function is called. This can be used with a multitasking
application w ithout a main.
•
unused (default) — every function is called by the generated main unless it
is called elsewhere by the code undergoing verification.
•
all — every function is called by the generated main except inline d.
custom — only functions present in the list are called from the main.
•
Inlined functions can be specified in the list.
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.
Note When using the unused option, the generated main may call functions
that are also called by a function pointer, meaning these functions may be
called twice.
Example:
polyspace-c -main-generator -main-generator-calls public
polyspace-c -main-generator -main-generator-calls
custom=function_1,function_2
1-41
1 Option Descriptions
Stubbing
• “-data-range-s
• “-permissive-
• “-no-automat
pecifications file_name” on page 1-42
stubber” on page 1-43
ic-stubbing” on page 1-43
-data-range-specifications file_name
This option p
global varia
For more inf
Functions (
File forma
The file fi
variable_name val_min val_max <init|permanent|globalassert>
Variabl
Variabl
d variable ( i.e. could be extern with option -allow-undef-variables).
define
ermits the setting of specific data ranges for a list of given
bles.
ormation, see “Specifying Data Ranges for Variables and
Contextual Verification)”.
t:
lename contains a list of global v ariables with the below format:
es scope:
es concern external linkage, const variables and not necessary a
1-42
Note On
No che
Some
or ty
Def
Dis
ample shell script entry:
Ex
ly one mode can be applied to a global variable.
cks are added w ith this option except for globalassert mode.
warning can be displayed in log file concerning variables when format
pe is not in the scope.
ault:
able.
PolySpace®Inner Settings Options
polyspace-c -data-range-specifications range.txt ...
-permissive-stubber
By default, the stubber rejects functions:
• with complex function pointers as parameters
• with function pointers as return type
To eliminate these restrictions and stub all functions, specify the Stub all
functions (
Caution Using this option may produce inaccurate results.
Note This option cannot be used with the no-automatic-stubbing option.
-permissive-stubber)option.
-no-automatic-stubbing
By default, PolySpace verification automatically stubs all functions. When
this option is used, the list of func tions to be stubbed is displayed and the
verification is stopped.
Benefits:
This option may be used where
• Theentirecodeistobeprovided,whichmaybethecasewhenverifying
a large piece of code. Wh en the verification stops, i t means the code is
not complete.
• Manual stubbing is preferred to improve the selectivity and speed of the
verification.
Note This option cannot be used with the permissive-stubber option .
1-43
1 Option Descriptions
Default:
All functions are stubbed automatically
Assumptions
• “-div-round-down” on page 1-44
• “-no-def-init-gl ob” on p a ge 1-45
• “-size-in-bytes” on page 1-45
• “-allow-ptr-arith -on-struct” on page 1-46
• “-ignore-float-rounding” on page 1-48
• “-detect-unsigned-overflows” on page 1-50
• “-enum-type-definition” on page 1-51
• “-known-NTC proc1[,proc2[,...]]” on page 1-52
1-44
-div-round-down
This option concerns the division and modulus of a negative number.
The ANSI standard stipulates that "if either operand of / or % is negative,
whether the result of the / operator, is the largest integer less or equal than the
algebraicquotientorthesmallestintegergreaterorequalthanthequotient,is
implementation defined, same for the sign of the % operator".
Note a=(a/b)*b+a%bis always true.
Default:
Without the option (default mode), if either operand of /or%is negative,
the result of the / operator is the smallest integergreaterorequalthanthe
algebraic quotient. The result of the % operator is deduced from
-(a/b)*b
Example:
a%b=a
PolySpace®Inner Settings Options
assert(-5/3 == -1 && -5%3 == -2); is true .
With the -div-round-down option:
If either operand /or%is negative, the result of the / operator is the largest
integer less or equal than the algebraic quotient. The result of the % operator
is deduced from
a%b=a-(a/b)*b.
Example:
assert(-5/3 == -2 && -5%3 == 1); is true .
Example Shell Script Entry:
polyspace-c -div-round-down ...
-no-def-init-glob
This option specifies that PolySpace verification should nottakeintoaccount
default initialization defined by ANSI C. When this option is not used, default
initialization are
• 0forintegers
• 0 for characters
• 0.0 for floats
With the option in use, all global variable will be treated as non initialized and therefore cause a red error - if they are read before being written to.
Example Shell Script Entry :
polyspace-c -no-def-init-glob ...
-size-in-bytes
This option allows incomplete or partial allocation of structures. This
allocation can be made by m alloc or cast .
1-45
1 Option Descriptions
The example below shows an example using malloc. Further explanation can
be found in the section describing the partial and incomplete allocation of
structures. Also refer to the -allow-ptr-arith-on-struct section.
typedef struct _little { int a; int b; } LITTLE;
typedef struct _big { int a; int b; int c; } BIG;
BIG *p = malloc(sizeof(LITTLE));
Default results
p->a = 0 ; // red pointer out of its bounds
or p->b = 0 ; // red pointer out of its bounds
or p->c = 0 ; // red pointer out of its bounds
Results using this option
if (p!= ((void *) 0) ) {
p->a = 0 ; // green pointer within bounds
or p->b = 0 ; // green pointer within bounds
or p->c = 0 ; // red pointer out of its bounds
}
1-46
-allow-ptr-arith-on-struct
This option enables navigation within a structure or union from on e field
to another, within the rules defined below. It automatically sets the
-size-in-bytes option.
Default
By default, when a pointer points to a variable then the size of the o bjected
pointed to is that of that variable - regardless of whether it is contained
within a bigger object, like a structure. Therefore, going out of the scope of
this variable leads to a red IDP check (Illegal Dereference Pointer). This is
illustrated below.
struct S {char a; char b; int c;} x;
char *ptr = &x.b;
ptr ++;
*ptr = 1; // red on the dereference, because the pointed
object was "b"
PolySpace®Inner Settings Options
Using this option
When this option is used in the above option, PolySpace verification considers
that the object pointed to is now the host object "x". The "ptr" pointer is in
fact pointing to &x, with the correct offset to the field “b” within the structure
of type S (inter-fields and end-padding included). Therefore, the dereference
becomes green
Consider a second example:
int main()
{
struct S {
char a;
/* 3 bytes of padding between 'a', 'b' */
int b;
int c;
char d[3];
unsigned char e:7;
char f;
/* 3 bytes of end padding */
}x;
char *ptr;
struct Nesting_S {
struct S s;
int c;
char buf[8];
int d;
}z
struct S *ptr0;
char *ptr;
ptr = &z.s.f;
ptr += 4;
*(int *)ptr = 10; /* access to z.c, Green IDP */
ptr0 = &z.s;
ptr = &ptr0->f;
1-47
1 Option Descriptions
ptr += 4;
*(int *) ptr = 10; /* access to z.c, Green IDP */
ptr = &z.buf[0];
ptr += 8;
*(int *)ptr = 10; /* access to z.d, Green IDP */
return (0);
}
In the third example below, the *ptr access is red regardless of whether the
option is set or not.
With the option set, the ptr pointer points to the structure+offset z.s, and ptr
can safely navigate within t h is structure z.s, but z.c is outside it.
Without the option, the ptr pointer points to z.s.f, which is only 1 byte long.
So no navigation is allowed, not even within z.s.
1-48
ptr = (char *)z.s.f; ptr += 4; *ptr = 10; // ptr points to the
first byte of c:
-ignore-float-rounding
Without this option, PolySpace verification rounds floats accord ing to the
®
IEEE
on target which define double as 64-bits.
With the option, exact computation is performed.
Example:
754 standard: simple precision on 32-bits targets and double precision
void ifr(float f)
{
double a,b;
a = 0.2;
b = 0.2;
if(a+b==0.4){
PolySpace®Inner Settings Options
// reached whether -ignore-float-rounding is used or not
assert (1);
f = 1.0F*f;
}
else {
assert (1);
f = 1.0F * f;
// reached only when -ignore-float-rounding is not used
}
}
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 verification 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/UNFL 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 ± Δ
void ifr(float f)
{
double a,b;
a = 0.2;
b = 0.2;
if ( a + b == 0.4) {
assert (1);
f = 1.0F*f; // Overflow never occurs because f <= FLT_MAX.
// reached when -ignore-float-rounding is used
}
else {
assert (1);
f = 1.0F * f; // OVFL could occur when f = (FLT_MAX + D)
1-49
1 Option Descriptions
// reached when -ignore-float-rounding is not used
}
}
Default:
IEEE 754 round ing under 32 bits and 64 bits.
Example Shell Script Entry:
polyspace-c -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 C standard requires.
The ANSI C standard states that promotion occurs for logic, bitw ise and
arithmetic operators. For
cast into integers before the operation. Then, after the operation, the
variables are downcast into the original type.
char, short,andint types, variables are implicitly
1-50
Consider the examples below.
Example 1
Using this option, the following example generates an error:
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:
PolySpace®Inner Settings Options
unsigned char Y=1;
Y = ~Y; //overflow because of type promotion
In this example:
1 Y is coded as an unsigned char: 000000001
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-c -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:
•
defined-by-standard –Usestheintegertype(signed int).
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
•
signed char, unsigned char, signed
enumerator values from the following lists:
- If enumerator values are all positive: unsigned char, unsigned short,
unsigned int, unsigned long, unsigned long long.
- If one or more e nume rato r values are negative: signed char, signed
, signed int, signed long, signed long long.
short
1-51
1 Option Descriptions
-known-NTC proc1[,proc2[,...]]
After a few verifications, you may discover that a few functions "never
terminate". Some functions such as tasks and threads contain infinite loops
by design, while functions that exit the program such as kill_task , exit or
Terminate_Thread are often stubbed by means of an infinite loop. If these
functions are used very often or if the results are for presentation to a third
party, it may be desirable to filter all NTC of that kind in the V iewer.
This option is provided to allow that filtering to be applied . All NTC specified
at launch will appear in the viewer in the known-NTC category, and filtering
will be possible.
Default :
All checks for deliberate Non Terminating Calls appear as red errors, listed
in the same category a s any problem NTC checks.
Example Shell Script Entry :
1-52
polyspace-c -known-NTC "kill_task,exit"
polyspace-c -known-NTC "Exit,Terminate_Thread"
Automatic Orange Tester
-prepare-automatic-tests
This option activates the PolySpace Automatic Orange Tester. The Automatic
Orange Tester finds runtime errors in the orange (and red) checks remaining
at the end of the PolySpace verification.
The Automatic Orange Tester results contain precise information to help you
identify the cause of a runtime error. This complements the results review in
theViewermoduleofPolySpaceClientforC/C++.
For more information, see “Automatically Testing Orange Code”.
The following options are not compatible with
-prepare-automatic-tests.
PolySpace®Inner Settings Options
• -entry-points
• -dialect
• -ignore-float-rounding
• -div-round-down
• -entry-points
• -char-is-16bits
• -short-is-8bits
• -respect-types-in-globals
• -respect-types-in-fields
The following options cannot take specific values when you select
-prepare-automatic-tests.
•
-align [8|16]
• -target [c-167 | tms320c3c | hc08 | sharc21x61]
• -data-range-specification (in global assert mode)
In addition, when using the Automatic Orange Tester, the
option must be used together with -pointer-is-32bits.
Default :
Disabled
Example Shell Script Entry :
polyspace-c -prepare-automatic-tests ...
-target mcpu
-machine-architecture
This option specifies whether verification runs in 32 or 64-bit mode.
1-53
1 Option Descriptions
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:
1-54
polyspace-c -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 processing, set: -max-processes 1.
Default:
4
Example Shell Script Entry:
polyspace-c -max-processes 1
Others
PolySpace®Inner Settings Options
• “-extra-flags o
• “-c-extra-fla
• “-il-extra-f
ption-extra-flag” on page 1-55
gs flag” on page 1-55
lags flag” on page 1-56
-extra-flags option-extra-flag
This option s
of the option
These flags
verificati
Default:
No extra fl
Example S
polyspa
-extra-
pecifies an expert option to be added to the analyzer. Each word
(even the parameters) must be preceded by -extra-flags.
will be given to you by Technical Support as necessary for your
ons.
ags.
hell Script Entry:
ce-c -extra-flags -param1 -extra-flags -param2 \
flags 10 ...
-c-extra-flags flag
This op
Each w
-c-ex
tion is used to specify an expert option to be added to a verification.
ord of the option (even the parameters) must be preceded by
tra-flags.
eflagswillbegiventoyoubyPolySpaceasnecessaryforyour
Thes
fications.
veri
ult:
Defa
xtra flags.
No e
mple Shell Script Entry:
Exa
1-55
1 Option Descriptions
polyspace-c -c-extra-flags -param1 -c-extra-flags -param2
-c-extra-flags 10
-il-extra-flags flag
This option is used to specify an expert option to be added to a verification.
Each word of the option (even the parameters) must be preceded by
-il-extra-flags.
TheseflagswillbegiventoyoubyPolySpaceasnecessaryforyour
verifications.
Default:
No extra flags.
Example Shell Script Entry:
polyspace-c -il-extra-flags -param1 -il-extra-flags -param2
-il-extra-flags 10
1-56
Precision/Scaling Options
In this section...
“-quick (Deprecated)” on page 1-58
“-O(0-3)” on page 1-58
“-modules-precision mod1:O(0-3)[,mod2:O(0-3)[,...]]” on page 1-59
“-from verification-phase” on page 1-60
“-to verification-phase” on page 1-61
“-context-sensitivity "proc1[,proc2[,...]]"” on page 1-62
“-context-sensitivity-auto” on page 1-62
“-path-sensitivity-delta number” on page 1-62
“-retype-pointer” on page 1-63
“-retype-int-pointer” on page 1-64
“-k-limiting number” on page 1-66
Precision/Scaling Options
“-no-fold” on page 1-66
“-respect-types-in-globals” on page 1-66
“-respect-types-in-fields” on page 1-67
“-inline "proc1[,proc2[,...]]"” on page 1-68
“-lightweight-thread-model” on page 1-69
“-less-range-information” on page 1-69
“-no-pointer-information” on page 1-70
1-57
1 Option Descriptions
-quick (Depreca
Note This option
quick mode is o
PASS0 takes so
The limitatio
no variable di
provides ful
This option
mewhat longer to run, but the results are more complete.
ns of
ctionary) no longer apply. Unlike
l navigation in the Viewer.
is used to select a very fast mode for PolySpace .
ted)
is deprecated in R2009a and later releases.
bsolete and has been replaced with ve rificatio n PASS0.
quick mode,(noNTLorNTCchecks,nofloatchecks,
quick mode, PASS0 also
Benefits
This optio
for initia
plentiful
n allows results to be generated very quickly. These are suitable
l verification of red and gray errors only, as orange checks are too
to be relevant using this option.
Limitations
• No NTL or NTC are displayed (non termination of loop/call)
• The variable dictionary is not available
1-58
• 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.
Precision/Scaling Options
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 domai n
values (a mixed approach with integer lattices and complex polyhedrons).
- -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-c -O1 -to pass4 ...
-modules-precision mod1:O(0-3)[,mod2:O(0-3)[,...]]
This option is used to specify the list of .c fi les to be analyzed with a different
precision from that specified generally -O(0-3) for this verification.
In batch mode, each specified module is followed by a colon and the desired
precision level for it. Any number of modules can be specified in this way, to
form a comma-separated list with no spaces.
Default:
All modules are treated with the same precision.
Example Shell Script Entry:
1-59
1 Option Descriptions
polyspace-c -O1 \
-modules-precision myMath:O2,myText:O1, ...
-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.
For example, if a verification has been completed -to pass1, PolySpace
verification 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.
1-60
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.
Default :
scratch
Example Shell Script Entry :
polyspace-c -from c-to-il ...
Precision/Scaling Options
-to verification-phase
This option specifies the 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 higher verification time
Note The MathWorks recommends you begin by running -to pass0
(Software Safety Analysis level 0
gray code before relaunching verification using higher integration levels.
Possible values:
) You can then address red errors and
•
c-compile or "C Source Compliance Checking"
c-to-il or "C 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"
•
pass4 or "Software Safety Analysis level 4"
•
other
•
Note If you use -to other then PolySpace verification will continue until you
stop it manually (via
kill-rte-kernel) or stops until it has reached pass20.
Default:
1-61
1 Option Descriptions
pass4
Example Shell Script Entry:
polyspace-c -to "Software Safety Analysis level 3"...
polyspace-c -to pass0 ...
-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 especially useful if a problem function is called from a multitude
of places.
1-62
-context-sensitivity-auto
This option is similar to the -context-sensitivity option, except that the system
automatically chooses the procedures to be considered.
-path-sensitivity-delta number
This option is used to improve interprocedural verification precision within
aparticularpass(see-topass1, pass2, pass3 or pass4). The propagation of
information within procedures is done earlier than usual when this option is
specified. That results i n improved selectivity and a longer ve rification time.
Consider two verifications, one with this option set to 1 (with), and one
without this option (without)
• a level 1 verification in (with) (pass1) will provide results equivalent to
level 1 or 2 in the (without) verification
• a level 1 verification in (with) can last x times more than a cumulated level
1+2 verification from (without). "x" might be exponential.
Precision/Scaling Options
• the same applies to level 2 in (with) equivalent to level 3 or 4 in (without),
with potentially exponential verification time for (a)
Gains using the o ption
• (+) highest selectivity obtained in level 2. no need to wait until level 4
• (-) This parameter increases exponentially the verification time and might
be even bigger than a cumulated verification in level 1+2+3+4
• (-) This option can only be used with less than 1000 lines of code
Default:
0
Example Shell Script Entry:
polyspace-c -path-sensitivity-delta 1 ...
-retype-pointer
This option can be used to retype variables o f pointer types in order to im pro ve
precision of pointer conversions chain.
The principle consists i n replacing original type by the aliased object type
when a symbol of pointer type aliases to a single type of objects.
For example, following assert can be proved using -retype-pointer option:
struct A {int a; char b;} s = {1,2};
char *tmp = (char *)&s;
struct A *pa = (struct A*)tmp;
assert((pa->a == 1) && (pa->b == 2));
This principle can be applied to fields of struct/unions of a pointer type.
However, this option set -size-in-bytes option and it does not have expected
precision with -allow-ptr-arith-on-struct.
Moreover, this option is forbidden when using -retype-int-pointer option.
1-63
1 Option Descriptions
Default:
disable by default
Example Shell ScriptEntry:
polyspace-c -retype-pointer ...
-retype-int-pointer
Thisoptioncanbeusedtoretypevariablesofpointertosignedor
unsigned integer types in order to improve precision of pointer conversions
chain.
The principle consists i n replacing original type by the aliased object type
when a symbol of pointer type aliases to a single type of objects. It applies
only on symbols of signed or unsigned integer types.
For example, following assert can be proved using -retype-int-pointer option:
1-64
void function(void)
{
struct S1 {
int x;
int y;
int z;
char t;
} s1 = {1,2,3,4};
struct S2 {
int first;
void *p;
} s2;
int addr;
addr = (int)(&s1);
assert(((struct S1 *)addr)->y == 2); // ASRT is verified
s2.first = (int)(&s1);
assert(((struct S1 *)s2.first)->y == 2); // ASRT is verified
}
Precision/Scaling Options
However, this option set -size-in-bytes and has no effect when set
-respect-types-in-globals on global symbols of integer types and when set
-respect-types-in-fields on fields of struct/union of integer types.
Some sides effects can be noticed on Po ly Space checks concerning initialization
on variables which can be stated as initialization on pointer check (NIP).
This option requires the -retype-pointer option.
This option should be used on:
• Code with memory mapping – When constant bg structures (global
variable) are declared with a pointer and points to const structure, setting
the option will consider that the pointer and the pointer structure are
synonyms (aliased) and precision of the result will increase. Option to
set:
-retype-pointer.
• Code close to the communication layer API (code with lot of cast in
(void *)) – When code contains low level drivers, generic pointer (void *) can
be used. It is recommended to use this with an
containing these casts. Options to set:
-retype-pointer -inline.
-inline of the functions
• Code in which MISRA rule 11.2 is violated – When integers contains
pointers, precision can b e improved w hen setting an option. Option to set:
-retype-int-pointer.
Theseoptionsarenotsetbydefaultbecausetheyallchangetheoption
-size-in-bytes. Therefore, precision can reduced and some red IDP checks
may be affected. In addition, using these options will consider "x" (previously
int) as a pointer. This results in checks changing category (NIV to NIP).
Default:
Disable by default
Example Shell ScriptEntry:
polyspace-c -retype-int-pointer...
1-65
1 Option Descriptions
-k-limiting num
This is a scaling
structures duri
This option is o
Default:
Thereisnofi
Example Shel
polyspace-
In this exa
ng pointer verification.
nly available for C and C++.
xed limit.
lScriptEntry:
c -k-limiting 1 ...
mple above, verification will be precise to only one level of nesting.
ber
option to limits the depth of verification into nested
-no-fold
When vari
may occur
initial
string)
It can sp
applic
ables are defined with huge static initialization, scaling problems
during the compilation phase. This option approximates the
ization of array types of integer, floating point, and char types (included
if needed.
eed up the verification, but may decrease precision for some
ations
1-66
Defaul
Examp
-re
Thi
app
co
t:
nnotset.
Optio
le Shell Script Entry:
space-c -no-fold ...
poly
spect-types-in-globals
s is a scaling option, designed to help process complex code. When it is
lied, PolySpace verification assumes that global variables not declared as
ntaining pointers are never used for holding pointer values. This option
Precision/Scaling Options
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 following example, we will lose p r ecision using option
–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 verification will not take care that x contains the address of y
resulting a green as sert.
Default:
PolySpace verification assumes that gl ob al variables may contain pointer
values.
Example Shell Script Entry:
polyspace-c -respect-types-in-globals ...
-respect-types-in-fields
This is a scaling option, designed to help process complex code. When it is
applied, PolySpace verification assumes that structure fields 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-globals.
In the following example, we will lose p r ecision using option
–respect-types-in-fields option:
struct {
unsigned x;
1-67
1 Option Descriptions
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);
}
PolySpace verification will not take care that S1.x contains the address of y
resulting a green as sert.
Default:
1-68
PolySpace verification assumes that structure fields may contain pointer
values.
Example Shell Script Entry:
polyspace-c -respect-types-in-fields ...
-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 viz:
procedure1_pst_cloned_nb,
where nb is a unique number giving the total number of cloned procedures.
Such an inlining allows the number of aliases in a given procedure to be
reduced, and may also improve precision.
Precision/Scaling Options
Restrictions :
• Extensive use of this option may duplicate too much code and may lead to
other scaling problems. Carefully choose procedures to inline.
• This option should be used in response to the inlining hints provided by
the alias verification
• This option should not be used on main, task entry points and critical
section entry points
-lightweight-thread-model
This scaling option can be used to reduce task complexity (see also
-entry-points ).
It uses a slightly less precise model of pointer/thread interaction compared
to that used by default, and is likely to prove helpful when there are a lot of
pointers in an application. See Chapter 3, “Approximations Used During
Verification” for more explanation of when to use it.
It causes a loss of precision:
• It causes a slight loss of precision when shared variables are reads via
pointers.
• Some read/write accesses may not appear in the Global Variable Dictionary.
Default:
disabled by default.
Example Shell Script Entry :
polyspace-c -lightweight-thread-model ...
polyspace-c -lwtm ...
-less-range-information
Limits the amount of range information displayed in verification results.
1-69
1 Option Descriptions
When you select this option, the software pro vide s range information on
assignments, but not on reads and operators.
In addition, selecting this option enables the
option. See “-no-pointer-information” o n page 1-70.
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
select this opti on , the software displays range information only when you
place the cursor over
Default:
Disabled.
Example Shell Script Entry :
polyspace-c -less-range-information
x.
no-pointer-information
x, y, z,or+. However, if you
-no-pointer-information
Stops the display of pointer information in verification results.
1-70
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;
Precision/Scaling Options
If you do not select this option (the default), the software displays pointer
information when you place the cursor on
p or *. If you select this option, the
software does not display pointer information.
Default:
Disabled.
Example Shell Script Entry :
polyspace-c -no-pointer-information
1-71
1 Option Descriptions
Multitasking Options (PolySpace Server for C/C++ Product
Only)
In this section...
“-entry-points str1[,str2[,...]]” on page 1-72
“-critical-section-[begin or end] "proc1:cs1[,proc2:cs2]"” on page 1-72
“-temporal-exclusions-file file_name” on page 1-73
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 server, using a Comma-separated list with no spaces.
1-72
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.
Using PolySpace verification, c tasks must have the prototype "void
task_name(void);".
Example Shell Script Entry:
polyspace-c -entry-points proc1,proc2,proc3 ...
-critical-section-[begin or end] "proc1:cs1[,proc2:cs2]"
-critical-section-begin "proc1:cs1[,proc2:cs2]"
and
-critical-section-end "proc3:cs1[,proc4:cs2]"
These options specify the procedures beginning and ending critical sections,
respectively. Each uses a list enclosed within double speech marks, with
Multitasking Options (PolySpace®Server™ for C/C++ Product Only)
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.
Note This option cannot be used for client verifications, or with the
main-generator option.
Default:
no critical sections.
Example Shell Script Entry:
polyspace-c -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.
Note This option cannot be used for client verifications, or with the
main-generator option.
Default:
1-73
1 Option Descriptions
No temporal exclusions.
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-c -temporal-exclusions-file sources/exclusions \
-entry-points task1_group1,task2_group1,task1_group2,\
task2_group2,task3_group2 ...
1-74
Batch Options
In this section...
“-server server_name_or_ip[:port_number]” on page 1-75
“-sources-list-file file_name” on page 1-75
“-v | -version” on page 1-76
“-h[elp]” on page 1-76
-server server_name_or_ip[:port_number]
Using polyspace-remote-[c] [–server [name or IP address][:<port number>]]
allows you to send a verification to a specific or referenced PolySpace server.
Note If the option –server is not specified, the default server referenced in
the PolySpace-Launcher.prf configuration file will be used as the server.
Batch Options
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 also that polyspace-remote- accepts all other options.
Option Example Shell Script Entry:
polyspace-remote-c server 192.168.1.124:12400
polyspace-remote-c
polyspace-remote-c server Bergeron
-sources-list-file file_name
This option is only available in batch mode. The syntax of file_name is the
following:
1-75
1 Option Descriptions
• Onefileperline.
• Each file name includes its absolute or relative path.
The source files are compiled in the order in which they are specified.
Note If y ou do not specify any files, the software verifies all files in the
source directory in alphabetical order.
Example Shell Script Entry for -sources-list-file:
polyspace-c -sources-list-file "C:\Analysis\files.txt"
polyspace-c -sources-list-file "files.txt"
-v | -version
Display the PolySpace version number.
1-76
Example Shell Script Entry:
polyspace-c v
It will show a result similar to:
PolySpace r2007a+
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-c h
Check Descriptions
2
2 Check Descriptions
Colored Source Code for C
In this section...
“Illegal Pointer Access to Variable or Structure Field: IDP” on page 2-3
“Array Conve rsio n Must Not Extend Range: COR” on page 2-4
“Array Index Within Bounds: OBAI” on page 2-5
“Initialized Return Value: IRV” on page 2-6
“Non-Initialized Variables: NIV/NIVL” on page 2-7
“Non-Initialized Pointer: NIP” on page 2-8
“POW (Deprecated)” on page 2-8
“User Assertion: ASRT” on page 2-8
“Scalar and Float Overflows: OVFL” on page 2-10
“Scalar and Float Underflows: UNFL (Deprecated)” on page 2-14
“Float Underflows and Overflows: UOVFL (Deprecated)” on page 2-14
2-2
“ScalarorFloatDivisionbyZero:ZDV”onpage2-14
“Shift Amount in 0..31 (0..63):SHF” o n page 2-15
“Left O perand of Left Shift is Negative: SHF” on page 2-16
“Function Pointer Must Point to a Valid Function: COR” on page 2 -16
“Wrong Type for Argument: COR” on page 2-18
“Wrong Number of Arguments: C OR ” on page 2-18
“Wrong Return Type of a Function Pointer: C OR ” on page 2-19
“Wrong Return Type for Arithmetic Functions: COR” on page 2-20
“Pointer Within Bounds: IDP” on page 2-21
“Non Termination of Call or Loop” on page 2-34
“Unreachable Code: UNR” on page 2-44
“Inspection Points” on page 2-46
Colored Source Code for C
Illegal Pointer
Access to Variable or Structure Field:
IDP
This is a check to
the form ptr+i,
the one access
Consider the f
1 int a;
2
3 struct {
4 int f1;
5 int f2;
6 int f3;
7}S;
8
9 void main(void)
10 {
11 volatile int x;
12
13 if (x)
14 *(&a+1) = 2;
15 // IDP ERROR: &a +1 doesn't point to a any longer
16 if (x)
17 *(&S.f1 +1) = 2;
18 // IDP ERROR: you are not allowed to access f2 like this
19 }
establish whether in the dereferencing of an expression of
the variable/structure fiel d initially pointed to by ptr is still
ed. See ANSI C standard ISO/IEC 9899 section 6.3.6.
ollowing example.
According to the ANSI C standard, it is not permissible to access a variab le
(or a structure field) from a pointer to another variable. That is, ptr+i may
only be dereferenced if ptr+i is the address of a subpart of the object pointed
to by ptr (such as an element of the array pointed to by ptr,orafieldofthe
structure pointed to by ptr).
For instance, the following code is correct because the length of the entity
pointed to by ptr_s reflects the full structure length of My_struct (at line 11):
1 typedef struct {
2 int f1;
3 int f2;
2-3
2 Check Descriptions
4 int f3;
5 } My_Struct;
6
7 My_Struct s = {1,2,3};
8
9intmain(void)
10 {
11 My_Struct *ptr_s = &s;
12
13 // change to f2 field
14 *((int *)&s +1) = 2; // Correct evaluation
15
16 return 0;
17 }
Array Conversion Must Not Extend Range: COR
This is a check to establish whether a small array is mapped onto a bigger one
through a pointer cast. Consider the following example.
2-4
1
2 typedef int Big[100];
3 typedef int Small[10];
4 typedef short EquivBig[200];
5
6 Small smalltab;
7Bigbigtab;
8
9 void main(void)
10 {
11 volatile int random;
12
13 Big * ptr_big = &bigtab;
14 Small * ptr_small = &smalltab;
15
16 if (random){
17 Big *new_ptr_big = (Big*)ptr_small; // COR ERROR: array
conversion must not extend range
18 }
19 if (random){
20 EquivBig *ptr_equivbig = (EquivBig*)ptr_big;
Colored Source Code for C
21 Small *ptr_new_small = (Small*)ptr_big; // Conversion
verified
22 }
23 }
In the example above, a pointer is initialized to the Big array w ith the address
of the Small array. This is not legal since it would be possible to dereference
this pointer outside the Small array. Line 20 shows that the mapping of
arrays with same size and different prototypes is acceptable.
Array Index Within Bounds: OBAI
This is a check to establish whether an index accessing an array is compatible
with the length of that array.
The message associated with an OBA I check provides the range of the array.
For example: Array index out of bounds [ 0..1023].
Consider the following example.
1
2 #define TAILLE_TAB 1024
3 int tab[TAILLE_TAB];
4
5 void main(void)
6{
7 int index;
8
9 for (index = 0; index < TAILLE_TAB ; index++)
10 {
11 tab[index]=0;
12 }
13 tab[index]=1;
14 // OBAI ERROR: Array index out of bounds [0..1023]
15 }
Just after the loop, index equals SIZE_TAB. Thus tab[in dex] = 1 overwrites
the memory cell just after the last array element.
2-5
2 Check Descriptions
An OBAI check can also be localized on a + operator, as another example
illustrates.
1 int tab[10];
2
3 void main(void)
4{
5 int index;
6 for (index =0;index <10;index++)
7 *(tab + index)=0;
8
9 *(tab + index) = 1; // OBAI ERROR: Array index out of bounds
10 }
Initialized Return Value: IRV
This is a check to establish whether a function returns an initialized value.
Consider the following example.
1
2 extern int random_int(void);
3
4intreply(int msg)
5{
6 int rep = 0;
7if(msg > 0) return rep;
8}
9
10 void main(void)
11 {
12 int ans;
13
14 if (random_int())
15 ans = reply(1); // IRV verified: function returns an
initialised value
16 else if (random_int())
17 ans = reply(0); // IRV ERROR: function does not return an
initialised value
18 else
19 reply(0); // No IRV checks because the return value
is not used
2-6
Colored Source Code for C
20
21 }
22
23
Variables are often initialized using the return value of functions. However,
in the above example the return value is not initialized for all input parameter
values. In this case, the target variable will not be always be properly
initialized with a valid return value.
Non-Initialized Variables: NIV/NIVL
This is a check to establish whether a variable is initialized before being
read. Consider the following example.
1
2 extern int random_int(void);
3
4 void main(void)
5{
6 int x,i;
7 double twentyFloat[20];
8 int y = 0;
9
10 if (random_int()) {
11 y += x; // NIV ERROR: Non
Initialized Variable (type: int 32)
12 }
13 if (random_int()) {
14 for (i =1;i < 20; i++){
15 if (i%2) twentyFloat[i] = 0.0;
16 }
17 twentyFloat[2]=twentyFloat[4] + 5.0; // NIV Warning.
Only odd indexes are initialized.
18 }
19 }
The result of the addition is unknown at line 11 because x is not initialized
(UNR unreachable code on "+" operator).
2-7
2 Check Descriptions
In addition, line 17 shows how PolySpace software prompts the user to
investigate further (by means of an orange check) when all cells have not
been initialized.
Note Associated to each message which concerns a NIV check, PolySpace
software gives the type of the variable like the following examples: (type:
volatile int32), (type: int 16), (type: unsigned int 8), etc.
Non-Initialized Pointer: NIP
Check to establish whether a reference is initialized before being dereferenced.
Consider the following example.
2
3 void main(void)
4{
5 int* p;
6 *p = 0; // NIP ERROR: reference is not initialized
7}
2-8
As p is not initialized, an undefined memory cell would be overwritten at line
6(*p = 0) (also leading to the unreachable gray check on "*").
POW (Deprecated)
Note The POW check is deprecated in R2009a and later. The POW check no
longer appears in PolySpace results.
Check to establish whether the standard pow function from math.h library is
used with an acceptable (positive) argument.
User Assertion: ASRT
This is a check to establish whether a user assertion is valid. If the assumption
implied by an assertion is invalid, then the standard behavior of the assert
macro is to abort the program. PolySpace verification therefo re considers a
failed assertion to be a runtime error. Consider the following example.
Colored Source Code for C
1 #include <assert.h>
2
3 typedef enum
4{
5 monday=1, tuesday,
6 wensday, thursday,
7 friday, saturday,
8 sunday
9 } dayofweek ;
10
11 // stubbed function
12 dayofweek random_day(void);
13 int random_value(void);
14
15 void main(void)
16 {
17 unsigned int var_flip;
18 unsigned int flip_flop;
19 dayofweek curDay;
20 unsigned int constant = 1;
21
22 if (random_value()) flip_flop=1; else flip_flop=0;
// flip_flop can randomly be 1 or 0
23 var_flip =(constant | random_value());
// var_flip is always > 0
24
25 if(random_value()) {
26 assert(flip_flop==0 || flip_flop==1); // User Assertion is
verified
27 assert(var_flip>0); // User Assertion is
verified
28 assert(var_flip==0); // ASRT ERROR: Failure User
Assert
29 }
30
31 if (random_value()) {
32 curDay = random_day(); // Random day of the week
33 assert( curDay > thursday); // ASRT Warning: User
assertion may fails
34 assert( curDay > thursday); // User assertion is
2-9
2 Check Descriptions
verified
35 assert( curDay <= thursday); // ASRT ERROR: Failure User
Assertion
36 }
37 }
In the main,theassert function is used in two different manners:
1 To establish whether the values flip_flop and var_flip in the program are
inside the domain which the program is designed to handle. If the values
were outside the range implied by the assert (see line 28), then the program
would not be able to run properly. Thus they are flagged as runtime errors.
2 To redefine the range of variables as shown at line 34 where curDay is
restricted to just a few days. Indeed, PolySpace verification makes the
assumption that if the program is executed withou t a runtime error at line
33, curDay can only have a value greater than thursday after this line.
Scalar and Float Overflows: OVFL
These are checks to establish whether arithmetic expressions overflow or
underflow. This is a scalar check with integer type and float check for floating
point expression. Consider the following example.
2-10
1 #include <float.h>
2 extern int random_int(void);
3
4 void main(void)
5{
6 int i = 1;
7 float fvalue = FLT_MAX;
8
9 i = i<<30; // i = 2**30
10 if (random_int())
11 i = 2 * (i-1) + 2; // OVFL ERROR: 2**31 is an overflow
value for int32
12 if (random_int())
13 fvalue = 2 * fvalue + 1.0; // OVFL ERROR: float variable is
overflow
14 }
Colored Source Code for C
On a 32 bit architecture platform, the maximum integer value is 2**31-1,thus
2**31will raise an overflow.
Inthesamemanner,iffval uerepresents the biggest float its double cannot be
represented with same type and raises an overflow.
How Much is the Biggest Float in C?
There are occasions when it is important to understand when overflow may
occur on a float value approaching its maximum value. Conside r the following
example.
void main(void)
{
float x, y;
x = 3.40282347e+38f; // is green
y=(float) 3.40282347e+38; // OVFL red
}
There is a red error on the second assignment, but not the first. The real
"biggest"valueforafloatis:
- MAXFLOAT -.
340282346638528859811704183484516925440.0
Now, rounding is not the same when casting a constant to a float, or a
constant to a double:
• floats are rounded to the n earest lower value;
• doubles are rounded to the nearest higher value;
• 3.40282347e+38 is strictly bigger than
340282346638528859811704183484516925440 (named MAXFLOAT).
• In the case of the second assignment, the value is cast to a double first
-byyourcompiler,usingatemporaryvariableD1-,thenintoafloatanother temporary variable -, because of the cast. Float value is greater
than
MAXFLOAT,sothecheckisred.
• In the case of the first assignment, 3.40282347e+38f is directly cast into a
float, which is less than
MAXFLOAT
The solution to this problem is to use the "f" suffix to specify the variable
directly as a float, rather than casting.
2-11
2 Check Descriptions
What is the Type of Constants/What is a Constant Overflow?
Consider the following example, which would cause an overflow.
int x = 0xFFFF; /* OVFL */
The type given to a constant is the first type which can accommodate its
value, from the appropriate sequence shown below. (See “Predefined T arge t
Processor Specifications” in the PolySpace P roducts for C User’s Guide for
information about the size of a type depending on the target.)
Decimals int , long , unsigned long
Hexadecimals Int, unsigned int, long, unsigned
long
Floats double
For examples (assuming 16-bits target):
5.8
6
65536
0x6
0xFFFF
5.8F
65536U
The options -ignore-constant-overflows allow the user to bypass this limitation
and consider the line:
int x = 0xFFFF; /* OVFL */ as int x = -1; instead of 65535, which does not fit
into a 16-bit integer (from -32768 to 32767).
double
int
long
int
unsigned int
float
unsigned int
Left shift overflow on signed variables: OVFL
Overflows can be also be encountered in the case of left shifts on signed
variables. In the following example, the higher order bit of 0x41021011
2-12
Colored Source Code for C
(hexadecimal value of 1090654225) has been lost, highlighting an overflow
(integer promotion).
1
2 void main(void)
3{
4 int i;
5
6 i = 1090654225 << 1; // OVFL ERROR: on left shift range
7}
Float Underflow Versus Values Near Zero: OVFL
The definition of the word "underflow" differs between the ANSI standard
and the ANSI/IEEE 754-1985 standard. According to the former definition,
underflow occurs when a number is sufficiently negative for its type not to
be capable of representing it. Accordin g to the latter, underflow describes
theerroneousrepresentationofavalueclosetozeroduetothelimitsofits
representation.
PolySpace verifications apply the former definition. The latter definition
does not impose the raising of an exception as a result of an underflow. B y
default, proces sors supporting this standard permit the deactivation of such
exceptions.
Consider the following example.
2 #define FLT_MAX 3.40282347e+38F // maximum representable
float found in <float.h>
3 #define FLT_MIN 1.17549435e-38F // minimum normalised
float found in <float.h>
4
5 void main(void)
6{
7 float zer_float = FLT_MIN;
8 float min_float = -(FLT_MAX);
9
10 zer_float = zer_float * zer_float; // No check overflow
near zero
11 min_float = min_float * min_float; // OVFL ERROR:
underflow checked by verifier
2-13
2 Check Descriptions
12
13 }
Scalar and Float Under flows: UNFL (Deprecated)
Note The UNFL check is deprecated in R2010a and later. The UNFL check
no longer appears in PolySpace results. Instead of two separate UNFL and
OVFL checks, a single OVFL check now appears.
These are checks to establish whether arithmetic expressions underflow. A
scalar check is used with integer type, and a float check for floating point
expressions. Consider the following example.
Float Underflows and Overflows: UOVFL
(Deprecated)
Note The UOVF L check is d eprecated in R2009a and later. The UOVFL
check no longer appears in PolySpace results. Instead of a single UOVFL
check, the results now display two checks, a UNFL and an OVFL.
2-14
The check UOVFL only concerns float variables. PolySpace verification
shows an UOVFL when both overflow and underflow can occur on the same
operation.
Scalar or Flo at Divis ion by Zero: ZDV
This is a check to establish whether the right operand of a division (that is,
the denominator) is different from 0[.0]. Consider the following example.
1 extern int random_value(void);
2
3 void zdvs(int p)
4{
5 int i, j = 1;
6 i = 1024 / (j-p); // ZDV ERROR: Scalar Division by Zero
7}
8
Colored Source Code for C
9 void zdvf(float p)
10 {
11 float i,j = 1.0;
12 i = 1024.0 / (j-p); // ZDV ERROR: float Division by Zero
13 }
14
15 int main(void)
16 {
17 volatile int random;
18 if (random_value()) zdvs(1);
// NTC ERROR: because of ZDV ERROR
in ZDVS.
19 if (random_value()) zdvf(1.0);
// NTC ERROR: because of ZDV ERROR
in ZDVF.
20 }
Shift Am ount in 0..31 (0..63):SHF
This is a check to establish whether a shift (left or right) is bigger than the
sizeoftheintegraltypeoperatedupon(intorlongint). Therangeofallowed
shift depends on the target processor: 16 bits on c-167,32bitsoni386 for int,
etc. Consider the following example.
1 extern int random_value(void);
2
3 void main(void)
4{
5 volatile int x;
6 int k, l = 1024; // 32 bits on i386
7 unsigned int v, u = 1024;
8
9if(x)k=l<<16;
10 if (x)k=l>>16;
11
12 if (x)k=l << 32; // SHF ERROR
13 if (x)k=l >> 32; // SHF ERROR
14
15 if (x)v=u >> 32; // SHF ERROR
16 if (x)k=u << 32; // SHF ERROR
17
2-15
2 Check Descriptions
18 }
In this example, it is shown that the shift amount is greater than the integer
size.
Left Operand of Left Shift is Negative: SHF
This is a check to establish whether the operand of a left shift is a signed
number. Consider the following example.
1
2
3 void main(void)
4{
5 int x = -200;
6 int y;
7
8y=x << 1; // SHF ERROR: left operand must be positive
9
10 }
2-16
As an aside, note that the -allow-negative-operand-in-shift option used at
launching time instructs PolySpace software to permit explicitly signed
numbers on shift operations. Using the option in the example above would
see the red check at line 8 transformed in a green one. Similarly, if the
verification had included the expression -2 << 2 at line 9, then that line
would have been given a green check and y would assume a values of -8.
Function Pointer Must Point to a Valid Function: COR
This is a check to establish whether a function pointer points to a valid
function, or to function with a valid prototype. Consider the following example.
1
2 typedef void (*CallBack)(float *data);
3
4 struct {
5 int ID;
6 char name[20];
7 CallBack func;
8}funcS;
Colored Source Code for C
9
10 float fval;
11
12 void main(void)
13 {
14 CallBack cb = (CallBack)((char*)&funcS + 24*sizeof(char));
15
16 cb(&fval); // COR ERROR: function pointer must point
to a valid function
17 }
In the example above, func has a prototype in conformance with CallBack’s
declaration. Therefore func is initialized to point to the NULL function
through the global declaration of funcS.
Consider a second example.
1
2 #define MAX_MEMSEG 32764
3 typedef void (*ptrFunc)(int memseg);
4 ptrFunc initFlash = (ptrFunc)(0x003c);
5
6 void main(void)
7{
8 int i;
9
10 for (i = 0 ; i < MAX_MEMSEG; i++) // NTL propagation
11 {
12 initFlash(i); // COR ERROR: function pointer must point to a
valid function
13 }
14
15 }
As PolySpace verification does not take the memory mapping of programs into
account, it cannot ascertain whether 0x003 is the address of a function code
segment or not (for instance, as far as PolySpace verification is concerned it
could b e a data segment). Thus a certain (red) error is raised.
2-17
2 Check Descriptions
Wrong T ype for Argument: COR
This is a check to establish whether each argument passed to a function
matches the prototype of that function. Consider the flowing example.
1
2 typedef struct {
3 float r;
4 float i;
5 } complex;
6
7 typedef int (*t_func)(complex*);
8
9intfoo_type(int *x)
10 {
11 if (*x%2 == 0) return 0;
12 else return 1;
13 }
14
15 void main(void)
16 {
17 t_func ptr_func;
18 int j,i = 0;
19
20 ptr_func = foo_type;
21 j = ptr_func(&i); // COR ERROR: wrong type of argument for #1
22 }
23
2-18
In this example, ptr_func is a pointer to a function which expects a pointer
to a complex as input argument. However, the parameter used is a pointer
to an int.
Wrong Number of Arguments: COR
This is a check to establish whether the number of arguments passed to a
function matches the number of arguments in its prototype. Consider the
following example.
1
2 typedef int (*t_func_2)(int);
Loading...