CIL swMATH ID: 26691 Software Authors: Necula, G.C.; McPeak, S.; Rahul, S.P.; Weimer, W. Description: CIL: intermediate language and tools for analysis and transformation of C programs. This paper describes the C Intermediate Language: a highlevel representation along with a set of tools that permit easy analysis and source-to-source transformation of C programs. Compared to C, CIL has fewer constructs. It breaks down certain complicated constructs of C into simpler ones, and thus it works at a lower level than abstract-syntax trees. But CIL is also more high-level than typical intermediate languages (e.g., three-address code) designed for compilation. As a result, what we have is a representation that makes it easy to analyze and manipulate C programs, and emit them in a form that resembles the original source. Moreover, it comes with a front-end that translates to CIL not only ANSI C programs but also those using Microsoft C or GNU C extensions. We describe the structure of CIL with a focus on how it disambiguates those features of C that we found to be most confusing for program analysis and transformation. We also describe a whole-program merger based on structural type equality, allowing a complete project to be viewed as a single compilation unit. As a representative application of CIL, we show a transformation aimed at making code immune to stack-smashing attacks. We are currently using CIL as part of a system that analyzes and instruments C programs with run-time checks to ensure type safety. CIL has served us very well in this project, and we believe it can usefully be applied in other situations as well. Homepage: https://link.springer.com/chapter/10.1007%2F3-540-45937-5_16 Related Software: BLAST; CBMC; SLAM; CUTE; veriSoft; CPAchecker; Why3; z3; DART; Java PathFinder; ASTREE; Coq; SPIN; Isabelle/HOL; UFO; Apron; OCaml; KLEE; SIMPLIFY; SatAbs Cited in: 34 Documents all top 5 Cited by 101 Authors 2 Chen, Liqian 2 Gupta, Aarti 2 Havelund, Klaus 2 Leroy, Xavier 2 Wang, Chao 2 Wang, Ji 2 Weimer, Westley 1 Akhundov, Murad 1 Barnat, Jiří 1 Behrends, Reimer 1 Blazy, Sandrine 1 Blot, Arthur 1 Boldo, Sylvie 1 Braunsdorf, Oliver 1 Chaki, Sagar 1 Chechik, Marsha 1 Chroboczek, Juliusz 1 Cousot, Patrick 1 Dai, Hanjun 1 Dixit, Ketan 1 Dos Reis, Gabriel 1 Evans, Jacob 1 Feng, Nick 1 Forrest, Stephanie 1 Foster, Jeffrey S. 1 Ganai, Malay K. 1 Gopalakrishnan, Ganesh Lalitha 1 Groce, Alex 1 Grosu, Radu 1 Gurfinkel, Arie 1 Holzmann, Gerard J. 1 Horsch, Julian 1 Hsiao, Michael S. 1 Huang, Xiaowan 1 Hui, Vincent W. H. 1 Igarashi, Atsushi 1 Imanishi, Akifumi 1 Jeannet, Bertrand 1 Jiang, Jiahong 1 Joshi, Rajeev 1 Kamkin, Alexander 1 Kapur, Deepak 1 Katoen, Joost-Pieter 1 Kerneis, Gabriel 1 Khoroshilov, Alexey 1 Kiselyov, Oleg 1 Kojima, Kensuke 1 Kong, Soonho 1 Kotsynyak, Artem 1 Krishnamoorthy, Saparya 1 Kundu, Sudipta 1 Lange, Tim 1 Lauko, Henrich 1 Limaye, Rhishikesh 1 Lingappan, Loganathan 1 Liu, Jiangchao 1 Lumezanu, Cristian 1 Mandrykin, M. U. 1 Marché, Claude 1 McPeak, Scott 1 Miné, Antoine 1 Mora, Federico 1 Mutilin, V. S. 1 Naik, Aaditya 1 Naik, Mayur 1 Necula, George C. 1 Neuhäußer, Martin R. 1 Nguyen, Thanhvu H. 1 Noll, Thomas 1 Ouadjaout, Abdelraouf 1 Prinz, Frederick 1 Putro, Pavel 1 Qian, Junyan 1 Rahul, Shree P. 1 Ročkai, Petr 1 Sessinghaus, Stefan 1 Seyster, Justin 1 Shved, P. E. 1 Si, Xujie 1 Simon, Luke 1 Smaragdakis, Yannis 1 Smith, Michael J. A. 1 Smolka, Scott A. 1 Song, Le 1 Sotin, Pascal 1 Stoller, Scott D. 1 Strichman, Ofer 1 Stroustrup, Bjarne 1 Terauchi, Tachio 1 Tuch, Harvey 1 Udrea, Octavian 1 Usui, Takayuki 1 Waddington, Daniel 1 Wu, Xueguang 1 Xu, Baowen 1 Xu, Ru-Gang 1 Yamamoto, Masaki 1 Yang, Yu 1 Yao, Bin 1 Yin, Banghu ...and 1 more Authors all top 5 Cited in 12 Serials 4 Journal of Automated Reasoning 2 Formal Methods in System Design 2 Mathematics in Computer Science 1 Programming and Computer Software 1 Science of Computer Programming 1 Information and Computation 1 Formal Aspects of Computing 1 Journal of Parallel and Distributed Computing 1 Annals of Mathematics and Artificial Intelligence 1 Informatica (Vilnius) 1 Higher-Order and Symbolic Computation 1 Science China. Information Sciences Cited in 5 Fields 34 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) 2 Information and communication theory, circuits (94-XX) 1 Numerical analysis (65-XX) 1 Fluid mechanics (76-XX) Citations by Year