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.

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

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.

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


TOC   TOC

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

eCv Manual, Version 7.0, February 2017.
© 2017 Escher Technologies Limited. All rights reserved.