{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:31Z","timestamp":1781238931055,"version":"3.54.1"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ERC","award":["ELVER 789108"],"award-info":[{"award-number":["ELVER 789108"]}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/K008528\/1"],"award-info":[{"award-number":["EP\/K008528\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"DARPA\/AFRL","award":["HR0011-18-C-0016,FA8750-10-C-0237"],"award-info":[{"award-number":["HR0011-18-C-0016,FA8750-10-C-0237"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>The semantics of pointers and memory objects in C has been a vexed question for many years. C values cannot be treated as either purely abstract or purely concrete entities: the language exposes their representations, but compiler optimisations rely on analyses that reason about provenance and initialisation status, not just runtime representations. The ISO WG14 standard leaves much of this unclear, and in some respects differs with de facto standard usage --- which itself is difficult to investigate.<\/jats:p>\n          <jats:p>In this paper we explore the possible source-language semantics for memory objects and pointers, in ISO C and in C as it is used and implemented in practice, focussing especially on pointer provenance. We aim to, as far as possible, reconcile the ISO C standard, mainstream compiler behaviour, and the semantics relied on by the corpus of existing C code. We present two coherent proposals, tracking provenance via integers and not; both address many design questions. We highlight some pros and cons and open questions, and illustrate the discussion with a library of test cases. We make our semantics executable as a test oracle, integrating it with the Cerberus semantics for much of the rest of C, which we have made substantially more complete and robust, and equipped with a web-interface GUI. This allows us to experimentally assess our proposals on those test cases. To assess their viability with respect to larger bodies of C code, we analyse the changes required and the resulting behaviour for a port of FreeBSD to CHERI, a research architecture supporting hardware capabilities, which (roughly speaking) traps on the memory safety violations which our proposals deem undefined behaviour. We also develop a new runtime instrumentation tool to detect possible provenance violations in normal C code, and apply it to some of the SPEC benchmarks. We compare our proposal with a source-language variant of the twin-allocation LLVM semantics proposal of Lee et al. Finally, we describe ongoing interactions with WG14, exploring how our proposals could be incorporated into the ISO standard.<\/jats:p>","DOI":"10.1145\/3290380","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":49,"title":["Exploring C semantics and pointer provenance"],"prefix":"10.1145","volume":"3","author":[{"given":"Kayvan","family":"Memarian","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Victor B. F.","family":"Gomes","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Brooks","family":"Davis","sequence":"additional","affiliation":[{"name":"SRI International, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stephen","family":"Kell","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexander","family":"Richardson","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robert N. M.","family":"Watson","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_24"},{"key":"e_1_2_2_4_1","volume-title":"ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings. 67\u201383","author":"Besson Fr\u00e9d\u00e9ric","year":"2015"},{"key":"e_1_2_2_5_1","volume-title":"ITP 2017, Bras\u00edlia, Brazil, September 26-29, 2017, Proceedings. 81\u201397","author":"Besson Fr\u00e9d\u00e9ric","year":"2017"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_2_2_7_1","volume-title":"Watson","author":"Chisnall David","year":"2016"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694367"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.09.061"},{"key":"e_1_2_2_11_1","volume-title":"VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings. 14\u201333","author":"Cuoq Pascal","year":"2017"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_2_2_14_1","unstructured":"FSF. 2018a. GNU Compiler Collection Torture Test Suite. https:\/\/github.com\/gcc- mirror\/gcc\/tree\/master\/gcc\/testsuite\/gcc. c- torture\/execute .  FSF. 2018a. GNU Compiler Collection Torture Test Suite. https:\/\/github.com\/gcc- mirror\/gcc\/tree\/master\/gcc\/testsuite\/gcc. c- torture\/execute ."},{"key":"e_1_2_2_15_1","unstructured":"FSF. 2018b. Using the GNU Compiler Collection (GCC) \/ 4.7 Arrays and pointers. https:\/\/gcc.gnu.org\/onlinedocs\/gcc\/ Arrays- and- pointers- implementation.html . Accessed 2018-10-22.  FSF. 2018b. Using the GNU Compiler Collection (GCC) \/ 4.7 Arrays and pointers. https:\/\/gcc.gnu.org\/onlinedocs\/gcc\/ Arrays- and- pointers- implementation.html . Accessed 2018-10-22."},{"key":"e_1_2_2_16_1","unstructured":"Matt Godbolt. 2017. Compiler Explorer. https:\/\/godbolt.org\/ .  Matt Godbolt. 2017. Compiler Explorer. https:\/\/godbolt.org\/ ."},{"key":"e_1_2_2_17_1","volume-title":"Huggins","author":"Gurevich Yuri","year":"1993"},{"key":"e_1_2_2_18_1","volume-title":"CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. 447\u2013453","author":"Guth Dwight","year":"2016"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737979"},{"key":"e_1_2_2_20_1","volume-title":"Dickey","author":"Huang Chin","year":"2018"},{"key":"e_1_2_2_21_1","unstructured":"Derek Jones. 1992. Applications POSIX.1 conformance testing. http:\/\/www.knosof.co.uk\/poschk.html . Presented at the EurOpen &amp; USENIX Spring 1992 Workshop\/Conference.  Derek Jones. 1992. Applications POSIX.1 conformance testing. http:\/\/www.knosof.co.uk\/poschk.html . Presented at the EurOpen &amp; USENIX Spring 1992 Workshop\/Conference."},{"key":"e_1_2_2_22_1","unstructured":"Derek M. Jones. 2009. The New C Standard: An Economic and Cultural Commentary. http:\/\/www.knosof.co.uk\/cbook\/ .  Derek M. Jones. 2009. The New C Standard: An Economic and Cultural Commentary. http:\/\/www.knosof.co.uk\/cbook\/ ."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064848"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738005"},{"key":"e_1_2_2_25_1","unstructured":"KCC. 2018. Example Test Suite. https:\/\/github.com\/kframework\/c- semantics\/tree\/master\/examples\/c .  KCC. 2018. Example Test Suite. https:\/\/github.com\/kframework\/c- semantics\/tree\/master\/examples\/c ."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814228.2814238"},{"key":"e_1_2_2_27_1","unstructured":"Krebbers and Wiedijk. 2012. N1637: Subtleties of the ANSI\/ISO C standard. http:\/\/www.open- std.org\/jtc1\/sc22\/wg14\/www\/ docs\/n1637.pdf .  Krebbers and Wiedijk. 2012. N1637: Subtleties of the ANSI\/ISO C standard. http:\/\/www.open- std.org\/jtc1\/sc22\/wg14\/www\/ docs\/n1637.pdf ."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_4"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535878"},{"key":"e_1_2_2_31_1","volume-title":"ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. 543\u2013548","author":"Krebbers Robbert","year":"2014"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_17"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693571"},{"key":"e_1_2_2_34_1","volume-title":"TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings. 389\u2013391","author":"Kroening Daniel","year":"2014"},{"key":"e_1_2_2_35_1","volume-title":"Proceedings of the 2018 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages &amp; Applications, OOPSLA 2018, part of SPLASH 2018","author":"Lee Juneyoung","year":"2018"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062343"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_2_38_1","unstructured":"Xavier Leroy et al. 2018. CompCert 3.4. http:\/\/compcert.inria.fr\/ .  Xavier Leroy et al. 2018. CompCert 3.4. http:\/\/compcert.inria.fr\/ ."},{"key":"e_1_2_2_39_1","unstructured":"Xavier Leroy Andrew W. Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert Memory Model Version 2. Research report RR-7987. INRIA. http:\/\/hal.inria.fr\/hal- 00703441  Xavier Leroy Andrew W. Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert Memory Model Version 2. Research report RR-7987. INRIA. http:\/\/hal.inria.fr\/hal- 00703441"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_2_2_41_1","unstructured":"Kayvan Memarian Victor Gomes and Peter Sewell. 2018. n2263: Clarifying Pointer Provenance v4. ISO WG14 http: \/\/www.open- std.org\/jtc1\/sc22\/wg14\/www\/docs\/n2263.htm .  Kayvan Memarian Victor Gomes and Peter Sewell. 2018. n2263: Clarifying Pointer Provenance v4. ISO WG14 http: \/\/www.open- std.org\/jtc1\/sc22\/wg14\/www\/docs\/n2263.htm ."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_2_2_43_1","volume-title":"N2090: Clarifying Pointer Provenance (Draft Defect Report or Proposal for C2x). ISO WG14 http:\/\/www.open- std.org\/jtc1\/sc22\/wg14\/www\/docs\/n2090","author":"Memarian Kayvan","year":"2016"},{"key":"e_1_2_2_44_1","volume-title":"ISO SC22 WG14 N2015","author":"Memarian Kayvan","year":"2016"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542504"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/647478.727796"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1254810.1254820"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/645393.651894"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254104"},{"key":"e_1_2_2_54_1","unstructured":"Runtime Verification Inc. 2017. RV-Match. https:\/\/runtimeverification.com\/match\/ .  Runtime Verification Inc. 2017. RV-Match. https:\/\/runtimeverification.com\/match\/ ."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSREW.2015.7392027"},{"key":"e_1_2_2_56_1","volume-title":"tis-interpreter"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"},{"key":"e_1_2_2_60_1","unstructured":"WG14. 2004. Defect Report 260. http:\/\/www.open- std.org\/jtc1\/sc22\/wg14\/www\/docs\/dr_260.htm .  WG14. 2004. Defect Report 260. http:\/\/www.open- std.org\/jtc1\/sc22\/wg14\/www\/docs\/dr_260.htm ."},{"key":"e_1_2_2_61_1","unstructured":"WG14. 2011a. ISO\/IEC 9899:2011.  WG14. 2011a. ISO\/IEC 9899:2011."},{"key":"e_1_2_2_62_1","first-page":"201x","article-title":"Programming Languages \u2014 C","volume":"9899","year":"2011","journal-title":"ISO\/IEC"},{"key":"e_1_2_2_63_1","unstructured":"WG14. 2017. JTC1\/SC22\/WG14 \u2013 C. http:\/\/www.open- std.org\/jtc1\/sc22\/wg14\/ .  WG14. 2017. JTC1\/SC22\/WG14 \u2013 C. http:\/\/www.open- std.org\/jtc1\/sc22\/wg14\/ ."},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.5555\/2665671.2665740"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290380","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290380","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290380"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":60,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290380"],"URL":"https:\/\/doi.org\/10.1145\/3290380","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}