Ignore assembly code (-ignore-assembly-code)

Specify that assembly instructions in C/C++ code cannot modify C/C++ variables

Since R2023a

Description

This option affects a Code Prover analysis only.

Enable an analysis mode that ignores assembly instructions in C/C++ code. In this mode, the analysis assumes that assembly instructions in a C/C++ function cannot modify local variables of the function.

Set Option

User interface (desktop products only): In your project configuration, the option is available on the analysis Assumptions node.

User interface (Polyspace Platform, desktop products only): In your project configuration, the option is on the Run Time Errors tab on the Verification Assumptions node.

Command line and options file: Use the option -ignore-assembly-code. See Command-Line Information.

Why Use This Option

Use this option to reduce orange checks from overapproximations around assembly instructions in C/C++ code.

By default, Code Prover makes the conservative assumption that following assembly instructions in a function, local variables can take any value allowed by their data types. This assumption can lead to many orange checks following assembly instructions. If you use assembly instructions primarily for no-ops such as introducing delays or for loading global variables, you can enable an analysis mode that ignores the assembly instructions.

Settings

On

The analysis considers that assembly instructions in a function cannot modify local variables of the function. Use this option if assembly instructions in your project do not modify local variables of a function.

Consider these examples:

• The analysis assumes that the assembly instructions cannot modify the local variable val1. Therefore, the results show a red Non-initialized variable check when val1 is returned.

  int func(void) { 
      int val1; 
      asm("NOP");
      //Instructions that do not modify val1
      //...
      return val1; 
  }

• The analysis assumes that the assembly instructions cannot modify the local variables val1 and val2. Therefore, the results show a green Overflow check when the two variables are added.

  int func(void) { 
      int val1 = 0, val2 = 0; 
      asm("NOP");
      //Instructions that do not modify val1 and val2
      //...
      return (val1+val2); 
  }

Off (default)

The analysis considers that assembly instructions in a function can modify local variables of the function. Use this option if assembly instructions in your project can modify local variables of a function.

Consider these examples:

• The analysis assumes that the assembly instructions can potentially modify the local variable val1. Therefore, the results show an orange Non-initialized variable check when val1 is returned.

  int func(void) { 
      int val1; 
      asm("mov 4%0,%%eax"::"m"(val1));
      //Instructions that do not modify val1
      //...
      return val1; 
  }

• The analysis assumes that the assembly instructions can modify the local variables val1 and val2 (and write any possible value allowed by their data types). Therefore, the results show an orange Overflow check when the two variables are added.

  int func(void) { 
      int val1 = 0, val2 = 0; 
      asm("mov 4%0,%%eax"::"m"(val1));
      //Instructions that do not modify val1 and val2
      //...
      return (val1+val2); 
  }

Command-Line Information

Parameter: -ignore-assembly-code

Default: Off

Example (Code Prover): polyspace-code-prover -sources file_name -ignore-assembly-code

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -ignore-assembly-code

Version History

Introduced in R2023a