Type inference in the C: applications to the static analysis of programs

What is it about?

Type inference is a feature that is common to a variety of programming languages. In the past, it has been prominently present in functional languages like ML and Haskell, but, today, many object-oriented/ multi-paradigm languages such as C# and C++ offer, to a certain extent, such a feature. Nevertheless, type inference still is an unexplored subject in the realm of C, a language that has been around for 4 decades. Over the years, C has evolved in numerous aspects, but its fundamental characteristics remain intact; in particular, its type system: in addition to being static — meaning that type-checking is performed during compilation —, the type system of C has the following distinct properties. - It is nominal, i.e., the equivalence of types is determined by names, which are specified in type declarations (e.g., of a struct). - In C, variable declarations must be annotated with a type, contrasting with the usual type inference setup, where programmers are free from this task. - Although there is no formal or universally accepted definition for "weak" or "strong" typing, we colloquially designate C's (liberal/permissive) type system to the first group. Given all the above, we ask (and respond) to the question of whether it is possible to devise a type inference technique for the C programming language.

Featured Image

Why is it important?

The existence of type inference technique for the C programming language: - enables static analysis on partial programs; - supports semantic tools despite of #include failures; - offers the possibility of a code snippet (e.g., retrieved from a bug tracker) compilation; - allows the generation of test-input data for a given function — in isolation; - allows the prototyping of an algorithm, even without "type specifications".

Perspectives