Defining the undefinedness of C

Chris Hathhorn, Chucky Ellison, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We present a "negative" semantics of the C11 language-a semantics that does not just give meaning to correct programs, but also rejects undefined programs. We investigate undefined behavior in C and discuss the techniques and special considerations needed for formally specifying it. We have used these techniques to modify and extend a semantics of C into one that captures undefined behavior. The amount of semantic infrastructure and effort required to achieve this was unexpectedly high, in the end nearly doubling the size of the original semantics. From our semantics, we have automatically extracted an undefinedness checker, which we evaluate against other popular analysis tools, using our own test suite in addition to a third-party test suite. Our checker is capable of detecting examples of all 77 categories of core language undefinedness appearing in the C11 standard, more than any other tool we considered. Based on this evaluation, we argue that our work is the most comprehensive and complete semantic treatment of undefined behavior in C, and thus of the C language itself.

Original languageEnglish (US)
Title of host publicationPLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsSteve Blackburn, David Grove
PublisherAssociation for Computing Machinery
Pages336-345
Number of pages10
ISBN (Electronic)9781450334686
DOIs
StatePublished - Jun 3 2015
Event36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015 - Portland, United States
Duration: Jun 13 2015Jun 17 2015

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Volume2015-June

Other

Other36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015
CountryUnited States
CityPortland
Period6/13/156/17/15

Keywords

  • C11
  • K framework
  • Programming language semantics
  • Undefined behavior

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Defining the undefinedness of C'. Together they form a unique fingerprint.

Cite this