Defining the undefinedness of C11 : practical semantics-based program analysis

Field of study: Computer science.|Dr. William L. Harrison, Dissertation Supervisor.|Includes vita."December 2017."[ACCESS RESTRICTED TO THE UNIVERSITY OF MISSOURI AT AUTHOR'S REQUEST.] This thesis extends the work of Ellison and Ros,u [13, 12] but focuses on the "negative" semantics of the C11 language--the semantics required to not just give meaning to correct programs, but also to reject undefined programs. We investigate undefined behavior in C and discuss the techniques and special considerations needed to formally specify it. Using these techniques, we have modified and extended 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 more than tripling the size of the original semantics. From our semantics, we automatically extract kcc, a tool for checking realworld C programs for undefined behavior and other common programmer mistakes. Previous versions of this tool were used primarily for testing the correctness of the semantics, but we have improved it into a tool for doing practical analysis of real C programs. It beats many similar tools in its ability to catch a broad range of undesirable behaviors. We demonstrate this with comparisons based on our own test suite in addition to third-party benchmarks. 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.Includes bibliographical references (pages 143-149)