This article is about the simplified subset of C. For the Common Intermediate Language (also known as MSIL), see Common Intermediate Language

Common Intermediate Language

Common Intermediate Language is the lowest-level human-readable programming language defined by the Common Language Infrastructure specification and is used by the .NET Framework and Mono...

.

CIL (C Intermediate Language) is a simplified subset of the C programming language, as well as a set of tools for transforming C programs into that language.

Several other tools use CIL as a way to have access to a C abstract syntax tree

Abstract syntax tree

In computer science, an abstract syntax tree , or just syntax tree, is a tree representation of the abstract syntactic structure of source code written in a programming language. Each node of the tree denotes a construct occurring in the source code. The syntax is 'abstract' in the sense that it...

. Some of this programs are Frama-c

Frama-C

Frama-C stands for Framework for Modular Analysis of C programs. Frama-C is a set of interoperable program analyzers for C programs. Frama-C has been developed by Commissariat à l'Énergie Atomique et aux Énergies Alternatives and Inria...

 (Framework to analyze C programs) or Compcert

Compcert

CompCert is a formally verified optimizing compiler for a subset of the C programming language which currently targets PowerPC, ARM and 32-bit x86 architectures. This project, led by Xavier Leroy, started officially in 2005, funded by the French institutes ANR and INRIA. The compiler is...

 (C compiler proven in coq

Coq

In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...

).

CIL was originally designed and implemented by George Necula

George Necula

George Ciprian Necula is a Romanian computer scientist and professor at the University of California, Berkeley who does research in the area of programming languages and software engineering, with a particular focus on software verification and formal methods. He is best known for his Ph.D...

et al. in 2002.

External links

• CIL on SourceForge
• CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs Lecture Notes In Computer Science; Vol. 2304 Proceedings of the 11th International Conference on Compiler Construction Pages: 213 - 228. Year of Publication: 2002. ISBN:3-540-43369-4