`unchecked_assert`

Constrain variable ranges for static analysis with Polyspace products

Syntax

unchecked_assert(condition);

Description

unchecked_assert(condition); is a function-like C/C++ macro that imposes a constraint on variable ranges for Polyspace^® analysis of the subsequent code. For instance, in the following example, when analyzing the return statement, Polyspace assumes that arg does not contain the value 0:

double reciprocal (int arg) {
      unchecked_assert(arg != 0);
      return 1.0/arg;
}

Since the macro is not part of the C/C++ language standard, to avoid compilation errors, enclose the macro in a preprocessor directive like this:

#ifdef POLYSPACE
   unchecked_assert(arg != 0);
#endif

When analyzing the code with Polyspace, specify the macro POLYSPACE as a defined preprocessor directive. For instance, at the command line, append the analysis option -D POLYSPACE. See Preprocessor definitions (-D). Enclosing the unchecked_assert macro in an preprocessor directive like this makes the macro visible to a Polyspace analysis but not during regular compilation.

A constraint specified through an unchecked_assert macro becomes part of the analysis assumptions. The analysis assumes the constraint and does not actually check if the constraint is true. If you want the constraint to be checked, instead of unchecked_assert, use the standard C debug macro assert.

Usage

Use the unchecked_assert macro to impose external constraints not directly supported through Polyspace analysis options such as Constraint setup (-data-range-specifications). When specifying external constraints, note the following:

Use unchecked_assert to specify preconditions on variables at the program boundary, in particular:
- Inputs to uncalled functions (when there is no main)
- Return values and modifiable parameters of undefined (stubbed) functions.
If you want to insert constraints in the middle of a program flow, use the standard C debug macro assert instead of unchecked_assert. Code Prover uses the User assertion check to determine if your constraints actually hold (in addition to imposing the constraint for the subsequent analysis).
Use unchecked_assert to specify only constraints that follow from actual external considerations. For instance, you can impose constraints to eliminate unphysical values of a physical quantity, such as temperature or efficiency ratio.

Examples

Impose Relations Between Inputs to Uncalled Functions

Consider the following example:

double getCoefficient(int item, int match)
{
    double coefficient = match/(match-item);
    return coefficient;
}

The function getCoefficient() has two apparently unrelated inputs: item and match. When analyzing the function in the absence of a callee, Code Prover analysis considers the possibility that:

The two variables might have the same value. As a result, the analysis shows a possible division by zero on the / operation.
The variables item and match might have opposite signs and arbitrarily large values allowed by their data types. As a result, the analysis shows a possible overflow on the - operation.

Suppose that you know from external requirements that:

The first parameter of getCoefficient() is positive.
The second parameter of getCoefficient() is greater than the first parameter.

You can enter unchecked_assert statements at the beginning of getCoefficient() to impose the external requirements.

double getCoeff(int item, int match)
{
    #ifdef POLYSPACE
            unchecked_assert(item > 0 && match > item);
    #endif
    
    double coefficient = match/(match-item);
    return coefficient;
}

If you analyze this example with the analysis option that defines the macro POLYSPACE and effectively activates the constraint, the analysis no longer shows the two possible errors. For more information on the option, see Preprocessor definitions (-D).

Impose Relations Between Parameters of Undefined Functions

Consider the following example:

int getAnItem();
void lookup(int item, int *match);

int main(char argc, char* argv[])
{
    int item = getAnItem(), match;
    lookup(item, &match);
    double coefficient = match/(match-item);
    return 0;
}

Both variables item and match are initialized with undefined functions, getAnItem() and lookup(). Since undefined functions are stubbed, a Code Prover analysis considers the possibility that:

The two variables might have the same value. As a result, the analysis shows a possible division by zero on the / operation.
The variables match and item might have opposite signs and arbitrarily large values allowed by their data types. As a result, the analysis shows a possible overflow on the - operation.

Suppose that you know from external requirements that:

The function getAnItem() returns a positive value.
The function lookup() writes a positive value to the second argument passed by pointer. The value written is greater than the value of the first argument.

You can enter dummy definitions of the getAnItem() and lookup() functions. Within the dummy definitions, you can use unchecked_assert statements to impose the external requirements.

int getAnItem();
void lookup(int item, int *match);

#ifdef POLYSPACE

// Function to initialize a variable with a random value
int getRandomValue();

// Dummy definition of getAnItem()
// Function returns a positive value
int getAnItem()
{
    int ret = getRandomValue();
    unchecked_assert(ret > 0);
    return ret;
}

// Dummy definition of lookup()
// Function writes its second argument
// With a positive value greater than first argument
void lookup(int item, int *match)
{
    *match = getRandomValue();
    unchecked_assert(*match > 0 && *match > item);
}
#endif

int main(char argc, char* argv[])
{
    int item = getAnItem(), match;
    lookup(item, &match);
    double coefficient = match/(match-item);
    return 0;
}

If you analyze this example with the analysis option that defines the macro POLYSPACE and effectively activates the dummy function definitions, the analysis no longer shows the two possible errors. For more information on the option, see Preprocessor definitions (-D).

Version History

Introduced in R2013b

unchecked_assert