Justify Coding Rule Violations Using Code Prover Checks

Coding rules are best practices that you observe for safe and secure code. Using the Polyspace^® coding rule checkers, you find instances in your code that violate a coding rule standard such as MISRA™ C:2023. If you run Code Prover, you also see results of checks that find run-time errors or prove their absence. In some cases, the two kinds of results can be used together for efficient review. For instance, you can use a green Code Prover check as rationale for not fixing a coding rule violation (justification). For instance:

• MISRA C:2012 Rule 9.1 and MISRA C:2023 Rule 9.1: The rule states that the value of an object with automatic storage duration shall not be read before it has been set. Use the results of a Non-initialized local variable (Polyspace Code Prover) check to justify the rule violations.

• MISRA C™:2004 Rule 13.7: The rule states that the Boolean operations whose results are invariant shall not be permitted. Use the results of an Unreachable code (Polyspace Code Prover) check to identify conditions that are always true or false.

MISRA checkers do not suppress rule violations even though corresponding green checks indicate that the violations have no consequence. You have the choice to do one of these:

• Strictly conform to the standard and fix the rule violations.

• Manually justify the rule violations using the green checks as rationale.

  Set a status such as No action planned to the result and enter the green check as rationale in the result comments. You can later filter justified results using that status.

The following sections show examples of situations where you can justify MISRA violations using green Code Prover checks.

Rules About Data Type Conversions

In some cases, implicit data type conversions are okay if the conversion does not cause an overflow.

In the following example, the line temp = var1 - var2; violates MISRA C:2023 Rule 10.3. The rule states that the value of an expression shall not be assigned to an object of a different essential type category. Here, the difference between two int variables is assigned to a char variable. You can justify this particular rule violation by using the results of a Code Prover Overflow (Polyspace Code Prover) check.

int func (int var1, int var2) {
    char temp;
    temp = var1 - var2;
    if (temp > 0)
        return -1;
    else
        return 1;
}

double read_meter1(void);
double read_meter2(void);

int main(char arg, char* argv[]) {
    int meter1 = (read_meter1()) * 10;
    int meter2 = (read_meter2()) * 999;
    int tol = 10;
    if((meter1 - meter2)> -tol && (meter1 - meter2) < tol)
        func(meter1, meter2);
    return 0;
}

Consider the rationale behind this rule. The use of implicit conversions between types can lead to unintended results, including possible loss of value, sign, or precision. For a conversion from int to char, a loss of sign or precision cannot happen. The only issue is a potential loss of value if the difference between the two int variables overflows.

Run Code Prover on this code. On the Source pane, click the = in temp = var1 - var2;. You see a green Overflow check. The green check indicates that the conversion from int to char does not overflow. You can use the green overflow check as rationale to justify the rule violation.

Rules About Pointer Arithmetic

Pointer arithmetic on nonarray pointers are okay if the pointers stay within the allowed buffer.

In the following example, the operation ptr += 1 violates MISRA C:2023 Rule 18.4. The rule is violated because the use of the operator += on a pointer type expression is not recommended.

#define NUM_RECORDS 3
#define NUM_CHARACTERS 6

void readchar(char);   

int main(int argc, char* argv[]) {
    char dbase[NUM_RECORDS][NUM_CHARACTERS] = { "r5cvx", "a2x5c", "g4x3c"};
    char *ptr = &dbase[0][0];
    for (int index = 0; index < NUM_RECORDS * NUM_CHARACTERS; index++) {
        readchar(*ptr);
        ptr += 1; //Violation of 18.4
    }
    return 0;
}

Consider the rationale behind this rule. After an increment, a pointer can go outside the bounds of an allowed buffer (such as an array) or even point to an arbitrary location. Pointer arithmetic is fine as long as the pointer points within an allowed buffer. You can justify this particular rule violation by using the results of a Code Prover Illegally dereferenced pointer (Polyspace Code Prover) check.

Run Code Prover on this code. On the Source pane, click the ++ in ptr++. Click the * on the operation readchar(*ptr). You see a green Illegally dereferenced pointer check. The green check indicates that the pointer points within allowed bounds when dereferenced.

You can use the green check to justify the rule violation.