Remove or Replace Keywords Before Compilation

The Polyspace^® compiler strictly follows the ANSI^® C99 Standard (ISO/IEC 9899:1999). If your compiler allows deviation from the Standard, the Polyspace compilation using default options cannot emulate your compiler. For instance, your compiler can allow certain non-ANSI keyword, which Polyspace does not recognize by default.

To emulate your compiler closely, you specify the Target & Compiler options. If you still get compilation errors from unrecognized keywords, you can remove or replace them only for the purposes of verification. The option Preprocessor definitions (-D) allows you to make simple substitutions. For complex substitutions, for instance to remove a group of space-separated keywords such as a function attribute, use the option Command/script to apply to preprocessed files (-post-preprocessing-command).

Remove Unrecognized Keywords

You can remove unsupported keywords from your code for the purposes of analysis. For instance, follow these steps to remove the far and 0x keyword from your code (0x precedes an absolute address).

Save the following template as C:\Polyspace\myTpl.pl.

Content of myTpl.pl

For reference, see a summary of Perl regular expressions.

Perl Regular Expressions

On the Configuration pane, select Environment Settings.
To the right of Command/script to apply to preprocessed files, click .
Use the Open File dialog box to navigate to C:\Polyspace.
In the File name field, enter myTpl.pl.
Click Open. You see C:\Polyspace\myTpl.pl in the Command/script to apply to preprocessed files field.

Remove Unrecognized Function Attributes

You can remove unsupported function attributes from your code for the purposes of analysis.

If you run verification on this code specifying a generic compiler, you can see compilation errors from the noreturn attribute. The code compiles using a GNU^® compiler.

void fatal () __attribute__ ((noreturn));
          
void fatal (/* ... */)
{
    /* ... */ /* Print error message. */ /* ... */
    exit (1);
}

If the software does not recognize an attribute and the attribute does not affect the code analysis, you can remove it from your code for the purposes of verification. For instance, you can use this Perl script to remove the noreturn attribute.

while ($line = <STDIN>) 
{

# __attribute__ ((noreturn))

  # Remove far keyword
  $line =~ s/__attribute__\ \(\(noreturn\)\)//g;
  
  # Print the current processed line to STDOUT
  print $line;
}

Specify the script using the option Command/script to apply to preprocessed files (-post-preprocessing-command).