Justify Coding Rule Violations Using Code Prover Checks

Coding rules are good 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™. 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).

If you run MISRA checking in Code Prover, some of the checkers use Code Prover static analysis under the hood to find MISRA violations. The MISRA checker in Code Prover is more rigorous compared to Bug Finder because Code Prover keeps precise track of the data and control flow in your code. For instance:

MISRA C:2012 Rule 9.1 (Polyspace Code Prover): The rule states that the value of an object with automatic storage duration shall not be read before it has been set. Code Prover uses the results of a Non-initialized local variable (Polyspace Code Prover) check to determine the rule violations.
MISRA C™:2004 Rule 13.7: The rule states that the Boolean operations whose results are invariant shall not be permitted. Code Prover uses the results of an Unreachable code (Polyspace Code Prover) check to identify conditions that are always true or false.

In some other cases, the 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:2012 Rule 10.3 (Polyspace Code Prover). 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 the expected violation of MISRA C:2012 Rule 10.3, but also a green Overflow check.

The Result Details pane shows both an overflow and a violation of MISRA C:2012 Rule 10.3.

The green check indicates that the conversion from int to char does not overflow.

The Result Details pane shows that the conversion operation from int32 to int8 type 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++ violates MISRA C:2004 Rule 17.4. The rule states that array indexing shall be the only allowed form of pointer arithmetic. Here, a pointer that is not an array is incremented.

#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++;
    }
    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++. You see the expected violation of MISRA C:2004 Rule 17.4.

The Result Details pane shows a violation of MISRA C:2004 Rule 17.4.

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.

The Result Details pane shows that the pointer 'ptr' is dereferenced within its bounds. The pointer is not null and pointers to 1 byte at offset [0 ..17] in a buffer of 18 bytes, so is within bounds.

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