Specify Target Environment and Compiler Behavior
Before verification, specify your source code language (C or C++), target processor, and the compiler that you use for building your code. In certain cases, to emulate your compiler behavior, you might have to specify additional options.
Using your specification, the verification determines the sizes of fundamental types, considers certain macros as defined, and interprets compiler-specific extensions of the Standard. If the options do not correspond to your run-time environment, you can encounter:
Compilation errors
Verification results that might not apply to your target
If you use a build command such as gmake
to build your code and the
build command meets certain restrictions, you can extract the options from the build
command after executing the command. Otherwise, specify the options explicitly.
Extract Options from Build Command
If you use build automation scripts to build your source code, you can set up a Polyspace® project from your scripts. The options associated with your compiler are specified in that project.
In the Polyspace desktop products, for information on how to trace your build command from the:
Polyspace user interface, see Add Source Files for Analysis in Polyspace User Interface.
DOS or UNIX® command line, see
polyspace-configure
.MATLAB® command line, see
polyspaceConfigure
.
In the Polyspace server products, for information on how to trace your build command, see Create Polyspace Analysis Configuration from Build Command (Makefile).
For Polyspace project creation, your build automation script (makefile) must meet certain requirements. See Requirements for Project Creation from Build Systems.
Specify Options Explicitly
If you cannot trace your build command and therefore manually create a project, you have to specify the options explicitly.
In the user interface of the Polyspace desktop products, select a project configuration. On the Configuration pane, select Target & Compiler. Specify the options.
At the DOS or UNIX command line, specify flags with the
polyspace-bug-finder
,polyspace-code-prover
,polyspace-bug-finder-server
orpolyspace-code-prover-server
command.At the MATLAB command line, specify arguments with the
polyspaceBugFinder
,polyspaceCodeProver
,polyspaceBugFinderServer
orpolyspaceCodeProverServer
function.
Specify the options in this order.
Required options:
Source code language (-lang)
: If all files have the same extension.c
or.cpp
, the verification uses the extension to determine the source code language. Otherwise, explicitly specify the option.Compiler (-compiler)
: Select the compiler that you use for building your source code. If you cannot find your compiler, use an option that closely matches your compiler.Target processor type (-target)
: Specify the target processor on which you intend to execute your code. For some processors, you can change the default specifications. For instance, for the processorhc08
, you can change the size of typesdouble
andlong double
from 32 to 64 bits.If you cannot find your target processor, you can create your own target and specify the sizes of fundamental types, default signedness of
char
, and endianness of the target machine. SeeGeneric target options
.
Language-specific options:
C standard version (-c-version)
: The default C language standard depends on your compiler specification. If you do not specify a compiler explicitly, the default analysis uses the C99 standard. Specify an earlier standard such as C90 or a later standard such as C11.C++ standard version (-cpp-version)
: The default C++ language standard depends on your compiler specification. If you do not specify a compiler explicitly, the default analysis uses the C++03 standard. Specify later standards such as C++11 or C++14.
Compiler-specific options:
Whether these options are available or not depends on your specification for
Compiler (-compiler)
. For instance, if you select avisual
compiler, the optionPack alignment value (-pack-alignment-value)
is available. Using the option, you emulate the compiler option/Zp
that you use in Visual Studio®.For all compiler-specific options, see Target and Compiler.
Advanced options:
Using these options, you can modify the verification results. For instance, if you use the option
Division round down (-div-round-down)
, the verification considers that quotients from division or modulus of negative numbers are rounded down. Use these options only if you use similar options when compiling your code.For all advanced options, see Target and Compiler.
Compiler header files:
If you specify the
diab
,tasking
orgreenhills
compiler, you must specify the path to your compiler header files. See Provide Standard Library Headers for Polyspace Analysis.
If you still see compilation errors after running analysis, you might have to specify other options:
Define macros: Sometimes, a compilation error occurs because the analysis considers a macro as undefined. Explicitly define these macros. See
Preprocessor definitions (-D)
.Specify include files: Sometimes, a compilation error occurs because your compiler defines standard library functions differently from Polyspace and you do not provide your compiler include files. Explicitly specify the path to your compiler include files. See Provide Standard Library Headers for Polyspace Analysis.
See Also
Source code
language (-lang)
| Compiler
(-compiler)
| Target
processor type (-target)
| C standard version (-c-version)
| C++ standard version (-cpp-version)
| Preprocessor
definitions (-D)