Remove or Replace Keywords Before Compilation

R2026b

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, use the command polyspace-configure. 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).

For a list of build options that you can use to manually emulate your build, see Configure Sources and Build Options.

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).

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

   Content of myTpl.pl

   #!/usr/bin/perl
   
   ##############################################################
   # Post Processing template script
   #
   ##############################################################
   # Usage from GUI:
   #
   # 1) Linux: /usr/bin/perl PostProcessingTemplate.pl
   # 2) Windows: polyspaceroot\sys\perl\win32\bin\perl.exe <pathtoscript>\
   # PostProcessingTemplate.pl
   #
   ##############################################################
   
   $version = 0.1;
   
   $INFILE = STDIN;
   $OUTFILE = STDOUT;
   
   while (<$INFILE>)
   {
   
       # Remove far keyword
       s/far//;
   
       # Remove "@ 0xFE1" address constructs
       s/\@\s0x[A-F0-9]*//g;
   
       # Remove "@0xFE1" address constructs
       s/\@0x[A-F0-9]*//g;
   
       # Remove "@ ((unsigned)&LATD*8)+2" type constructs
       s/\@\s\(\(unsigned\)\&[A-Z0-9]+\*8\)\+\d//g;
   
       # DON'T DELETE LINE BELOW: Print the current processed line
       print $OUTFILE $_;
   }

   For reference, see a summary of Perl regular expressions.

   Perl Regular Expressions

   #########################################################
   # Metacharacter What it matches
   #########################################################
   # Single Characters
   # . Any character except newline
   # [a-z0-9] Any single character in the set
   # [^a-z0-9] Any character not in set
   # \d A digit same as
   # \D A non digit same as [^0-9]
   # \w An Alphanumeric (word) character
   # \W Non Alphanumeric (non-word) character
   #
   # Whitespace Characters
   # \s Whitespace character
   # \S Non-whitespace character
   # \n newline
   # \r return
   # \t tab
   # \f formfeed
   # \b backspace
   #
   # Anchored Characters
   # \B word boundary when no inside []
   # \B non-word boundary
   # ^ Matches to beginning of line
   # $ Matches to end of line
   #
   # Repeated Characters
   # x? 0 or 1 occurrence of x
   # x* 0 or more x's
   # x+ 1 or more x's
   # x{m,n} Matches at least m x's and no more than n x's
   # abc All of abc respectively
   # to|be|great One of "to", "be" or "great"
   #
   # Remembered Characters
   # (string) Used for back referencing see below
   # \1 or $1 First set of parentheses
   # \2 or $2 First second of parentheses
   # \3 or $3 First third of parentheses
   ##########################################################
   # Back referencing
   #
   # e.g. swap first two words around on a line
   # red cat -> cat red
   # s/(\w+) (\w+)/$2 $1/;
   #
   ##########################################################

2. On the Configuration pane, select Environment Settings.

3. To the right of Command/script to apply to preprocessed files, click .

4. Use the Open File dialog box to navigate to C:\Polyspace.

5. In the File name field, enter myTpl.pl.

6. 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).