Polyspace Inner Settings Options

Run a verification unit by unit (-unit-by-unit)

This option creates a separate verification job for each source file in the project.

Each file is compiled, sent to the Polyspace Server, and verified individually. Verification results can be viewed for the entire project, or for individual units.

Note   Unit by unit verification is available only for server verifications. It is not compatible with multitasking options such as -entry-points.

Default:

            Not selected

Example Shell Script Entry:

      polyspace-c -unit-by-unit

Back to Top

Unit by Unit common source files (-unit-by-unit-common-source)

Specifies a list of files to include with each unit verification. These files are compiled once, and then linked to each unit before verification. Functions not included in this list are stubbed.

Default:

            None

Example Shell Script Entry:

      polyspace-c -unit-by-unit-common-source c:/polyspace/function.c

Back to Top

Main Generator Behavior for Polyspace Software

This same options can be used for both Polyspace Client™ for C/C++ and Polyspace Server™ for C/C++ verifications, but the default behavior differs between the two:

• Server Verification – You have the choice whether to activate the main generator.

• Client Verification – The main generator is always activated.

Polyspace Client for C/C++ Main Generator

For client verifications, you do not need to determine whether the code contains a "main" or not. Polyspace Client for C/C++ product automatically checks your code for a main.

• If a main exists in the set of files, the verification uses that main.

• If a main does not exist, the tool generates a main using the options you specify.

Polyspace Server for C/C++ Main Generator

If you do not select the -main-generator option, a Polyspace Server for C/C++ verification stops if it does not detect a main. This behavior can help isolate files missing from the verification.

When you select the -main-generator option, the Polyspace Server for C/C++ product checks your code for a main.

• If a main exists in the set of files, the verification uses that main.

• If a main does not exist, the tool generates a main using the options you specify.

Back to Top

Generate a main (-main-generator)

This option activates the Polyspace main generator.

When you select this option, the main generator automatically generates a main unless a main already exists in your verification.

The generated main has the following behavior.

1. It initializes any variables identified by the option -variables written-before-loop.

2. It calls any functions specified by the option -functions-called-before-loop. This could be considered an initialization function.

3. It initializes any variables identified by the option -variables written-in-loop.

4. It calls any functions specified by the option -functions-called-in-loop.

5. It calls any functions specified by the option -functions-called-after-loop. This could be a terminate function for a cyclic program.

The following sections describe each of these options in detail.

Note   The main generator is always active for client verifications.

Main for Generated Code

The following example shows how to use the main generator options to generate a main for a cyclic program, such as code generated from a Simulink^® model.

init parameters		\\ -variables-written-before-loop
init_fct()				\\ -functions-called-before-loop
	while(1){			\\ start main loop
	init inputs			\\ -variables-written-in-loop
	step_fct()			\\ -functions-called-in-loop
}
terminate_fct()		\\ -functions-called-after-loop

Back to Top

Variables written before loop (-variables-written-before-loop)

This option specifies how the generated main initializes global variables.

Settings available:

• -none (default) — no global variable will be written by the main.

• -public — every variable except static and const variables are assigned a "random" value, representing the full range of possible values

• -all — every variable except const variables are assigned a "random" value, representing the full range of possible values

• -custom — only variables present in the list are assigned a "random" value, representing the full range of possible values

When defining the main for a cyclic program (such as generated code from a Simulink model), use this option to define how the main initializes your init parameters.

Example
polyspace-c -main-generator -variables-written-before-loop none
polyspace-c -main-generator -variables-written-before-loop custom=variable_a,variable_b

Back to Top

Variables written in loop (-variables-written-in-loop)

Specifies how the generated main initializes global variables within a cyclic program loop.

This option is useful when defining the main for a cyclic program, such as code generated from a Simulink model. When defining the main for a cyclic program, use this option to define how the main initializes inputs within the program loop.

Settings available:

• -none (default) — no global variable will be written by the main.

• -public — every variable except static and const variables are assigned a "random" value, representing the full range of possible values

• -all — every variable except const variables are assigned a "random" value, representing the full range of possible values

• -custom — only variables present in the list are assigned a "random" value, representing the full range of possible values

Example
polyspace-c -main-generator -variables-written-in-loop none
polyspace-c -main-generator -variables-written-in-loop custom=variable_a,variable_b

Back to Top

Functions called before loop (-function-called-before-loop)

