-code-behavior-specifications

Description

-code-behavior-specifications file allows you to associate certain behaviors with elements of your code and modify the results of checks on those elements. Here, file associates specific behaviors to code elements such as functions, and can be in one of two formats:

An XML file.
You can only specify a single XML file as argument. A sample template file code-behavior-specifications-template.xml shows the XML syntax. The file is in polyspaceroot\polyspace\verifier\cxx\ where polyspaceroot is the Polyspace^® installation folder.
A Datalog (.dl) file.
You can specify multiple Datalog files as comma-separated arguments.

Specify an absolute path or a relative path to the XML file or Datalog files. For example, say a Datalog file myFile.dl is located in the folder C:\CodeBehaviorSpec and your current folder is C:\myScript. You can specify the absolute path to the file at the command line:

polyspace-bug-finder ... -code-behavior-specification "C:\CodeBehaviorSpec\myFile.dl"

Alternatively, specify a path that is relative to the current folder:

polyspace-bug-finder ... -code-behavior-specification "..\CodeBehaviorSpec\myFile.dl"

The XML and Datalog format support different code behaviors. For more information, see:

Modify Bug Finder Checkers Through Code Behavior Specifications
Modify Code Prover Run-Time Checks Through Code Behavior Specifications (Polyspace Code Prover)

For instance, you can:

Map your library functions to corresponding standard functions that Polyspace recognizes. Mapping to standard library functions can help with precision improvement or automatic detection of new threads.
Specify that a function has a special behavior or must be subjected to special checks.
For instance, you can specify that a function must only take addresses of initialized variables as arguments, or that a function must not be used altogether.

You can specify this option in the user interface of the Polyspace desktop products, at the command line or in IDE-s:

If you run verification from the command line, specify the absolute path to the XML files or path relative to the folder from which you run the command.
If you run verification from the user interface (desktop products only), in the Other field, specify the option along with an absolute path to the XML or the path relative to the location of your Polyspace project. See Other.
If you use Polyspace as You Code extensions in IDEs, enter this option in an analysis options file. See options file.

A report generated from the analysis results only show the use of this option and not the details of which behaviors were associated with code elements.

Examples

Specify Mapping to Standard Function

You can adapt the sample mapping XML file provided with your Polyspace installation and map your function to a standard function.

Suppose the default verification produces an orange User assertion (Polyspace Code Prover) check on this code:

double x = acos32(1.0);  
assert(x <= 2.0);

Suppose you know that the function acos32 behaves like the function acos and the return value is 0. You expect the check on the assert statement to be green. However, the verification considers that acos32 returns any value in the range of type double because acos32 is not precisely analyzed. The check is orange. To map your function acos32 to acos:

Copy the file code-behavior-specifications-template.xml from polyspaceroot\polyspace\verifier\cxx\ to another location, for instance, "C:\Polyspace_projects\Common\Config_files". Change the write permissions on the file.
To map your function to a standard function, modify the contents of the XML file. To map your function acos32 to the standard library function acos, change the following code:
```
<function name="my_lib_cos" std="acos"> </function>
```
To:
```
<function name="acos32" std="acos"> </function>
```

Specify the location of the file for verification:

Code Prover:

polyspace-code-prover -code-behavior-specifications "C:\Polyspace_projects\Common\Config_files\code-behavior-specifications-template.xml"

Code Prover Server:

polyspace-code-prover-server -code-behavior-specifications "C:\Polyspace_projects\Common\Config_files\code-behavior-specifications-template.xml"

Specify Mapping to Standard Function with Argument Remapping

Sometimes, the arguments of your function do not map one-to-one with arguments of the standard function. In those cases, remap your function argument to the standard function argument. For instance:

__ps_lookup_table_clip:
This function specific to Polyspace takes only a look-up table array as argument and returns values within the range of the look-up table. Your look-up table function might have additional arguments besides the look-up table array itself. In this case, use argument remapping to specify which argument of your function is the look-up table array.
For instance, suppose a function my_lookup_table has the following declaration:
```
double my_lookup_table(double u0, const real_T *table,
                                     const double *bp0);
```
The second argument of your function my_lookup_table is the look-up table array. In the file code-behavior-specifications-template.xml, add this code:
```
<function name="my_lookup_table" std="__ps_lookup_table_clip">
    <mapping std_arg="1" arg="2"></mapping>
</function>
```
When you call the function:
```
res = my_lookup_table(u, table10, bp);
```
The verification interprets the call as:
```
res =__ps_lookup_table_clip(table10);
```
The verification assumes that the value of res lies within the range of values in table10.
Polyspace supports mapping these lookup tables to __ps_lookup_table_clip:
- integer to integer lookup tables: looks up values from a int* table and returns an int value
- integer to float lookup tables: looks up values from a int* table and returns a float value
- float to float lookup tables: looks up values from a float* table and returns a float value
__ps_meminit:
This function specific to Polyspace takes a memory address as the first argument and a number of bytes as the second argument. The function assumes that the bytes in memory starting from the memory address are initialized with a valid value. Your memory initialization function might have additional arguments. In this case, use argument remapping to specify which argument of your function is the starting address and which argument is the number of bytes.
For instance, suppose a function my_meminit has the following declaration:
```
     void my_meminit(enum InitKind k, void* dest, int is_aligned, unsigned int size);
```
The second argument of your function is the starting address, and the fourth argument is the number of bytes. In the file code-behavior-specifications-template.xml, add this code:
```
<function name="my_meminit" std="__ps_meminit">
    <mapping std_arg="1" arg="2"></mapping>
    <mapping std_arg="2" arg="4"></mapping>
</function>
```
When you call the function:
```
my_meminit(INIT_START_BY_END, &buffer, 0, sizeof(buffer));
```
The verification interprets the call as:
```
__ps_meminit(&buffer, sizeof(buffer));
```
The verification assumes that sizeof(buffer) number of bytes starting from &buffer are initialized.
memset: Variable number of arguments.
If your function has variable number of arguments, you cannot map it directly to a standard function without explicit argument remapping. For instance, say your function is declared as:
```
void* my_memset(void*, int, size_t, ...)
```
To map the function to the memset function, use the following mapping:
```
<function name="my_memset" std="memset">
    <mapping std_arg="1" arg="1"></mapping>
    <mapping std_arg="2" arg="2"></mapping>
    <mapping std_arg="3" arg="3"></mapping>
</function>
```

