Defining the Undefinedness of C

From FSL
Revision as of 21:22, 26 February 2016 by Yzhng173 (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

PLDI'15

Defining the Undefinedness of C
Chris Hathhorn and Chucky Ellison and Grigore Rosu
PLDI'15, ACM, pp 336-345. 2015
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.
PDF, C Semantics, DOI, PLDI'15, BIB


Technical Report

Defining the Undefinedness of C
Chucky Ellison and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30780, April 2012
Abstract. This paper investigates undefined behavior in C and offers a few simple techniques for operationally specifying such behavior formally. A semantics-based undefinedness checker for C is developed using these techniques, as well as a test suite of undefined programs. The tool is evaluated against other popular analysis tools, using the new test suite in addition to a third-party test suite. The semantics-based tool performs at least as well or better than the other tools tested.
PDF, K, DOI, BIB

Personal tools
Namespaces

Variants
Actions
Navigation