, The resources, given as string literals, are either processor register names or the special resources "memory" and "cc", denoting unpredictable changes to the memory and the processor's condition codes, respectively. CompCert always assumes that inline assembly can modify memory and condition codes in unpredictable ways, even if the "memory" and "cc" clobbers are not specified. The register names are case-insensitive and depend on the target processor, as follows: Processor Register names ARM integer registers

, MISRA-C: 2004-Guidelines for the use of the C language in critical systems, Motor Industry Software Reliability Association, 2004.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development-Coq'Art: The Calculus of Inductive Constructions, EATCS Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

E. Eide and J. Regehr, Volatiles are miscompiled, and what to do about it, Proceedings of the 8th ACM & IEEE International conference on Embedded software, pp.255-264, 2008.
DOI : 10.1145/1450058.1450093

URL : http://www.cs.utah.edu/~regehr/papers/emsoft08-preprint.pdf

, AbsInt Angewandte Informatik GmbH. AbsInt Advanced Analyzer

, International standard ISO/IEC 9899:1999, Programming languages-C, 1999.

, ISO. International standard ISO/IEC 9899:2011, Programming languages-C, 2011.

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00415861

X. Leroy, A formally verified compiler back-end, Journal of Automated Reasoning, vol.43, issue.4, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4

URL : https://hal.archives-ouvertes.fr/inria-00360768

J. Mccarthy and J. Painter, Correctness of a compiler for arithmetical expressions, In Mathematical Aspects of Computer Science, vol.19, pp.33-41, 1967.

R. Milner and . Weyrauch, Proving compiler correctness in a mechanized logic, Proc. 7th Annual Machine Intelligence Workshop, pp.51-72, 1972.

C. Benjamin, A. Pierce, C. Azevedo-de-amorim, M. Casinghino, M. Gaboardi et al., C?at?alinC?at?C?at?alin Hri¸tcuHri¸tcu, Vilhelm Sjöberg, and Brent Yorgey. Software Foundations. Electronic textbook, 2017.

, IEEE standard for floating-point arithmetic, IEEE Computer Society, pp.754-2008, 2008.

X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and understanding bugs in C compilers, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp.283-294, 2011.
DOI : 10.1145/2345156.1993532

URL : http://www.stanford.edu/class/cs343/resources/finding-bugs-compilers.pdf