Appendix F

Main differences between eCv in C'90 or C'99 mode and MISRA-C

Here are lists of the main differences between the C subset accepted by eCv and MISRA-C. Numbers in brackets are the corresponding MISRA rule numbers.

MISRA-C 2004 guidelines 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 55 MISRA-C 2004 rules in full and a further 16 rules in part. Future versions of eCv may support additional MISRA compliance checks.

Here are the MISRA-C 2004 rules that eCv allows to be violated without generating a warning or error message, when the compiler type is set to C90 and MISRA-C 2004 checking has been enabled in the project settings.

• eCv does not fully enforce rule 1.1 because it supports a few language extensions, such as inline functions, long long int type, and the syntax used by many embedded C compilers to place variables at particular addresses.
• 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).
• 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 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:

1. 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.
2. 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-C 2004 guidelines

• 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 any part of a conditional expression 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.

MISRA-C 2012 guidelines not fully enforced by eCv

The MISRA-C 2012 standard has 16 directives and 143 rules constraining how the C language may be used. Compliance with most rules can in principle be checked by source code analysis, with formal verification needed in some cases. Compliance with some of the directives can also be partially checked by source code analysis and formal verification, although in most cases additional information is needed. eCv currently checks 68 MISRA-C 2012 rules in full, and a further 6 rules and one directive in part. Future versions of eCv may support additional MISRA compliance checks.

Here are the MISRA-C 2012 directives and rules that eCv allows to be violated without generating a warning or error message, when the compiler type is set to C90 or C99 and MISRA-C 2012 checking has been enabled in the project settings.

• Directives 1.1, 2.1, 3.1, 4.2 are outside the scope of formal verification
• The eCv verifier enforces directive 4.1 in respect of integer arithmetic overflow, pointer arithmetic, array bound errors, function parameters (provided the functions are specified with the correct preconditions) and pointer dereferencing. It does not verify absence of overflow of floating point computations. eCv does not support dynamic memory.
• eCv enforces rule 1.1 in respect of syntax (apart from the extensions supported by eCv) and constraints, but not in respect of implementation limits.
• eCv supports a small number of common language extensions (rule 1.2)
• When code is unreachable, the eCv verifier will often warn about it by way of a "given false" message, but this is not guaranteed (rules 2.1 and 2.2)
• eCv does not check rules 2.3, 2.4, 2.5, 2.6, 2.7
• eCv does not check rule 3.2
• eCv does not check rule 4.1
• eCv does not check rules 5.1, 5.2
• eCv does not check rule 5.4. The eCv preprocessor considers all characters in a macro name to be significant.
• eCv does not check rules 5.5, 5.8, 5.9
• eCv does not check rule 7.1
• eCv does not check rules 8.4, 8.5, 8.6, 8.7, 8.9, 8.10, 8.12, 8.13, 8.14
• eCv does not support C99 designated initializers, therefore rules 9.4, 9.5 are not applicable
• eCv does not check rules 10.6, 10.7, 10.8
• eCv does not check rule 11.9
• eCv enforces rule 12.1 only partially, for example in most cases it does not warn if an operand of a Boolean operator is not parenthesized
• eCv does not check rule 12.3
• eCv does not check rules 13.3, 13.4, 13.5
• eCv does not check rules 14.1, 14.2, 14.3
• eCv does not check rules 15.1, 15.4, 15.5
• eCv does not fully enforce rule 16.3 because it allows a switch-case to be terminated by a return- or continue-statement
• eCv does not fully enforce rule 17.2 because it allows a function to be directly recursive if a recursion variant was specified, and does not check for indirect calls
• eCv does not check rules 17.7, 17.8
• eCv allows and understands pointer arithmetic (rule 18.4)
• eCv does not check rules 18.5, 18.6
• eCv does not check rule 19.2, however it requires that unions are used only for the purpose of storing different values at different times, not for performing type conversions
• eCv does not check rules 20.1, 20.2, 20.7, 20.8, 20.10, 20.11, 20.12
• eCv checks rule 21.1 in respect of #define but not in respect of #undef
• eCv does not check the remaining rules in section 21
• eCv does not check the section 22 rules

Notes:

1. The commenting rules (3.x) and preprocessor rules (20.x) are only checked if you are using eCv's own preprocessor, not if you are using your compiler's preprocessor.
2. Compliance with some rules 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-C 2012 guidelines

• The essential type of an enumeration constant or a variable of enumeration type is always that type (not int), even if the type is an anonymous enum type.
• 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

MISRA and MISRA-C are registered trademarks of MIRA Limited.