Mapping to Standard Function for Precision Improvement

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <functions>
        <function name="custom_function" std="std_function"> 
        </function>
    </functions>
</specifications>

Use this entry in the XML file to reduce the number of false negatives in a Bug Finder analysis. Sometimes, the analysis does not model certain kinds of functions precisely because of inherent limitations in static verification. In those cases, if you find a standard function that is a close analog of your function, use this mapping. Though your function itself is not analyzed, the analysis is more precise at the locations where you call the function. For instance, if the analysis cannot model your function cos32 precisely and considers full range for its return value, map it to the cos function for a return value in [-1,1].

The analysis ignores the body of your function but emulates your function behavior in the following ways:

The functions that you can map to include:

If you run Code Prover, you can map to other functions to improve the verification precision. See Modify Code Prover Run-Time Checks Through Code Behavior Specifications (Polyspace Code Prover).

See also Extend Bug Finder Checkers for Standard Library Functions to Custom Libraries.

Mapping to Standard Function for Concurrency Detection

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <functions>
        <function name="custom_function" std="std_function"> 
        </function>
    </functions>
</specifications>

Use this entry in the XML file for automatic detection of thread-creation functions and functions that begin and end critical sections. Polyspace supports automatic detection for certain families of multitasking primitives only. Extend the support using this XML entry.

If your thread-creation function, for instance, does not belong to one of the supported families, map your function to a supported concurrency primitive.

See Extend Concurrency Defect Checkers to Unsupported Multithreading Environments.

Blocking Functions, Keywords or Macros

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <functions>
        <function name="my_func">
            <behavior name="FORBIDDEN_FUNC"/>
        </function>
    </functions>
</specifications>

Use this entry in the XML file to specify that a function my_func must not be used in your source code.

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <tokens>
        <token name="my_keyword" kind="keyword">
            <behavior name="FORBIDDEN_KEYWORD"/>
        </token>
    </tokens>
</specifications>

Use this entry in the XML file to specify that a keyword my_keyword must not be used in your source code.

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <token name="my_macro" kind="macro">
          <behavior name="FORBIDDEN_MACRO"/>
    </token>
</specifications>

Use this entry in the XML file to specify that a macro my_macro must not be used in your source code.

Note that you can use the * wildcard for functions and keywords (but not for macros). For instance, to forbid all functions whose names contain DEBUG, you can enter:

<function name="*DEBUG*">
      <behavior name="FORBIDDEN_FUNC"/>
</function>

<token name="DEFINED_.*" kind="macro" regex="true">
    <behavior name="FORBIDDEN_MACRO"/>
</token>

See Flag Deprecated or Unsafe Functions, Keywords, or Macros Using Bug Finder Checkers.

Extending Initialization Checks

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <functions>
        <function name="my_func">
            <check name=name="ARGUMENT_POINTS_TO_INITIALIZED_VALUE" arg="n/>
        </function>
    </functions>
</specifications>

Use this entry in the XML file to specify if the pointer argument to a function my_func must point to an initialized buffer. The number n specifies which argument must be checked for buffer initialization.

See Extend Checkers for Initialization to Check Function Arguments Passed by Pointers.

Modifying Global Behavior

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <global_scope>
        <parameter name="MAX_NUMBER_NESTED_LEVEL_CONTROL_FLOW" value="n1"/>
        <parameter name="MAX_NUMBER_NESTED_LEVEL_INCLUDES" value="n2"/>
        <parameter name="MAX_NUMBER_CONSTANT_IN_ENUMERATION" value="n3"/>
        <parameter name="MAX_NUMBER_MACROS_TRANSLATION_UNIT" value="n4"/>
        <parameter name="MAX_NUMBER_MEMBERS_IN_STRUCT" value="n5"/>
        <parameter name="MAX_NUMBER_NESTED_MEMBERS_IN_STRUCT" value="n6"/>
        <parameter name="NUMBER_SIGNIFICANT_CHARACTER_EXTERNAL_IDENTIFIER" value="n7"/>
        <parameter name="NUMBER_SIGNIFICANT_CHARACTER_INTERNAL_IDENTIFIER" value="n8"/>
    </global_scope>
