Appendix G

Main differences between eCv C and MISRA-C 2004

Here is a list of the main differences between the language accepted by eCv in C90 mode and MISRA-C 2004. Numbers in brackets are the corresponding MISRA rule numbers.

MISRA rules not fully enforced by eCv

The MISRA-C 2004 standard has 141 rules constraining how the C language may be used. Compliance with about 128 of these rules can in principle be checked by source code analysis, with formal verification needed in the case of a few rules. eCv currently checks 52 MISRA rules in full and 16 rules in part. Future versions of eCv may support additional MISRA compliance checks.

The following lists the MISRA rules that eCv allows to be violated without generating a warning or error message.

eCv does not fully enforce rule 1.1 because it supports a few language extensions, such as inline functions, long long int type, and HiTech C compiler placement syntax for variables.
Rules 1.3, 1.4 and 1.5 are outside the scope of source code static checking.
eCv does not enforce rule 2.1.
eCv permits comments introduced by // (2.2).
eCv does not enforce rule 2.4.
The documentation rules (3.x) are outside the scope of source code static checking. However, the behaviour of integer division is included when specifying the compiler/platform behaviour (3.3).
eCv does not enforce rules 5.4, 5.5, 5.6 and 5.7.
eCv enforces rule 6.1 and 6.2 to the extent that conversions in either direction between other integral types and plain char must be made explicit.
eCv does not enforce rule 6.3.
eCv does not require prototypes for functions whose definitions are visible at each place where they are called (8.1).
eCv permits objects to be defined in header files, in particular inline function declarations (8.5).
eCv does not enforce rules 8.6, 8.7, 8.8, 8.9, 8.10, 8.11 or 8.12.
eCv does not enforce rule 9.3.
eCv enforces part (a) of rules 10.1 and 10.2 but not parts (b), (c) or (d).
eCv does not enforce rules 10.3, 10.4 or 10.5.
eCv does not enforce rules 12.1, 12.4, 12.5 or 12.10.
eCv cannot enforce rule 12.11 because it depends on detailed knowledge of the behaviour of the compiler you will be using. Wrap-around will not occur when using the eCv preprocessor.
eCv does not enforce rule 12.13.
eCv allows assignment-expressions to be used within expressions yielding a Boolean value (13.1), provided that an assignment-expression is not used where a Boolean value is required. For example, "(a = b) && c" is forbidden, but "(a = b) == 0" is permitted.
eCv allows floating point expressions to be tested for equality and inequality (13.3).
eCv treats a for-loop as if is were an equivalent while-loop, therefore it does not place additional restrictions on the expressions in a for-loop header (13.4, 13.5) or on modifying for-loop variables (13.6).
eCv does not prohibit Boolean operations whose results are invariant, however they will typically lead to "given false" warnings during verification, indicating unreachable code (13.7).
eCv does not guarantee to detect unreachable code (14.1), however it will typically lead to "given false" warnings during verification.
eCv does not check that a non-null statement either has a side effect or causes control flow to change (14.2).
eCv does not check rule 14.3. You can use pass to introduce a null statement explicitly.
eCv supports continue (14.5).
eCv allows multiple break statements in a loop (14.6).
eCv allows multiple return statements in a function (14.7).
An if..else if.. construct does not need to have a final else clause (14.10).
A case clause in a switch statement need not end in "break;" if it cannot fall through, for example if it ends in an if-statement for which both branches end in a jump statement (15.2).
eCv does not enforce rule 15.5.
A switch statement need not have a default label; and if it does have a default label, it need not be the last case (15.3).
eCv only allows recursive functions if a recursion variant is declared (16.2).
eCv does not enforce rule 16.3.
eCv treats a function or function prototype declared with an empty parameter list as having no parameters; it does not insist on the parameter list being declared as "(void)" (16.5).
eCv does not warn about pointer parameters that could have been declared const but were not (16.7).
eCv does not enforce rule 16.9.
eCv does not check that error information returned by a function is tested, provided the specification is met (16.10).
eCv permits pointer arithmetic on array pointers (17.4), however verification of pointer arithmetic typically requires additional annotation, therefore pointer arithmetic should be avoided as far as possible.
eCv does not place a limit on pointer indirection, however compliance with the MISRA limit of 2 is recommended (17.5).
eCv does not enforce rule 17.6.
eCv permits unions, provided they are not used to convert between different types (18.4).
eCv does not enforce preprocessing rules 19.1, 19.2, 19.4, 19.5, 19.7, 19.9, 19.10, 19.13 or 19.15.
eCv partially enforces rule 20.1 but does not enforce the remaining library rules (20.x).

Notes:

The above assumes that the "Enable MISRA warnings" feature is turned on; otherwise, checks for a few MISRA rules are relaxed or disabled.
The commenting rules (2.x) and preprocessor rules (19.x) are only checked if you are using eCv's own preprocessor, not if you are using your compiler's preprocessor.
Compliance with rules 1.2, 12.2, 12.8, 17.2, 17.3 and 21.1 can only be ensured if verification is run and the verification conditions corresponding to these rules are successfully discharged by the theorem prover.

eCv rules that are stronger than the MISRA rules

eCv has a Boolean type bool. The underlying type of an operator expression in which the operator is a comparison or logical operator is bool. Implicit conversions between bool and other types other than 1-bit unsigned int bit fields generate warnings.
eCv has strongly-typed enumerations. The underlying type of an enumeration constant or a variable of enumeration type is that type, not int. Implicit conversions from enumeration types to int, long int and long long int do not generate warnings. Implicit conversions from integral to enumeration types do generate warnings.
Type wchar_t is treated as a separate type by eCv, not as a typedef for some integral type. It is treated in a similar way to plain char, i.e. all conversions between wchar_t and other types must be explicit.
Pointers to arrays much be qualified by the array keyword when they are declared.
Pointers that are allowed to take the null pointer value must be qualified by the null keyword when they are declared.
eCv will warn about conversions between different pointer types, except for conversions to void*.
eCv does not allow conditional expressions to have side effects.
eCv does not allow you to take the address of a member of a union, or of any part of a member of a union.
eCv does not allow you to use the sizeof operator with a character literal operand.

TOC