Setting Up a Target

Target/Compiler Overview

Many applications are designed to run on specific target CPUs and operating systems. The type of CPU determines many data characteristics, such as data sizes and addressing. These factors can affect whether errors (such as overflows) will occur.

Since some run-time errors are dependent on the target CPU and operating system, you must specify the type of CPU and operating system used in the target environment before running a verification.

For detailed information on each Target/Compilation option, see Target/Compilation Options in the Polyspace Products for C/C++ Reference.

Back to Top

Specifying Target Environment

The Compiler Settings tab in the Configuration pane of the Project Manager perspective allows you to specify the target operating system and processor type for your application.

To specify the target environment for your application:

1. From the Target operating system drop-down list, select the operating system on which your application is designed to run.

   

2. From the Target processor type drop-down list, select the processor on which your application is designed to run.

For detailed specifications for each predefined target processor, see Predefined Target Processor Specifications.

Specifying Target/Compilation Parameters

You can also set Target/Compilation options through the Configuration > All Settings tab in the Project Manager perspective.

To specify target parameters for your configuration:

1. In the Configuration pane, select the All Settings tab. Under Analysis options, you see different categories of options, for example, General, Target/Compilation, and Compliance with standards

2. Expand Target/Compilation.

3. The Target/Compilation options appear.

   

4. Select the Target processor type for your application.

5. Specify the Operating system target for your application.

For detailed specifications for each predefined target processor, see Predefined Target Processor Specifications.

For information on each Target/Compilation option, see Target/Compilation Options in the Polyspace Products for C/C++ Reference.

Back to Top

Predefined Target Processor Specifications

Polyspace software supports many commonly used processors, as listed in the table below. To specify one of the predefined processors, select it from the Target processor type drop-down list.

Predefined Target Processor Specifications

Note   The following target processors are supported only for C code verifications: tms320c3x, sharc21x61, NEC-V850, hc08, hc12, mpc5xx, and c18.

After selecting a predefined target, you can modify some default attributes by selecting the browse button to the right of the Target processor type drop-down menu. The optional settings for each target are shown in [brackets] in the table.

If your processor is not listed, you can specify a similar processor that shares the same characteristics, or create a generic target processor.

Note   If your target processor does not match the characteristics of any processor described above, contact MathWorks technical support for advice.

Back to Top

Modifying Predefined Target Processor Attributes

You can modify certain attributes of the predefined target processors. If your specific processor is not listed, you may be able to specify a similar processor and modify its characteristics to match your processor.

Note   The settings that you can modify for each target are shown in [brackets] in the Predefined Target Processor Specifications table.

To modify target processor attributes:

1. In the Project Manager perspective, select the Configuration > All Settings tab.

2. Expand the Target/Compilation node.

   

3. Select the Target processor type you want to use.

4. Select the browse button to the right of the Target processor type drop-down menu.

   The Advanced target options dialog box opens.

   

5. Modify the attributes as needed.

   For information on each target option, see Generic Target Options in the Polyspace Products for C/C++ Reference.

6. Click OK to save your changes.

Back to Top

Defining Generic Target Processors

If your application is designed for a custom target processor, you can configure many basic characteristics of the target by selecting the selecting the mcpu... (Advanced) target, and specifying the characteristics of your processor.

To configure a generic target:

1. In the Project Manager perspective, select the Configuration > All Settings tab.

2. Under Analysis options, expand the Target/Compilation node.

3. From the Target processor type drop-down list, select mcpu... (Advanced).

   The Generic target options dialog box opens.

   

4. In the Enter the target name field, enter a name for your target.

5. Specify the appropriate parameters for your target, such as the size of basic types, and alignment with arrays and structures.

   For example, when the alignment of basic types within an array or structure is always 8, it implies that the storage assigned to arrays and structures is strictly determined by the size of the individual data objects (without fields and end padding).

   Note   For information on each target option, see Generic Target Optionsin the Polyspace Products for C/C++ Reference.

6. Click Save to save the generic target options and close the dialog box.

