Main Content

-dump-preprocessing-info

Show all macros implicitly defined during a particular analysis

Syntax

-dump-preprocessing-info

Description

-dump-preprocessing-info prints all the macros implicitly defined (or undefined) during a particular Polyspace® analysis. The macro definitions come from:

Use this option only if you want to know how Polyspace defines a specific macro. In case you want to use a different definition for the macro, you can then override the current definition.

If you are running an analysis from the user interface (Polyspace desktop products only), on the Configuration pane, you can enter this option in the Other field. See Other. On the Output Summary pane, you can see each macro definition on a separate line. You can search for the macro name in the user interface and click the line with the macro name to see further details in the Detail pane.

Examples

Suppose that you use the ARM v6 compiler for building your source code. For the Polyspace analysis, you use the value armclang for the option Compiler (-compiler). Suppose that you want to know what Polyspace uses as definition for the macro __ARM_ARCH.

  1. Enter the following command and pipe the console output to a file that you can search later:

    polyspace-bug-finder -sources aFile.c -compiler armclang -dump-preprocessing-info
    aFile.c can be a simple C file. You can also replace polyspace-bug-finder with polyspace-code-prover, polyspace-bug-finder-server or polyspace-code-prover-server.

  2. Search for __ARM_ARCH in the file containing the console output. You can see the line with the macro definition:

    Remark: Definition of macro __ARM_ARCH (pre-processing __polyspace__stdstubs.c)
|#define __ARM_ARCH 8
|defined by syntax extension xml file
|predefined macro
    In this example, the macro is set to the value 8.

See Also

Topics