{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:23:47Z","timestamp":1779074627064,"version":"3.51.4"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2024,8,29]],"date-time":"2024-08-29T00:00:00Z","timestamp":1724889600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,8,29]],"date-time":"2024-08-29T00:00:00Z","timestamp":1724889600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005713","name":"Technische Universit\u00e4t M\u00fcnchen","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005713","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2024,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The C programming language offers  as a mechanism for nonlocal control flow. This mechanism has complicated semantics. As most developers do not encounter it day-to-day, they may be unfamiliar with all its intricacies \u2013 leading to subtle programming errors. At the same time, most static analyzers lack proper support, implying that otherwise sound tools miss whole classes of program deficiencies. We propose a concrete semantics of a subset of C with , where interprocedural s are performed directly, as well as an equivalent formulation where such jumps are implemented via stack-unwinding at the call-sites. Reflecting this semantic equivalence, we propose an approach for lifting existing interprocedural analyses to support  and to flag their misuse. To deal with the nonlocal semantics, our approach leverages side-effecting transfer functions, which, when executed, may additionally trigger contributions for program points that are not static control-flow successors. We showcase our analysis on a real-world example and propose a set of litmus tests for other analyzers.<\/jats:p>","DOI":"10.1007\/s10009-024-00764-z","type":"journal-article","created":{"date-parts":[[2024,8,29]],"date-time":"2024-08-29T14:02:43Z","timestamp":1724940163000},"page":"589-605","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["When long jumps fall short: control-flow tracking and misuse detection for nonlocal jumps in C"],"prefix":"10.1007","volume":"26","author":[{"given":"Julian","family":"Erhard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Schwarz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vesal","family":"Vojdani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simmo","family":"Saan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helmut","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,8,29]]},"reference":[{"key":"764_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-35182-2_12","volume-title":"Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Proceedings","author":"K. Apinis","year":"2012","unstructured":"Apinis, K., Seidl, H., Vojdani, V.: side-effecting constraint systems: a Swiss army knife for program analysis. In: Jhala, R., Igarashi, A. (eds.) Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Proceedings, Kyoto, Japan, December 11-13, 2012, Lecture Notes in Computer Science, vol.\u00a07705, pp.\u00a0157\u2013172. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-35182-2_12"},{"issue":"2\u20133","key":"764_CR2","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1561\/2500000002","volume":"2","author":"J. Bertrane","year":"2015","unstructured":"Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Static analysis and verification of aerospace software by abstract interpretation. Found. Trends Program. Lang. 2(2\u20133), 71\u2013190 (2015). https:\/\/doi.org\/10.1561\/2500000002","journal-title":"Found. Trends Program. Lang."},{"key":"764_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-031-57256-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems \u2013 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings, Part III","author":"D. Beyer","year":"2024","unstructured":"Beyer, D.: State of the art in software verification and witness validation: SV-COMP 2024. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems \u2013 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings, Part III, Luxembourg City, Luxembourg, April 6\u201311, 2024. Lecture Notes in Computer Science, vol.\u00a014572, pp.\u00a0299\u2013329. Springer, Berlin (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_15"},{"key":"764_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-52234-0_7","volume-title":"Verification, Model Checking, and Abstract Interpretation \u2013 18th International Conference, VMCAI 2017, Proceedings","author":"S. Blazy","year":"2017","unstructured":"Blazy, S., B\u00fchler, D., Yakobowski, B.: Structuring abstract interpreters through state and value abstractions. In: Bouajjani, A., Monniaux, D. (eds.) Verification, Model Checking, and Abstract Interpretation \u2013 18th International Conference, VMCAI 2017, Proceedings, Paris, France, January 15\u201317, 2017. Lecture Notes in Computer Science, vol.\u00a010145, pp.\u00a0112\u2013130. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_7"},{"key":"764_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.infsof.2016.05.003","volume":"77","author":"B. Chang","year":"2016","unstructured":"Chang, B., Choi, K.: A review on exception analysis. Inf. Softw. Technol. 77, 1\u201316 (2016). https:\/\/doi.org\/10.1016\/j.infsof.2016.05.003","journal-title":"Inf. Softw. Technol."},{"key":"764_CR6","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1145\/2970276.2970347","volume-title":"Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering, ASE 2016","author":"M. Christakis","year":"2016","unstructured":"Christakis, M., Bird, C.: What developers want and need from program analysis: an empirical study. In: Lo, D., Apel, S., Khurshid, S. (eds.) Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3\u20137, 2016, pp.\u00a0332\u2013343. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2970276.2970347"},{"key":"764_CR7","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Conference Record of the Fourth ACM Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, pp.\u00a0238\u2013252. ACM, New York (1977). https:\/\/doi.org\/10.1145\/512950.512973"},{"key":"764_CR8","volume-title":"Proceedings of the 13th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis, SOAP 2024","author":"J. Erhard","year":"2024","unstructured":"Erhard, J., Schinabeck, J.F., Schwarz, M., Seidl, H.: When to stop going down the rabbit hole: taming context-sensitivity on the fly. In: Monat, R., Rubio-Gonz\u00e1lez, C. (eds.) Proceedings of the 13th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis, SOAP 2024, Copenhagen, Denmark. ACM, New York (2024). To appear"},{"key":"764_CR9","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1145\/1133981.1134028","volume-title":"Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation","author":"X. Feng","year":"2006","unstructured":"Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. In: Schwartzbach, M.I., Ball, T. (eds.) Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, Ottawa, Ontario, Canada, June 11\u201314, 2006, pp.\u00a0401\u2013414. ACM, New York (2006). https:\/\/doi.org\/10.1145\/1133981.1134028"},{"key":"764_CR10","series-title":"Proceedings, Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-319-77935-5_14","volume-title":"NASA Formal Methods - 10th International Symposium, NFM 2018, Newport News","author":"A. Fromherz","year":"2018","unstructured":"Fromherz, A., Ouadjaout, A., Min\u00e9, A.: Static value analysis of python programs by abstract interpretation. In: Dutle, A., Mu\u00f1oz, C.A., Narkawicz, A. (eds.) NASA Formal Methods - 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17\u201319, 2018. Proceedings, Lecture Notes in Computer Science, vol.\u00a010811, pp.\u00a0185\u2013202. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-77935-5_14"},{"issue":"1","key":"764_CR11","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/S0167-6423(00)00014-9","volume":"39","author":"M. Hind","year":"2001","unstructured":"Hind, M., Pioli, A.: Evaluating the effectiveness of pointer alias analyses. Sci. Comput. Program. 39(1), 31\u201355 (2001). https:\/\/doi.org\/10.1016\/S0167-6423(00)00014-9","journal-title":"Sci. Comput. Program."},{"key":"764_CR12","unstructured":"Leroy, X.: The CompCert C verified compiler \u2013 documentation and user\u2019s manual \u2013 version 3.12 (2022). Tech. rep"},{"issue":"2","key":"764_CR13","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/2644805","volume":"58","author":"B. Livshits","year":"2015","unstructured":"Livshits, B., Sridharan, M., Smaragdakis, Y., Lhot\u00e1k, O., Amaral, J.N., Chang, B.E., Guyer, S.Z., Khedker, U.P., M\u00f8ller, A., Vardoulakis, D.: In defense of soundiness: a manifesto. Commun. ACM 58(2), 44\u201346 (2015). https:\/\/doi.org\/10.1145\/2644805","journal-title":"Commun. ACM"},{"key":"764_CR14","unstructured":"MITRE: CVE-2018-14876. (2018). https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2018-14876. [accessed 09-March-2023]"},{"key":"764_CR15","unstructured":"MITRE: CVE-2013-1441. (2013). https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2013-1441. [Accessed 09-March-2023]"},{"key":"764_CR16","unstructured":"Monat, R.: Static type and value analysis by abstract interpretation of Python programs with native C libraries. (analyse statique, de type et de valeur, par interpr\u00e9tation abstraite, de programmes Python utilisant des librairies C). Ph.D. thesis, Sorbonne University, Paris, France (2021) https:\/\/tel.archives-ouvertes.fr\/tel-03533030"},{"key":"764_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-031-57256-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings, Part III","author":"R. Monat","year":"2024","unstructured":"Monat, R., Milanese, M., Parolini, F., Boillot, J., Ouadjaout, A., Min\u00e9, A.: Mopsa-c: improved verification for C programs, simple validation of correctness witnesses (competition contribution). In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings, Part III, Luxembourg City, Luxembourg, April 6\u201311, 2024. Lecture Notes in Computer Science, vol.\u00a014572, pp.\u00a0387\u2013392. Springer, Berlin (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_26"},{"key":"764_CR18","unstructured":"Patrakov, A.: Dangers of setjmp()\/longjmp() (2009). https:\/\/patrakov.blogspot.com\/2009\/07\/dangers-of-setjmplongjmp.html. Online; accessed 09-March-2023"},{"key":"764_CR19","unstructured":"Roberts, E.S.: Implementing exceptions in C. Tech. Rep. 40, Digital Equipment Corporation, Systems Research Center (1989)"},{"key":"764_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-031-57256-2_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems \u2013 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings, Part III","author":"S. Saan","year":"2024","unstructured":"Saan, S., Erhard, J., Schwarz, M., Bozhilov, S., Holter, K., Tilscher, S., Vojdani, V., Seidl, H.: Goblint: abstract interpretation for memory safety and termination (competition contribution). In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems \u2013 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings, Part III, Luxembourg City, Luxembourg, April 6-11, 2024. Lecture Notes in Computer Science, vol.\u00a014572, pp.\u00a0381\u2013386. Springer, Berlin (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_25"},{"key":"764_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-030-17465-1_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems \u2013 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings, Part II","author":"P.D. Schubert","year":"2019","unstructured":"Schubert, P.D., Hermann, B., Bodden, E.: Phasar: an inter-procedural static analysis framework for C\/C++. In: Vojnar, T., Zhang, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems \u2013 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings, Part II, Prague, Czech Republic, April 6\u201311, 2019. Lecture Notes in Computer Science, vol.\u00a011428, pp.\u00a0393\u2013410. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_22"},{"key":"764_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-030-88806-0_18","volume-title":"Static Analysis \u2013 28th International Symposium, SAS 2021, Proceedings","author":"M. Schwarz","year":"2021","unstructured":"Schwarz, M., Saan, S., Seidl, H., Apinis, K., Erhard, J., Vojdani, V.: Improving thread-modular abstract interpretation. In: Dragoi, C., Mukherjee, S., Namjoshi, K.S. (eds.) Static Analysis \u2013 28th International Symposium, SAS 2021, Proceedings, Chicago, IL, USA, October 17\u201319, 2021. Lecture Notes in Computer Science, vol.\u00a012913, pp.\u00a0359\u2013383. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_18"},{"key":"764_CR23","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/3589250.3596140","volume-title":"Proceedings of the 12th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis, SOAP 2023","author":"M. Schwarz","year":"2023","unstructured":"Schwarz, M., Erhard, J., Vojdani, V., Saan, S., Seidl, H.: When long jumps fall short: control-flow tracking and misuse detection for non-local jumps in C. In: Ferrara, P., Hadarean, L. (eds.) Proceedings of the 12th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis, SOAP 2023, Orlando, FL, USA, 17 June 2023, pp.\u00a020\u201326. ACM, New York (2023). https:\/\/doi.org\/10.1145\/3589250.3596140"},{"key":"764_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-031-30044-8_2","volume-title":"Programming Languages and Systems \u2013 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings","author":"M. Schwarz","year":"2023","unstructured":"Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V.: Clustered relational thread-modular abstract interpretation with local traces. In: Wies, T. (ed.) Programming Languages and Systems \u2013 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings, Paris, France, April 22\u201327, 2023. Lecture Notes in Computer Science, vol.\u00a013990, pp.\u00a028\u201358. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-30044-8_2"},{"key":"764_CR25","first-page":"413","volume-title":"Proceedings \u2013 Estonian Academy of Sciences Physics Mathematics","author":"H. Seidl","year":"2003","unstructured":"Seidl, H., Vene, V., M\u00fcller-Olm, M.: Global invariants for analysing multi-threaded applications. In: Proceedings \u2013 Estonian Academy of Sciences Physics Mathematics, vol.\u00a052, pp.\u00a0413\u2013436. Estonian Academy Publishers (2003)"},{"key":"764_CR26","first-page":"141","volume":"30","author":"V. Vojdani","year":"2009","unstructured":"Vojdani, V., Vene, V.: Goblint: path-sensitive data race analysis. Ann. Univ. Sci. Budapest., Sect. Comput. 30, 141\u2013155 (2009)","journal-title":"Ann. Univ. Sci. Budapest., Sect. Comput."},{"key":"764_CR27","first-page":"391","volume-title":"Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering, ASE 2016","author":"V. Vojdani","year":"2016","unstructured":"Vojdani, V., Apinis, K., R\u00f5tov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the Goblint approach. In: Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering, ASE 2016, pp.\u00a0391\u2013402. ACM, New York (2016)"},{"key":"764_CR28","unstructured":"Wilson, R.P.: Efficient, context-sensitive pointer analysis for C programs. Ph.D. thesis, Stanford University (1997)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00764-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-024-00764-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00764-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,27]],"date-time":"2024-09-27T13:05:18Z","timestamp":1727442318000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-024-00764-z"}},"subtitle":["Extended version"],"short-title":[],"issued":{"date-parts":[[2024,8,29]]},"references-count":28,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["764"],"URL":"https:\/\/doi.org\/10.1007\/s10009-024-00764-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,29]]},"assertion":[{"value":"14 August 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 August 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}