Specifies an initialization function, or list of functions, that are called on startup after the initialization of the global variables and before the main loop.

The skeleton of the generated main looks like:

1. Initialization of global variables

2. Call the specified functions fname1, fname2

3. Main loop with a call to all the functions specified using the option -functions-called-in-loop

Example shell script entry:

polyspace-c -main-generator -function-called-before-loop MyInitFunction,MyFunction2

Back to Top

Functions called in loop (-functions-called-in-loop)

Specifies the functions to be called within the loop of the generated main.

Possible values:

• none — no function is called. This can be used with a multitasking application without a main.

• unused (default) — every function is called by the generated main unless it is called elsewhere by the code undergoing verification.

• all — every function is called by the generated main except inlined.

• custom — only functions present in the list are called from the main. Inlined functions can be specified in the list.

An inline (static or extern) function is not called by the generated main program with values all or unused. An inline function can only be called with custom value: -main-generator-calls custom=my_inlined_func.

Note   When using the unused option, the generated main may call functions that are also called by a function pointer, meaning these functions may be called twice.

Example:

polyspace-c -main-generator -functions-called-in-loop public

polyspace-c -main-generator -functions-called-in-loop custom=function_1,function_2

Back to Top

Functions called after loop (-function-called-after-loop)

Specifies a function, or list of functions, that are called after the main loop of the generated main.

This option is useful when defining the main for a cyclic program, such as code generated from a Simulink model. When defining the main for a cyclic program, use this option to define the terminate function after the main loop.

The skeleton of the generated main looks like:

1. Initialization of global variables

2. Main loop with a call to all the functions specified using the option -functions-called-in-loop

3. Call the specified functions fname1, fname2

Example shell script entry:

polyspace-c -main-generator -function-called-after-loop MyTermFunction,MyFunction2

Back to Top

Variable/function range setup (-data-range-specifications)

This option permits the setting of specific data ranges for a list of given global variables.

For more information, see Specifying Data Ranges for Variables and Functions (Contextual Verification).

File format:

The file filename contains a list of global variables with the below format:

variable_name val_min val_max <init|permanent|globalassert>

Variables scope:

Variables concern external linkage, const variables and not necessary a defined variable (i.e. could be extern with option -allow-undef-variables).

Note   Only one mode can be applied to a global variable. No checks are added with this option except for globalassert mode. Some warning can be displayed in log file concerning variables when format or type is not in the scope.

Default:

Disable.

Example shell script entry:

polyspace-c -data-range-specifications range.txt ...

Back to Top

Stub complex functions (-permissive-stubber)

By default, the stubber rejects functions:

• with complex function pointers as parameters

• with function pointers as return type

To eliminate these restrictions and stub all functions, specify the Stub complex functions (-permissive-stubber) option.

Caution   Using this option may produce inaccurate results.

Note   This option cannot be used with the –no-automatic-stubbing option. This option is set automatically when you select the -permissive option.

Back to Top

Functions to stub (-functions-to-stub)

Specifies functions that you want the software to stub.

Enter a comma-separated list of functions. For example, function_1,function_2.

The following special characters are allowed for C functions:

( ) < > ; _

Spaces are not allowed for C functions.

Example Shell Script Entry:

 polyspace-c -functions-to-stub function_1,function_2 ...

Back to Top

No automatic stubbing (-no-automatic-stubbing)

By default, Polyspace verification automatically stubs all functions. When this option is used, the list of functions to be stubbed is displayed and the verification is stopped.

Benefits:  

This option may be used where

• The entire code is to be provided, which may be the case when verifying a large piece of code. When the verification stops, it means the code is not complete.

• Manual stubbing is preferred to improve the selectivity and speed of the verification.

Note   This option cannot be used with the –permissive-stubber option.

Default:  

All functions are stubbed automatically

Back to Top

Division round down (-div-round-down)

This option concerns the division and modulus of a negative number.

The ANSI standard stipulates that "if either operand of / or % is negative, whether the result of the / operator, is the largest integer less or equal than the algebraic quotient or the smallest integer greater or equal than the quotient, is implementation defined, same for the sign of the % operator".

Note   a = (a / b) * b + a % b is always true.

Default:

Without the option (default mode), if either operand of / or % is negative, the result of the / operator is the smallest integer greater or equal than the algebraic quotient. The result of the % operator is deduced from a % b = a - (a / b) * b   

