Range Specification Macros in Polyspace Test xUnit API

You can specify the input and output ranges of tests written using the Polyspace^® Test™ xUnit API. You use various xUnit macros to define the ranges and perform associated range assessments. When you run static analysis on your tests, these range specifications act as external constraints on the input and output variables. This topic enumerates the macros that your can use to specify and assess input or output ranges.

For a tutorial on specifying ranges using these macros, see Test Functions and Constrain Polyspace Code Prover Analysis for Ranges of Inputs and Outputs.

Prerequisites

This topic describes test authoring using the Polyspace Test xUnit API. To compile these tests, you are required to know some file paths in advance. For your convenience, you can define environment variables to stand for the file paths, or otherwise include the file paths in your build. For more information, see Set Up C/C++ Testing and Code Profiling Using Self-Managed Builds.

Types of Range Specification Macros

Polyspace Test supports these types of range specification macros:

• Input range defining macros — These macros return a value from a specified range. This value is intended to be an input to a test.

• Input buffer filling macros — These macros fill a specified buffer using values within a specified range. The buffer is intended to be used by a test.

• Configuration macros — These macros configure which values are selected from a range during tests.

• Output range defining macros — These macros test whether a value is within a range. The value is expected to be the output of a function under test. Polyspace supports ASSERT, VERIFY, and ASSUME macros when testing the range of the output. For more about the differences among the three types of assessments, see Types of Assessment Macros.

List of Range Specification Macros

Configuration Macros

The range specification macros specify the range of an input. When running dynamic tests, Polyspace selects one of the values in the range to perform the tests. You can configure which value is selected by using the macro PST_RANGE_SET_POLICY(policy). You can set this values for policy:

• PST_RANGE_LOWER_BOUND — This value selects the lower bound of a range when running a test.

• PST_RANGE_UPPER_BOUND — This value selects the upper bound of a range when running a test.

• PST_RANGE_MIDPOINT — This value selects the midpoint of a range when running a test. the midpoint is computed as 0.5 × (upper bound + lower bound). For integer data types, the midpoint is rounded to the nearest smaller integer.

• PST_RANGE_RANDOM — This value selects a random value within a range when running a test. You can define an initial seed using the macro PST_RANGE_SET_RANDOM_SEED(seed).

Input Range Defining macros

You can specify range for an input variable and pick a specific value from the range for testing if the variable is a signed integer, an unsigned integer, or a floating number. The following table lists the input range specification macros for various data types.

