Consider environment pointers as unsafe (-stubbed-pointers-are-unsafe)

Specify that environment pointers can be unsafe to dereference unless constrained otherwise

Description

This option affects a Code Prover analysis only.

This option is not available for code generated from MATLAB® code or Simulink® models.

Specify that the verification must consider environment pointers as unsafe unless otherwise constrained. Environment pointers are pointers that can be assigned values outside your code.

Environment pointers include:

  • Global or extern pointers.

  • Pointers returned from stubbed functions.

    A function is stubbed if your code does not contain the function definition or you override a function definition by using the option Functions to stub (-functions-to-stub).

  • Pointer parameters of functions whose calls are generated by the software.

    A function call is generated if you verify a module or library and the module or library does not have an explicit call to the function. You can also force a function call to be generated with the option Functions to call (-main-generator-calls).

Set Option

Set the option using one of these methods:

  • Polyspace® user interface (desktop products only): In your project configuration, select the Verification Assumptions node and then select this option.

  • Polyspace Platform user interface (desktop products only): In your project configuration, on the Static Analysis tab, select the Run Time Errors > Verification Assumptions node and then select this option.

  • Command line and options file: Use the option -stubbed-pointers-are-unsafe. See Command-Line Information.

Why Use This Option

Use this option so that the verification makes more conservative assumptions about pointers from external sources.

If you specify this option, the verification considers that environment pointers can have a NULL value. If you read an environment pointer without checking for NULL, the Illegally dereferenced pointer check shows a potential error in orange. The message associated with the orange check shows the pointer can be NULL.

Settings

On

The verification considers that environment pointers can have a NULL value.

Off (default)

The verification considers that environment pointers:

  • Cannot have a NULL value.

  • Points within allowed bounds.

Tips

  • Enable this option during the integration phase. In this phase, you provide complete code for verification. Even if an orange check originates from external sources, you are likely to place protections against unsafe pointers from such sources. For instance, if you obtain a pointer from an unknown source, you check the pointer for NULL value.

    Disable this option during the unit testing phase. In this phase, you focus on errors originating from your unit.

  • If you are verifying code implementation of AUTOSAR runnables, Code Prover assumes that pointer arguments to runnables and pointers returned from Rte_ functions are not NULL. You cannot use this option to change the assumption. See Run Polyspace on AUTOSAR Code with Conservative Assumptions.

  • If you enable this option, the number of orange checks in your code might increase.

    Environment Pointers SafeEnvironment Pointers Unsafe

    The Illegally dereferenced pointer check is green. The verification assumes that env_ptr is not NULL and any dereference is within allowed bounds. The verification assumes that the result of the dereference is full range. For instance, in this case, the return value has the full range of type int.

      int func (int *env_ptr) {
      return *env_ptr;
  }

    The Illegally dereferenced pointer check is orange. The verification assumes that env_ptr can be NULL.

      int func (int *env_ptr) {
      return *env_ptr;
  }

    If you enable this option, the number of gray checks might decrease.

    Environment Pointers SafeEnvironment Pointers Unsafe

    The verification assumes that env_ptr is not NULL. The if condition is always true and the else block is unreachable.

      #include <stdlib.h>
  int func (int *env_ptr) {
      if(env_ptr!=NULL)
	         return *env_ptr;
      else
	         return 0;
  }

    The verification assumes that env_ptr can be NULL. The if condition is not always true and the else block can be reachable.

      #include <stdlib.h>
  int func (int *env_ptr) {
      if(env_ptr!=NULL)
	         return *env_ptr;
      else
	         return 0;
  }

  • Instead of considering all environment pointers as safe or unsafe, you can individually constrain some of the environment pointers. See the description of Initialize Pointer in External Constraints for Polyspace Analysis.

    When you individually constrain a pointer, you first specify an Init Mode, and then specify through the Initialize Pointer option whether the pointer is Null, Not Null, or Maybe Null. Depending on the Init Mode, you can either override the global specification for all environment pointers or not.

    • If you set the Init Mode of the pointer to INIT or PERMANENT, your selection for Initialize Pointer overrides your specification for this option. For instance, if you specify Not NULL for an environment pointer ptr, the verification assumes that ptr is not NULL even if you specify that environment pointers must be considered unsafe.

    • If you set the Init Mode to MAIN GENERATOR, the verification uses your specification for this option.

      For pointers returned from stubbed functions, the option MAIN GENERATOR is not available. If you override the global specification for such a pointer through the Initialize Pointer option in constraints, you cannot toggle back to the global specification without changing the Initialize Pointer option too.

  • If you disable this option, the verification considers that dereferences at all pointer depths are valid.

    For instance, all the dereferences are considered valid in this code:

    int*** stub(void);

void func2() {
        int ***ptr = stub();
        int **ptr2 = *ptr;
        int *ptr3 = *ptr2;
}

Command-Line Information

Parameter: -stubbed-pointers-are-unsafe
Default: Off
Example (Code Prover): polyspace-code-prover -sources file_name -stubbed-pointers-are-unsafe
Example (Code Prover Server): polyspace-code-prover-server -sources file_name -stubbed-pointers-are-unsafe

Version History

Introduced in R2016b

See Also

Topics