Example:

    assert(-5/3 == -1 && -5%3 == -2); is true .

With the -div-round-down option:

If either operand / or % is negative, the result of the / operator is the largest integer less or equal than the algebraic quotient. The result of the % operator is deduced from a % b = a - (a / b) * b .  

 Example:

    assert(-5/3 == -2 && -5%3 == 1); is true .

Example Shell Script Entry:

 polyspace-c -div-round-down ...

Back to Top

Do not consider all global variables to be initialized (-no-def-init-glob)

This option specifies that Polyspace verification should not take into account default initialization defined by ANSI C. When this option is not used, default initialization are

• 0 for integers

• 0 for characters

• 0.0 for floats

With the option in use, all global variable will be treated as non initialized, and therefore cause a red NIV error if they are read before being written to.

NIV Example 1:

1	 int var;		// line 1: -no-def-init-glob does not follow ANSI C
2      	    		// initialization behavior on global variables 
3	 int main(void) 
4	 { 
5		int res; 
6		res = var;	// line 6: red NIV using -no-def-init-glob 
7		return res; 
8  } 

To change the red NIV to green using the -no-def-init-glob option, change line 1 to:

int var = 0;

NIV Example 2 — With Tasks:

	// -entry-points t1, t2, 
	// -no-def-init-glob 
	
1		int var;  								// line 1 
2		void main(void) { var = 1;} 		// line 2 
3		void t1(void) 
4		{ 
5			int res; 
6			while(1) { 
7				res = var; 		// line 7: green NIV using -no-def-init-glob 
8									// because var has been initialized before read 
9			} 
10	} 
11	static var2; 							// line 11 
12	void t2(void) 
13	{ 
14		int res; 
15		while(1) { 
16		res = var2; 	// line 16: red NIV using -no-def-init-glob because 
17          				// var2 is not initialized before first read 
18		} 
19	} 

At line 7, the variable has a green NIV because the variable has been written before first read in task t1(). At line 16, the verification reports a red NIV because a global variable has not been explicitly written before first read.

To workaround the red NIV at line 16, change line 11 to:

static var2 = 0;

Example Shell Script Entry :

 polyspace-c -no-def-init-glob ...

Back to Top

Enable pointer arithmetic out of bounds of fields (-allow-ptr-arith-on-struct)

This option enables navigation within a structure or union from one field to another, within the rules defined below. It automatically sets the -size-in-bytes option.

Default

By default, when a pointer points to a variable then the size of the objected pointed to is that of that variable - regardless of whether it is contained within a bigger object, like a structure. Therefore, going out of the scope of this variable leads to a red IDP check (Illegal Dereference Pointer). This is illustrated below.

struct S {char a; char b; int c;} x;
	char *ptr = &x.b;
	ptr ++;
	*ptr = 1; // red on the dereference, because the pointed
object was "b"

Using this option

When this option is used in the above option, Polyspace verification considers that the object pointed to is now the host object "x". The "ptr" pointer is in fact pointing to &x, with the correct offset to the field "b" within the structure of type S (inter-fields and end-padding included). Therefore, the dereference becomes green

Consider a second example:

int main()
{

	struct S {
		char a;
		/* 3 bytes of padding between 'a', 'b' */
		int b;
		int c;
		char d[3];
		unsigned char e:7;
		char f;
		/* 3 bytes of end padding */
	} x;
	char *ptr;
	struct Nesting_S {
		struct S s;
		int c;
		char buf[8];
		int d;
	} z
	
	struct S *ptr0;
	char *ptr;
	
	ptr = &z.s.f;
	ptr += 4;
	*(int *)ptr = 10; /* access to z.c, Green IDP */
	
	ptr0 = &z.s;
	ptr = &ptr0->f;
	ptr += 4;
	
	*(int *) ptr = 10; /* access to z.c, Green IDP */
	
	ptr = &z.buf[0];
	ptr += 8;
	*(int *)ptr = 10; /* access to z.d, Green IDP */
	
	return (0);
}

In the third example below, the *ptr access is red regardless of whether the option is set or not. 

With the option set, the ptr pointer points to the structure+offset z.s, and ptr can safely navigate within this structure z.s, but z.c is outside it.

Without the option, the ptr pointer points to z.s.f, which is only 1 byte long. So no navigation is allowed, not even within z.s.

