Main Content

Inline (-inline)

Specify functions that must be cloned internally for each function call

Description

This option affects a Polyspace® Code Prover™ analysis only.

Specify the functions that the verification must clone internally for each function call.

Set Option

User interface, in desktop products only: In your project configuration, the -inline option is available on the Scaling node.

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

Command line and options file: Use the -inline option. See Command-Line Information.

Why Use This Option

You use the -inline to internally clone a function for each function call. Doing so might reduce the complexity of the analysis in Polyspace Code Prover. Consider this code:

void foo(int* p);
void bar(){
	int* intP, intP2;
	foo(intP);
	foo(intP2)
}
In this code, Polyspace analyzes the functions foo() and bar(). When the option -inline Is not specified, the analysis keeps track of three objects: the pointers intP, intP2, and the parameter p. If you specify the option -inline, Polyspace internally clones foo for each function call. The code effectively becomes:
void foo_clone1(int* p);
void foo_clone2(int* p);
void bar(){
	int* intP, intP2;
	foo_clone1(intP);
	foo_clone2(intP2)
}
Analyzing the function foo_clone1() requires Polyspace to keep track of only two objects, intP and p, instead of three objects. The same is true for the function foo_clone2(). By using -inline, you reduce the complexity of the analysis and increase the amount of code to analyze.

Using -inline might reduce the complexity of your analysis while increasing the amount of code to analyze. This option might help you resolve scaling issues in specific situations. Technical Support might ask you to use this option for certain functions. Using this option changes the meaning of the colors of Polyspace Code Prover checks. See Settings.

Avoid using this option to distinguish between the Code Prover check colors in the different calls to the same function. Instead, use the option Sensitivity context (-context-sensitivity).

Settings

No Default

Enter function names or choose from a list.

  • Click to add a field and enter the function name.

  • Click to list functions in your code. Choose functions from the list.

The verification internally clones the function for each call. For instance, if you specify the function func for inlining and call func twice, the software internally creates two copies of func for verification.

However, for each run-time check in the function body, you see only one color in your verification results. The semantics of the check color differ from the normal specification.

Check TypeResult color without the option -inlineResult color with the option -inline
Orange checks If a function is called twice and an operation causes a definite error in one of the calls, the check color is orange.If a function is called twice and an operation causes a definite error in one of the calls, the check color is dark orange. The check is shown with an orange exclamation mark in the results list.
Gray checks If a function is called twice and an if statement branch is unreachable in one of the calls, the branch does not appear gray. If a function is called twice and an if statement branch is unreachable in one of the calls, the branch appears gray.

Below each check in an inlined function, you see information specific to each calling context. For instance, if an orange exclamation point appears next to Division by zero occurs because a specific function call leads to a definite division by zero, you can identify the call along with values resulting from that call.

Polyspace results for inlined functions

Do not use this option to understand results. Use this option only if a certain function causes scaling issues.

Tips

  • Choose functions to inline based on hints provided by the alias verification.

  • Do not use this option for entry point functions, including main.

  • Using this option can increase the number of gray Unreachable code checks.

    For example, in the following code, if you enter max for Inline, two Unreachable code checks appear for each call to max.

    int max(int a, int b) {
  return a > b ? a : b;
} 

void main() {
  int i=3, j=1, k;
  k=max(i,j);
  i=0;
  k=max(i,j);
}

  • If you use the keyword inline before a function definition, place the definition in a header file and call the function from multiple source files, the result is the same as using the option Inline.

  • For C++ code, this option applies to all overloaded methods of a class.

Command-Line Information

Parameter: -inline
Value: function1[,function2[,...]]
No Default
Example (Code Prover): polyspace-code-prover -sources file_name -inline func1,func2
Example (Code Prover Server): polyspace-code-prover-server -sources file_name -inline func1,func2

See Also

Topics