Back to Top

Common Generic Targets

The following tables describe the characteristics of common generic targets.

ST7 (Hiware C compiler : HiCross for ST7)

ST9 (GNU C compiler : gcc9 for ST9)

Hitachi H8/300, H8/300L

Hitachi H8/300H, H8S, H8C, H8/Tiny

Back to Top

Viewing Existing Generic Targets

Generic targets that you create are listed in the Polyspace Preferences dialog box.

To view existing generic targets:

1. Select Options > Preferences.

   The Preferences dialog box appears.

2. Select the Generic targets tab.

   Previously defined generic targets appear in the generic targets list.

   

3. Click Cancel to close the dialog box.

Back to Top

Deleting a Generic Target

Generic targets that you create are stored as a Polyspace software preference. Generic targets remain in your preferences until you delete them.

Note   You cannot delete a generic target if it is the currently selected target processor type for the project.

To delete a generic target:

1. Select Options > Preferences.

   The Polyspace Preferences dialog box opens.

2. Select the Generic targets tab.

3. Select the target you want to remove.

4. Click Remove.

5. Click OK to apply the change and close the dialog box.

Back to Top

Compiling Operating System Dependent Code (OS-target issues)

This section describes the options required to compile and verify code designed to run on specific operating systems. It contains the following:

• Predefined Compilation Flags for C Code

• Predefined Compilation Flags for C++ Code

• My Target Application Runs on Linux

• My Target Application Runs on Solaris

• My Target Application Runs on Vxworks

• My Target Application Does Not Run on Linux, vxworks nor Solaris

Predefined Compilation Flags for C Code

These flags concern the predefined OS-target options: no-predefined-OS, linux, vxworks, Solaris and visual (-OS-target option).

Note   The use of the OS-target option is entirely equivalent to the following alternative approaches. Setting the same -D flags manually, or Using the -include option on a copied and modified pst-OS-target.h file

Predefined Compilation Flags for C++ Code

The following table shown for each —OS-target, the list of compilation flags defined by default, including pre-include header file (see also –include):

Note   This list of compiler flags is written in every log file.

My Target Application Runs on Linux

The minimum set of options is as follows:

polyspace-c \
	-OS-target Linux \
	-I Polyspace_Install/Verifier/include/include-linux \
	-I Polyspace_Install/Verifier/include/include-linux/next \
	...

where the Polyspace product has been installed in the folder Polyspace_Install.

If your target application runs on Linux but you are launching your verification from Windows, the minimum set of options is as follows:

polyspace-c \
	-OS-target Linux \
	-I Polyspace_Install\Verifier\include\include-linux \
	-I Polyspace_Install\Verifier\include\include-linux\next \
	...

where the Polyspace product has been installed in the folder Polyspace_Install.

My Target Application Runs on Solaris

If Polyspace software runs on a Linux machine:

polyspace-c \
	-OS-target Solaris \
	-I /your_path_to_solaris_include

If Polyspace software runs on a Solaris™ machine:

polyspace-c \
	-OS-target Solaris \
	-I /usr/include

My Target Application Runs on Vxworks

If Polyspace software runs on either a Solaris or a Linux machine:

polyspace-c \
	-OS-target vxworks \
	-I /your_path_to/Vxworks_include_folders

My Target Application Does Not Run on Linux, vxworks nor Solaris

If Polyspace software does not run on either a Solaris or a Linux machine:

polyspace-c \
	-OS-target no-predefined-OS \
	-I /your_path_to/MyTarget_include_folders

Back to Top

Address Alignment

Polyspace software handles address alignment by calculating sizeof and alignments. This approach takes into account 3 constraints implied by the ANSI standard which guarantee that: 

• that global sizeof and offsetof fields are optimum (i.e. as short as possible); 

• the alignment of all addressable units is respected;

• global alignment is respected.

Consider the example:

struct foo {char a; int b;} 

• Each field must be aligned; that is, the starting offset of a field must be a multiple of its own size^[7]

