Skip to Main content Skip to Navigation
Conference papers

A Precise and Abstract Memory Model for C Using Symbolic Values

Frédéric Besson 1 Sandrine Blazy 1 Pierre Wilke 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Real life C programs are often written using C dialects which, for the ISO C standard, have undefined behaviours. In particular, according to the ISO C standard, reading an uninitialised variable has an undefined behaviour and low-level pointer operations are implementation defined. We propose a formal semantics which gives a well-defined meaning to those behaviours for the C dialect of the CompCert compiler. Our semantics builds upon a novel memory model leveraging a notion of symbolic values. Symbolic values are used by the semantics to delay the evaluation of operations and are normalised lazily to genuine values when needed. We show that the most precise normalisation is computable and that a slightly relaxed normalisation can be efficiently implemented using an SMT solver. The semantics is executable and our experiments show that the enhancements of our semantics are mandatory to give a meaning to low-levels idioms such as those found in the allocation functions of a C standard library.
Document type :
Conference papers
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download
Contributor : Frédéric Besson <>
Submitted on : Wednesday, December 10, 2014 - 2:54:16 PM
Last modification on : Tuesday, December 8, 2020 - 9:50:36 AM
Long-term archiving on: : Wednesday, March 11, 2015 - 11:15:14 AM


Files produced by the author(s)



Frédéric Besson, Sandrine Blazy, Pierre Wilke. A Precise and Abstract Memory Model for C Using Symbolic Values. 12th Asian Symposium on Programming Languages and Systems (APLAS 2014), 2014, Singapore, Singapore. pp.449 - 468, ⟨10.1007/978-3-319-12736-1_24⟩. ⟨hal-01093312⟩



Record views


Files downloads