Macro	Description	Returned data type	Static interpretation
PST_INT_IN_RANGE(min, max)	Returns an integer within the range [min..max]. Picks either the minimum value, the maximum value, the midpoint of the range, or a random value. The choice of the value is set by PST_RANGE_SET_POLICY().	int	Say you have this code: int var = PST_INT_IN_RANGE(min,max); During static analysis, Polyspace assumes var has the range [min..max].
PST_INT_IN_RANGE_USING_POLICY(min, max, policy)	Returns an integer within the range following the specified policy.	int
PST_INT_IN_RANGE_USING_VALUE(min, max, value)	At runtime, uses the specified value for dynamic testing.	int
PST_INT_ANY_VALUE()	Returns any signed integer value at runtime.	int	When you run static analysis, the function under test is analyzed assuming the input has a range [INT_MIN..INT_MAX].
PST_INT_ANY_VALUE_USING_POLICY(policy)	Returns any signed integer value using the specified policy.	int
PST_INT_ANY_VALUE_USING_VALUE(value)	At runtime, uses the specified value for dynamic testing.	int
PST_UINT_IN_RANGE(min, max)	Returns an unsigned integer within the range [min..max]. Picks either the minimum value, the maximum value, the midpoint of the range, or a random value. The choice of the value is set by PST_RANGE_SET_POLICY().	unsigned int	Say you have this code: int var = PST_UINT_IN_RANGE(min,max); During static analysis, Polyspace assumes var has the range [min..max].
PST_UINT_IN_RANGE_USING_POLICY(min, max, policy)	Returns an unsigned integer within the range following the specified policy.	unsigned int
PST_UINT_IN_RANGE_USING_VALUE(min, max, value)	Returns the specified value at runtime	unsigned int
PST_UINT_ANY_VALUE()	Returns any value at runtime.	unsigned int	When you run static analysis, the function under test is analyzed assuming the input has a range [UINT_MIN..UINT_MAX].
PST_UINT_ANY_VALUE_USING_POLICY(policy)	Returns any value using the specified policy.	unsigned int
PST_UINT_ANY_VALUE_USING_VALUE(value)	Returns the specified value at runtime	unsigned int
PST_FLT_IN_RANGE(min, max)	Returns a floating number within the range [min..max]. Picks either the minimum value, the maximum value, the midpoint of the range, or a random value. The choice of the value is set by PST_RANGE_SET_POLICY().	float	Say you have this code: int var = PST_FLT_IN_RANGE(min,max); During static analysis, Polyspace assumes var has the range [min..max].
PST_FLT_IN_RANGE_USING_POLICY(min, max, policy)	Returns a floating number within the range following the specified policy.	float
PST_FLT_IN_RANGE_USING_VALUE(min, max, value)	Returns the specified value at runtime	float
PST_FLT_ANY_VALUE()	Returns any value at runtime.	float	When you run static analysis, the function under test is analyzed assuming the input is a full range floating number. The floating number is assumed to have the largest size that fits your -target.
PST_FLT_ANY_VALUE_USING_POLICY(policy)	Returns any value using the specified policy.	float
PST_FLT_ANY_VALUE_USING_VALUE(value)	Returns the specified value at runtime	float

Input Buffer Filling Macros

You can fill buffers with integers, unsigned integer, or floating numbers using these macros:

Macro	Description	Static interpretation
PST_FILL_INT_BUFFER_WITH_RANGE(buffer, nmemb, membsz, min, max)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using an integer value within the range [min..max].	During static analysis, each element of the buffer is assumed to be an integer with the range [min..max]
PST_FILL_INT_BUFFER_WITH_RANGE_USING_POLICY(buffer, nmemb, membsz, min, max, policy)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using an integer value within the range [min..max]. The value is selected using policy.
PST_FILL_INT_BUFFER_WITH_RANGE_USING_VALUE(buffer, nmemb, membsz, min, max, value)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using an integer value value.
PST_FILL_INT_BUFFER_WITH_ANY(buffer, nmemb, membsz)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using any value.	During static analysis, each element of the buffer is assumed to be a full-range integer with the size memsz.
PST_FILL_INT_BUFFER_WITH_ANY_USING_POLICY(buffer, nmemb, membsz, policy)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using either INT_MIN, INT_MAX, the midpoint of the integer range, or a random value. Which of these values is picked depends on the policy.
PST_FILL_INT_BUFFER_WITH_ANY_USING_VALUE(buffer, nmemb, membsz, value)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using the specified value.
PST_FILL_UINT_BUFFER_WITH_RANGE(buffer, nmemb, membsz, min, max)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using an unsigned integer value within the range [min..max].	During static analysis, each element of the buffer is assumed to be an unsigned integer with the range [min..max]
PST_FILL_UINT_BUFFER_WITH_RANGE_USING_POLICY(buffer, nmemb, membsz, min, max, policy)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using an unsigned integer value within the range [min..max]. The value is selected using policy.
PST_FILL_UINT_BUFFER_WITH_RANGE_USING_VALUE(buffer, nmemb, membsz, min, max, value)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using an unsigned integer value value.
PST_FILL_UINT_BUFFER_WITH_ANY(buffer, nmemb, membsz)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using any unsigned integer value.	During static analysis, each element of the buffer is assumed to be a full-range unsigned integer with the size memsz.
PST_FILL_UINT_BUFFER_WITH_ANY_USING_POLICY(buffer, nmemb, membsz, policy)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using either UINT_MIN, UINT_MAX, the midpoint of the unsigned integer range, or a random value. Which of these values is picked depends on the policy.
PST_FILL_UINT_BUFFER_WITH_ANY_USING_VALUE(buffer, nmemb, membsz, value)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using the specified unsigned integer value.
PST_FILL_FLT_BUFFER_WITH_RANGE(buffer, nmemb, membsz, min, max)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using a floating point value within the range [min..max].	During static analysis, each element of the buffer is assumed to be a floating point number with the range [min..max]
PST_FILL_FLT_BUFFER_WITH_RANGE_USING_POLICY(buffer, nmemb, membsz, min, max, policy)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using a floating point value within the range [min..max]. The value is selected using policy.
PST_FILL_FLT_BUFFER_WITH_RANGE_USING_VALUE(buffer, nmemb, membsz, min, max, value)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using a floating point value value.
PST_FILL_FLT_BUFFER_WITH_ANY(buffer, nmemb, membsz)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using a floating point value.	During static analysis, each element of the buffer is assumed to be a full-range floating point number with the size memsz.
PST_FILL_FLT_BUFFER_WITH_ANY_USING_POLICY(buffer, nmemb, membsz, policy)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using either minimum possible floating point, the maximum possible floating point, the midpoint of the unsigned integer range, or a random value. Which of these values is picked depends on the policy.
PST_FILL_FLT_BUFFER_WITH_ANY_USING_VALUE(buffer, nmemb, membsz, value)	Fills the buffer pointed to by buffer, which must have nmemb elements of size memsz, using a floating point value value.