</specifications>

Use the entries n1,..,n6 for the following parameters to specify limits on certain aspects of your program. The modifications affect the checking of MISRA C:2012 Rule 1.1.

Use the entries n7 and n8 to specify how many characters must be compared to determine if two identifiers as identical. The modifications affect the checking of Rules 5.x.

Specifying Real-Time Functions

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <functions>
        <function name="my_func">
            <behavior name="REAL_TIME_FUNC"/>
        </function>
    </functions>
</specifications>

Use this entry in the XML file to specify a function my_func as a real-time function See AUTOSAR C++14 Rule A18-5-7.

Specifying Functions that Manage Memory

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <functions>
        <function name="my_func">
            <behavior name="MANAGES_MEMORY"/>
        </function>
    </functions>
</specifications>

Use this entry in the XML file to specify a function my_func as a function that allocates or deallocates dynamic memory. See AUTOSAR C++14 Rule A18-5-7.

Specifying Functions that Handle Exceptions

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <functions>
        <function name="my_func">
            <behavior name="EXCEPTION_HANDLING"/>
        </function>
    </functions>
</specifications>

Use this entry in the XML file to specify a function my_func as a function that handles one or more exceptions. See AUTOSAR C++14 Rule A15-0-7.

Specifying Critical Data Members

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <members>
        <member name="my_critical_object" kind="variable">
            <behavior name="CRITICAL_DATA"/>
        </member>
    </members>
</specifications>

Use this entry in the XML file to specify the data member my_critical_object as critical. See Critical data member is not private.

You can specify multiple similarly-named data members in the list of critical data members using regular expressions. To use regular expressions, in addition to the attributes name and kind, you have to set an attribute regex to true.

For instance, to consider all member names starting with user as critical data members, enter:

<member name="user.*" kind="variable" regex="true">
    <behavior name="CRITICAL_DATA"/>
</member>

Datalog Example

Consider the following example. The function insertIntoDatabase() reads a string from standard input and uses the string in the construction of an SQL query.

#include <stdio.h>
#include <string.h>
#include <sqlite3.h>

void addToName(char *, char *);

// Function to insert names into database
void insertIntoDatabase(void)
{
    sqlite3* db;
    char query[256] = "";
    char partialName[256];
    char fullName[256];
    
    char* error_message;
    int nameLength;

    sqlite3_open("userCredentials.db", &db);

    fread(partialName, 1, 128, stdin);
    
    addToName(partialName, fullName); //Function with unknown semantics

    strcat(query, "INSERT INTO privatenames (name) VALUES ('");
    strcat(query, fullName);
    strcat(query, "');");

    // Possible SQL injection here
    if (sqlite3_exec(db, query, NULL, NULL, &error_message))
        {
            sqlite3_free(error_message);
        }
}

However, the defect checker SQL injection cannot find this defect because the function addToName() is not defined in this code and its semantics are not known. (In some cases, if the function is sufficiently complex, the analysis might lose track of a data flow from one function argument to another despite the function being defined.)

To help with the analysis, you can externally specify the semantics of the addToName() function using Datalog syntax. In a file with extension .dl, for instance bufferFlows.dl, enter the following:

.include "models/interfaces/taint.dl"

Taint.Basic.hasFlow("addToName", $InParameterDeref(0), $OutParameterDeref(1), "Source buffer copied to destination").

Specify the Datalog file as argument for the analysis option -code-behavior-specifications, for instance:

-code-behavior-specifications bufferFlows.dl

The two options that support Datalog file specification are:

Behaviors Supported by Datalog Format

The following checkers can be modified using code behavior specifications in Datalog format.

The following code behaviors can be specified to modify the checkers: