View Full Document

A Theory of Type Qualifiers



View the full content.
View Full Document
View Full Document

4 views

Unformatted text preview:

A Theory of Type Qualifiers Jeffrey S Foster jfoster cs berkeley edu Manuel Fa hndrich maf microsoft com Alexander Aiken aiken cs berkeley edu EECS Department University of California Berkeley Berkeley CA 94720 1776 Purify Pur which test for properties in a particular program execution A canonical example of a type qualifier from the C world is the ANSI C qualifier const A variable with a type annotated with const can be initialized but not updated 1 A primary use of const is annotating pointer valued function parameters as not being updated by the function Not only is this information useful to a caller of the function but it is automatically verified by the compiler up to casting Another example is Evans s lclint Eva96 which introduces a large number of additional qualifier like annotations to C as an aid to debugging memory usage errors One such annotation is nonnull which indicates that a pointer value must not be null Evans found that adding such annotations greatly increased compile time detection of null pointer dereferences Eva96 Although it is not a typebased system we believe that annotations like lclint s can be expressed naturally as type qualifiers in our framework Yet another example of type qualifiers comes from binding time analysis which is used in partial evaluation systems Hen91 DHM95 Binding time analysis infers whether values are known at compile time the qualifier static or may not be known until run time the qualifier dynamic by specializing the program with respect to an initial input There are also many other examples of type qualifiers in the literature Each of the cited examples adds particular type qualifiers for a specific application This paper presents a framework for adding new user specified type qualifiers to a language in a general way Our framework also extends the standard type system to perform qualifier inference which propagates programmer supplied annotations through the program and checks them Such a system gives the



Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view A Theory of Type Qualifiers and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view A Theory of Type Qualifiers and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?