ptr = (char *)z.s.f; ptr += 4; *ptr = 10; // ptr points to the
first byte of c:

Back to Top

Allows incomplete or partial allocation of structures (-size-in-bytes)

This option allows incomplete or partial allocation of structures. This allocation can be made by malloc or cast .

The example below shows an example using malloc. Further explanation can be found in the section describing the partial and incomplete allocation of structures. Also refer to the -allow-ptr-arith-on-struct section.

typedef struct _little { int a; int b; } LITTLE;
typedef struct _big { int a; int b; int c; } BIG;
BIG *p = malloc(sizeof(LITTLE));

Default results

	p->a = 0 ; 		// red pointer out of its bounds
or p->b = 0 ; 	// red pointer out of its bounds
or p->c = 0 ; 	// red pointer out of its bounds

Results using this option

if (p!= ((void *) 0) ) {
	p->a = 0 ; 		// green pointer within bounds
or p->b = 0 ; 	// green pointer within bounds
or p->c = 0 ; 	// red pointer out of its bounds
}

Back to Top

Ignore float rounding (-ignore-float-rounding)

Without this option, Polyspace verification rounds floats according to the IEEE^® 754 standard: simple precision on 32-bits targets and double precision on target which define double as 64-bits.

With the option, exact computation is performed.

Example:

void ifr(float f) 
{ 
	double a,b; 
 	a = 0.2; 
 	b = 0.2; 
   
 	if ( a + b == 0.4) { 
		// reached whether -ignore-float-rounding is used or not 
		assert (1);                   
		f = 1.0F*f; 
 	} 
	else { 
		assert (1); 
		f = 1.0F * f; 
		// reached only when -ignore-float-rounding is not used 
	} 
} 

Using this option can lead to different results compared to the "real life" (compiler and target dependent): Some paths will be reachable or not for Polyspace verification while they are not (or are) depending of the compiler and target. So it can potentially give approximate results (green should be unproven). This option has an impact on OVFL/UNFL checks on floats.

 However, this option allows reducing the number of unproven checks because of the "delta" approximation.

For example:

• FLT_MAX (with option set) = 3.40282347e+38F

• FLT_MAX (following IEEE 754 standard) = 3.40282347e+38F ± Δ

void ifr(float f) 
{ 
	double a,b; 
	a = 0.2; 
	b = 0.2; 
   
	if ( a + b == 0.4) { 
		assert (1);                   
		f = 1.0F*f; 		// Overflow never occurs because f <= FLT_MAX.
								// reached when -ignore-float-rounding is used
	} 
	else { 
		assert (1); 
		f = 1.0F * f; 		// OVFL could occur when f = (FLT_MAX + D)
								// reached when -ignore-float-rounding is not used
	} 
} 

Default:

IEEE 754 rounding under 32 bits and 64 bits.

Example Shell Script Entry:

polyspace-c -ignore-float-rounding ...

Back to Top

Green absolute address checks (-green-absolute-address-checks)

If you know that the absolute addresses in your code are valid, you can specify this option to make all ABS_ADDR checks green. Otherwise, the software generates an orange ABS_ADDR check when an absolute address is assigned to a pointer. This is because the software has no information about the absolute address and therefore cannot verify, for example, the address, availability of memory, and initialization of memory.

The software permits memory access to the absolute address after generating the orange ABS_ADDR check for the first assignment operation. IDP and NIV checks for memory access operations after the first assignment operation are green.

Default:

Orange ABS_ADDR check generated when an absolute address is assigned to a pointer.

Example Shell Script Entry:

polyspace-c -green-absolute-address-checks ...

Back to Top

Detect overflows on (-scalar-overflows-checks)

Specifies how verification handles overflowing computations on integers.

Possible settings are:

• none – The verification does not check for integer computation overflows. If a computation value exceeds the range of the result type, the result is wrapped, and no OVFL check is reported.

  For example, MAX_INT + 1 wraps to MIN_INT.

• signed (default) – Verification checks all signed integer computations and signed integer to signed integer conversions. The option -scalar-overflows-behavior specifies whether results for signed integers are restricted to an acceptable value or wrapped.

  For unsigned integer operations, the results are wrapped, and no OVFL check is reported.

  This behavior conforms to the ANSI C (ISO C++) standard.

