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. 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 (Polyspace Code Prover Server).

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 (Polyspace Bug Finder Server) or polyspace-code-prover-server (Polyspace Code Prover Server) command.

• At the MATLAB command line, specify arguments with the polyspaceBugFinder, polyspaceCodeProver, polyspaceBugFinderServer or polyspaceCodeProverServer 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 processor hc08, you can change the size of types double and long 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. See Generic 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 a visual compiler, the option Pack 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 or greenhills 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.