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; z3; DART; Java PathFinder; ASTREE; Coq; SPIN; KLEE; CPAchecker; SIMPLIFY; Why3; SatAbs; JML; Bandera; Isabelle/HOL; CCured
Cited in: 30 Publications
all top 5

Cited by 86 Authors

2 Gupta, Aarti
2 Havelund, Klaus
2 Leroy, Xavier
2 Wang, Chao
2 Weimer, Westley
1 Akhundov, Murad
1 Barnat, Jiří
1 Behrends, Reimer
1 Blazy, Sandrine
1 Blot, Arthur
1 Boldo, Sylvie
1 Chaki, Sagar
1 Chechik, Marsha
1 Chen, Liqian
1 Chroboczek, Juliusz
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 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 Kapur, Deepak
1 Kerneis, Gabriel
1 Kiselyov, Oleg
1 Kojima, Kensuke
1 Kong, Soonho
1 Krishnamoorthy, Saparya
1 Kundu, Sudipta
1 Lauko, Henrich
1 Limaye, Rhishikesh
1 Lingappan, Loganathan
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 Nguyen, Thanhvu H.
1 Ouadjaout, Abdelraouf
1 Qian, Junyan
1 Rahul, Shree P.
1 Ročkai, Petr
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 Wang, Ji
1 Wu, Xueguang
1 Xu, Baowen
1 Xu, Ru-Gang
1 Yamamoto, Masaki
1 Yang, Yu
1 Yao, Bin
1 Zadok, Erez

Citations by Year