• signed-and-unsigned – Verification checks all integer computations and integer conversions, including conversions that cause a change of signs.

  The option -scalar-overflows-behavior specifies whether operation results are restricted to an acceptable value or wrapped.

  This behavior is more strict than the ANSI C (ISO C++) standard requires.

Consider the examples below.

Example 1

When you use the signed-and-unsigned option, the following example generates an error:

unsigned char x;
x = 255;
x = x+1; 		//overflow due to this option

Using the none option, however, the example does not generate an error.

unsigned char x;
x = 255;
x = x+1;		// turns x into 0 (wrap around)

Example 2

When you use the signed-and-unsigned option, the following example does not generate an error:

unsigned char Y=1;
Y = ~Y;		//no overflow and GREEN OVFL check 

As the ~ operator applies directly to an unsigned char variable, there is no risk of an overflow. The outcome of the operation is a wrapped-around unsigned char variable. In this example, the Polyspace verification continues with the value 254 assigned to the unsigned char variable Y.

Example Shell Script Entry:

 polyspace-c -scalar-overflows-checks signed ...

Back to Top

Overflows computation mode (-scalar-overflows-behavior)

Specifies how verification computes the results of overflowing integer computations or integer conversions.

Possible settings are:

• truncate-on-error (default) — Result of an overflowing operation is restricted to an acceptable value. If the check is red, verification stops (in the current code). If the check is orange, verification continues with restricted value.

• wrap-around — Result of an overflowing operation wraps around the type range. The check has no impact on values for the rest of the verification.

  For example, MAX_INT + 1 wraps to MIN_INT.

Example Shell Script Entry:

 polyspace-c -scalar-overflows-behavior wrap-around ...

Back to Top

Enum type definition (-enum-type-definition)

Allows the verification to use different base types to represent an enumerated type, depending on the enumerator values and the selected definition.

When using this option, each enum type is represented by the smallest integral type that can hold all its enumeration values.

Possible values are:

• defined-by-standard – Uses the integer type (signed int).

• auto-signed-first - Uses the first type that can hold all of the enumerator values from the following list: signed char, unsigned char, signed short, unsigned short, signed int, unsigned int, signed long, unsigned long, signed long long, unsigned long long.

• auto-unsigned-first - Uses the first type that can hold all of the enumerator values from the following lists:

  • If enumerator values are all positive: unsigned char, unsigned short, unsigned int, unsigned long, unsigned long long.

  • If one or more enumerator values are negative: signed char, signed short, signed int, signed long, signed long long.

Back to Top

Functions known to cause NTC (-known-NTC)

After a few verifications, you may discover that a few functions "never terminate". Some functions such as tasks and threads contain infinite loops by design, while functions that exit the program such as kill_task , exit or Terminate_Thread are often stubbed by means of an infinite loop. If these functions are used very often or if the results are for presentation to a third party, it may be desirable to filter all NTC of that kind in the Viewer.

This option is provided to allow that filtering to be applied. All NTC specified at launch will appear in the viewer in the known-NTC category, and filtering will be possible.

Default :

All checks for deliberate Non Terminating Calls appear as red errors, listed in the same category as any problem NTC checks.

Example Shell Script Entry :

 polyspace-c -known-NTC "kill_task,exit"

 polyspace-c -known-NTC "Exit,Terminate_Thread"

Back to Top

Continue with compile error (-continue-with-compile-error)

Specifies that verification continues even if some source files do not compile. Functions that are used but not specified are stubbed automatically.

If a source file contains global variables, you may also need to select the option -allow-undef-variables to enable verification.

Example Shell Script Entry :

 polyspace-c -continue-with-compile-error ...

Back to Top

Verification time limit (-timeout)

Specifies a time limit for the verification (in hours).

If the verification does not complete within the specified time, the verification fails.

You can specify fractions of an hour in decimal form. For example:

• -timeout 5.75 – Five hours, 45 minutes.

• -timeout 3,5 – Three hours, 30 minutes.

Example Shell Script Entry :

 polyspace-c -timeout 5.75 ...

Back to Top

Automatic Orange Tester (-automatic-orange-tester)

Activates the Automatic Orange Tester at the end of static verification. By running dynamic stress tests on unproven code, the Automatic Orange Test can identify orange checks that are potential run-time errors. See Automatically Testing Orange Code.

Note   The software still supports the option -prepare-automatic-tests. However, support for this option will cease in a future release.