Effect of Mapping on Precision

These examples show the result of mapping certain functions to standard functions:

my_acos → acos:
If you use the mapping, the User assertion (Polyspace Code Prover) check turns green. The verification assumes that the return value of my_acos is 0.
- Before mapping:
```
double x = my_acos(1.0);  
assert(x <= 2.0);
```
- Mapping specification:
```
<function name="my_acos" std="acos">
</function>
```
- After mapping:
```
double x = my_acos(1.0);  
assert(x <= 2.0);
```
my_sqrt → sqrt:
If you use the mapping, the Invalid use of standard library routine (Polyspace Code Prover) check turns red. Otherwise, the verification does not check whether the argument of my_sqrt is nonnegative.
- Before mapping:
```
res = my_sqrt(-1.0);
```
- Mapping specification:
```
<function name="my_sqrt" std="sqrt"> 
</function>
```
- After mapping:
```
res = my_sqrt(-1.0);
```
my_lookup_table (argument 2) →__ps_lookup_table_clip (argument 1):
If you use the mapping, the User assertion (Polyspace Code Prover) check turns green. The verification assumes that the return value of my_lookup_table is within the range of the look-up table array table.
- Before mapping:
```
double table[3] = {1.1, 2.2, 3.3}
.
.
double res = my_lookup_table(u, table, bp);
assert(res >= 1.1 && res <= 3.3);
```
- Mapping specification:
```
<function name="my_lookup_table" std="__ps_lookup_table_clip">
    <mapping std_arg="1" arg="2"></mapping>
</function>
```
- After mapping:
```
double table[3] = {1.1, 2.2, 3.3}
.
.
res_real = my_lookup_table(u, table9, bp);
assert(res_real >= 1.1 && res_real <= 3.3);
```
my_meminit →__ps_meminit:
If you use the mapping, the Non-initialized local variable (Polyspace Code Prover) check turns green. The verification assumes that all fields of the structure x are initialized with valid values.
- Before mapping:
```
struct X {
  int field1;
  int field2;
};
.
.
struct X x;
my_meminit(&x, sizeof(struct X));
return x.field1;
```
- Mapping specification:
```
<function name="my_meminit" std="__ps_meminit">
     <mapping std_arg="1" arg="1"></mapping>
     <mapping std_arg="2" arg="2"></mapping>
</function>
```
- After mapping:
```
struct X {
  int field1 ;
  int field2 ;
};
.
.
struct X x;
my_meminit(&x, sizeof(struct X));
return x.field1;
```
my_meminit →__ps_meminit:
If you use the mapping, the Non-initialized local variable (Polyspace Code Prover) check turns red. The verification assumes that only the field field1 of the structure x is initialized with valid values.
- Before mapping:
```
struct X {
  int field1 ;
  int field2 ;
};
.
.
struct X x;
my_meminit(&x, sizeof(int));
return x.field2;
```
- Mapping specification:
```
<function name="my_meminit" std="__ps_meminit">
</function>
```
- After mapping:
```
struct X {
  int field1 ;
  int field2 ;
};
.
.
struct X x;
my_meminit(&x, sizeof(int));
return x.field2;
```

Limitations

You can map your custom functions to similar standard library functions using the option -code-behavior-specifications, subject to the following constraints:

Your custom function must have the same number of arguments as the standard library function or more. Make sure that every argument of the standard library function is mapped to an argument of the custom function.
The mapped function arguments must have compatible data types. Likewise, the custom function must have a return type that is compatible with the standard library function. For instance:
- An integer type (char, int, etc.) is not compatible with a floating point type (float, double, etc.)
- A fundamental type is not compatible with a structure or enumeration.
- A pointer type is not compatible with a non-pointer type.

Syntax

Description

Examples

Specify Mapping to Standard Function

Specify Mapping to Standard Function with Argument Remapping

Effect of Mapping on Precision

Limitations

Version History

See Also

Topics