• So in the example, char a begins at offset 0 and its size is 8 bits. int b cannot begin at 8 (the end of the previous field) because the starting offset must be a multiple of its own size (32 bits). Consequently, int b begins at offset=32. The size of the struct foo before global alignment is therefore 64 bits. 

• The global alignment of a structure is the maximum of the individual alignments of each of its  fields; 

• In the example, global_alignment = max (alignment char a, alignment int b) = max (8, 32) = 32 

• The size of a struct must be a multiple of its global alignment. In our case, b begins at 32 and is 32 long, and the size of the struct (64) is a multiple of the global_alignment (32), so sizeof is not adjusted.

Back to Top

Ignoring or Replacing Keywords Before Compilation

You can ignore noncompliant keywords such as "far" or 0x followed by an absolute address. The template provided in this section allows you to ignore these keywords.

To ignore keywords:

1. Save the following template in c:\Polyspace\myTpl.pl.

2. In the Target/Compilation options, select Command/script to apply to preprocessed files.

3. Select myTpl.pl using the browse button.

For more information, see -post-preprocessing-command.

Content of the myTpl.pl file

#!/usr/bin/perl

##############################################################
# Post Processing template script
#
##############################################################
# Usage from Project Manager GUI:
#
# 1) Linux: /usr/bin/perl PostProcessingTemplate.pl
# 2) Solaris: /usr/local/bin/perl PostProcessingTemplate.pl
# 3) Windows: \Verifier\tools\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;

	# Convert current line to lower case
# $_ =~ tr/A-Z/a-z/;

	# Print the current processed line
	print $OUTFILE $_;
}

Perl Regular Expression Summary

#########################################################
# 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 occurence 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/;
#
##########################################################

Back to Top

Verifying Code That Uses Keil or IAR Dialects

Typical embedded control applications frequently read and write port data, set timer registers and read input captures. To deal with this without using assembly language, some microprocessor compilers have specified special data types like sfrand sbit. Typical declarations are:

sfr A0 = 0x80; 
sfr A1 = 0x81; 
sfr ADCUP = 0xDE; 
sbit EI = 0x80; 

These declarations reside in header files such as regxx.h for the basic 80Cxxx micro processor. The definition of sfr in these header files customizes the compiler to the target processor.

When accessing a register or a port, using sfr data is then simple, but is not part of standard ANSI C:

int status,P0; 

void main (void) { 
  ADCUP = 0x08; /* Write data to register */ 
  A1 = 0xFF; /* Write data to Port */ 
  status = P0; /* Read data from Port */ 
  EI = 1; /* Set a bit (enable all interrupts) */ 
} 

You can verify this type of code using the Dialect support option (-dialect). This option allows the software to support the Keil or IAR C language extensions even if some structures, keywords, and syntax are not ANSI standard. The following tables summarize what is supported when verifying code that is associated with the Keil or IAR dialects.

The following table summarizes the supported Keil C language extensions:

Example: -dialect keil -sfr-types sfr=8

bit x = 0, y = 1,
 z = 2;
assert(x == 0);
assert(y == 1);
assert(z == 1);
assert(sizeof(bit)
 == sizeof(int));

sfr x = 0xf0; // 
declaration of
variable x at 
address 0xF0
sfr16 y = 0x4EEF;
 

-dialect keil 
-sfr-types sfr=8,		\
				sfr16=16

sfr x = 0xF0;
sbit x1 = x ^ 1; // 1st bit of x
sbit x2 = 0xF0 ^ 2; // 2nd bit of x
sbit x3 = 0xF3; // 3rd bit of x
sbit y0 = t[3] ^ 1;

/* file1.c */
sbit x = P0 ^ 1;
/* file2.c */
extern bit x;
x = 1; // set the 1st bit of P0 to 1

int var _at_ 0xF0
int x @ 0xFE ;
static const 
int y @ 0xA0 = 3;

void foo1 (void) 
interrupt XX = YY
using 99 {…}
void foo2 (void) _
task_ 99 _priority_
2 {…}

The following table summarize the IAR dialect:

