UC BERKELEY
EECS technical reports
TECHNICAL REPORTS


CSD-01-1160.pdf
CSD-01-1160.ps
Conditions of Use

Archive Home Page

Checking Programmer-Specified Non-Aliasing

Authors:
Foster, Jeffrey S.
Aiken, Alex
Technical Report Identifier: CSD-01-1160
October 3, 2001
CSD-01-1160.pdf
CSD-01-1160.ps

Abstract: We study the new ANSI C type qualifier restrict, which allows programmers to specify pointers that are not aliased to other pointers. The main contribution of this paper is a formal semantics for restrict and a type and effect system for checking that restrict-annotated programs are correct with respect to our semantics. We give an efficient inference algorithm for our type system and describe natural extensions of our type system to include subtyping, parametric polymorphism, and affects clauses that capture the effects of calling a function. We also discuss ways in which our type system differs from the ANSI C standard.