For these macros, memsz must be a valid size for your target.

Output Range Specification Macros

You can test if the output of a function is within an specified range. The following table lists the output assessment macros that use range specification. For details about output assessment using the xUnit API, see Assessment Macros in Polyspace Test API for C/C++ Code.

Macro	Description	Static interpretation
PST_ASSERT_INT_IN_RANGE[_MSG](value, min, max)	Assert, verify, or assume that value is in the range min..max. If assertion fails, emit message [MSG]. The specified range must be smaller than or equal to the full range of a variable.	During static analysis, Polyspace constraints the variable value with the range min..max.
PST_VERIFY_INT_IN_RANGE[_MSG](value, min, max)
PST_ASSUME_INT_IN_RANGE[_MSG](value, min, max)
PST_ASSERT_UINT_IN_RANGE[_MSG](value, min, max)
PST_VERIFY_UINT_IN_RANGE[_MSG](value, min, max)
PST_ASSUME_UINT_IN_RANGE[_MSG](value, min, max)
PST_ASSERT_FLT_IN_RANGE[_MSG](value, min, max)
PST_VERIFY_FLT_IN_RANGE[_MSG](value, min, max)
PST_ASSUME_FLT_IN_RANGE[_MSG](value, min, max)
PST_ASSERT_INT_BUFFER_IN_RANGE[_MSG](buffer, numel, sz, min, max)	Assert, verify, or assume that buffer contains numel consecutive elements of size sz and each element is within the range min..max. The specified range must be smaller than the full range of a variable with size sz. The size of the elements sz must be a valid size for the data type supported by the target processor.	During static analysis, Polyspace constraints each element of buffer with the range min..max.
PST_VERIFY_INT_BUFFER_IN_RANGE[_MSG](buffer, numel, sz, min, max)
PST_ASSUME_INT_BUFFER_IN_RANGE[_MSG](buffer, numel, sz, min, max)
PST_ASSERT_UINT_BUFFER_IN_RANGE[_MSG](buffer, numel, sz, min, max)
PST_VERIFY_UINT_BUFFER_IN_RANGE[_MSG](buffer, numel, sz, min, max)
PST_ASSUME_UINT_BUFFER_IN_RANGE[_MSG](buffer, numel, sz, min, max)
PST_ASSERT_FLT_BUFFER_IN_RANGE[_MSG](buffer, numel, sz, min, max)
PST_VERIFY_FLT_BUFFER_IN_RANGE[_MSG](buffer, numel, sz, min, max)
PST_ASSUME_FLT_BUFFER_IN_RANGE[_MSG](buffer, numel, sz, min, max)