Example: -dialect iar -sfr-types sfr=8

union { 
  int v; 
  struct { 
    int z; 
  } y; 
} s; 

void f(void) { 
  bit y1 = s.y.z . 2; 
  bit x4 = x.4; 
  bit x5 = 0xF0 . 5; 
  y1 = 1; 
	// 2nd bit of s.y.z
	// is set to 1 
}; 

sfr x = 0xf0; // 
declaration of
variable x at 
address 0xF0

int x[3], y;
x[2].2 = x[0].3 + y.1;

int var @ 0xF0; 
int xx @ 0xFE ; 
static const int y   \
	@0xA0 = 3; 

interrupt [1] 		 \
 using [99] void 	 \ 
 foo1(void) { ... }; 

monitor [3] void 	 \
 foo2(void) { ... }; 

union { int x; };
union { int y; struct { int
z; }; } @ 0xF0;

no_init int x;
no_init union 
{ int y; } @ 0xFE;

The option –sfr-types defines the size of a sfr type for the Keil or IAR dialect.

The syntax for an sfr element in the list is type-name=typesize.

For example:

–sfr-types sfr=8,sfr16=16

defines two sfr types: sfr with a size of 8 bits, and sfr16 with a size of 16-bits. A value type-name must be given only once. 8, 16 and 32 are the only supported values for type-size.

Note   As soon as an sfr type is used in the code, you must specify its name and size, even if it is the keyword sfr.

Note   Many IAR and Keil compilers currently exist that are associated to specific targets. It is difficult to maintain a complete list of those supported.

Back to Top

How to Gather Compilation Options Efficiently

The code is often tuned for the target (as discussed to Verifying Code That Uses Keil or IAR Dialects). Rather than applying minor changes to the code, create a single polyspace.h  file which will contain all target specific functions and options. The -include option can then be used to force the inclusion of the polyspace.h file in all source files under verification.

Where there are missing prototypes or conflicts in variable definition, writing the expected definition or prototype within such a header file will yield several advantages.

Direct benefits:

• The error detection is much faster since it will be detected during compilation rather than in the link or subsequent phases.

• The position of the error will be identified more precisely.

• There will be no need to modify original source files.

Indirect benefits:

• The file is automatically included as the very first file in all original .c files.

• The file can contain much more powerful macro definitions than simple -D options.

• The file is reusable for other projects developed under the same environment.

Example

This is an example of a file that can be used with the -include option.

// The file may include (say) a standard include file implicitly 
// included by the cross compiler 

#include <stdlib.h> 
#include "another_file.h" 

// Generic definitions, reusable from one project to another 
#define far 
#define at(x) 

// A prototype may be positioned here to aid in the solution of 
// a link phase conflict between 
// declaration and definition. This will allow detection of the 
// same error at compilation time instead of at link time. 
// Leads to: 
// - earlier detection 
// - precise localisation of conflict at compilation time 
void f(int); 

// The same also applies to variables. 
extern int x; 

// Standard library stubs can be avoided, 
// and OS standard prototypes redefined. 

#define POLYSPACE_NO_STANDARD_STUBS	// use this flag to prevent the
									 				//automatic stubbing of std functions 
#define __polyspace_no_sscanf 
#define __polyspace_no_fgetc 
void sscanf(int, char, char, char, char, char); 
void fgetc(void); 

^[a] The M68k family (68000, 68020, etc.) includes the "ColdFire" processor

^[b] All operations on long double values will be imprecise (that is, shown as orange).

^[c] Non ANSI C specified keywords and compiler implementation-dependent pragmas and interrupt facilities are not taken into account by this support

^[d] All kinds of pointers (near or far pointer) have 2 bytes (hc08) or 4 bytes (hc12) of width physically.

^[e] The c18 target supports the type short long as 24-bits.

^[f] Use option -long-is-32bits to support Microsoft C/C++ Win64 target

^[7] except in the cases of "double" and "long" on some targets.

Back to Top

Emulating Your Runtime Environment

Verifying a C Application Without a "Main"