With -automatic-orange-tester, the software does not support the following:

• -div-round-down

• -char-is-16bits

• -short-is-8bits

• Global asserts in the code of the form Pst_Global_Assert(A,B)

In addition, there are restrictions on other options. You must not specify the following with -automatic-orange-tester:

• -target [c18 | tms320c3c | x86_64 | sharc21x61]

• -data-range-specification (in global assert mode)

You must use the -target mcpu option together with -pointer-is-32bits.

Default :

Disabled

Example Shell Script Entry :

 polyspace-c -automatic-orange-tester ...

Back to Top

Number of automatic tests (-automatic-orange-tester-tests-number)

Specify total number of test cases that you want to the Automatic Orange Tester to run. Running more tests increases the chances of finding a run-time error, but takes more time to complete.

Option is available only if you select Automatic Orange Tester (-automatic-orange-tester). The maximum value that the software supports is 100,000.

Default:

500

Example Shell Script Entry:

polyspace-c -automatic-orange-tester -automatic-orange-tester-tests-number 550 ...

Back to Top

Maximum loop iterations (-automatic-orange-tester-loop-max-iteration)

Specify maximum number of iterations for a loop after which the Automatic Orange Tester considers the loop to be an infinite loop. A larger number of iterations decreases the chances of incorrectly identifying an infinite loop, but takes more time to complete.

Option is available only if you select Automatic Orange Tester (-automatic-orange-tester). The maximum value that the software supports is 1000.

Default:

1000

Example Shell Script Entry:

polyspace-c -automatic-orange-tester -automatic-orange-tester-loop-max-iteration 800 ...

Back to Top

Maximum test time (-automatic-orange-tester-timeout)

Maximum time (in seconds) allowed for a test before Automatic Orange Tester moves on to next test. Increasing test time reduces number of tests that time out, but increases total verification time.

Option is available only if you select Automatic Orange Tester (-automatic-orange-tester). The maximum value that the software supports is 60.

Default:

5 seconds

Example Shell Script Entry:

polyspace-c -automatic-orange-tester -automatic-orange-tester-timeout 10 ...

Back to Top

Run verification in 32 or 64-bit mode (-machine-architecture)

This option specifies whether verification runs in 32 or 64-bit mode.

Note   You should only use the option -machine-architecture 64 for verifications that fail due to insufficient memory in 32 bit mode. Otherwise, you should always run in 32–bit mode.

Available options are:

• -machine-architecture auto – Verification always runs in 32-bit mode.

• -machine-architecture 32 – Verification always runs in 32-bit mode.

• -machine-architecture 64 – Verification always runs in 64-bit mode.

Default:

           auto

Example Shell Script Entry:

polyspace-c -machine-architecture auto

Back to Top

Number of processes for multiple CPU core systems (-max-processes)

This option specifies the maximum number of processes that can run simultaneously on a multi-core system. The valid range is 1 to 128.

Note   To disable parallel processing, set: -max-processes 1.

Default:

            4

Example Shell Script Entry:

            polyspace-c -max-processes 1

Back to Top

Other Options

• -extra-flags

• -c-extra-flags

• -il-extra-flags

-extra-flags

This option specifies an expert option to be added to the analyzer. Each word of the option (even the parameters) must be preceded by -extra-flags.

These flags will be given to you by Technical Support as necessary for your verifications.

Default: 

 No extra flags.

Example Shell Script Entry:

 polyspace-c -extra-flags -param1 -extra-flags -param2 \

  -extra-flags 10 ...

-c-extra-flags

This option is used to specify an expert option to be added to a verification. Each word of the option (even the parameters) must be preceded by -c-extra-flags.

These flags will be given to you by MathWorks as necessary for your verifications.

Default:

No extra flags.

Example Shell Script Entry:

polyspace-c -c-extra-flags -param1 -c-extra-flags -param2 -c-extra-flags 10

-il-extra-flags

This option is used to specify an expert option to be added to a verification. Each word of the option (even the parameters) must be preceded by -il-extra-flags.

These flags will be given to you by MathWorks as necessary for your verifications.

Default:

No extra flags.

Example Shell Script Entry:

polyspace-c -il-extra-flags -param1 -il-extra-flags -param2 -il-extra-flags 10

Back to Top

Compliance with Standards Options

Precision/Scaling Options