Checking Programmer-Specified Non-Aliasing

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 2001
Accession Number
ADA603563

Entities

People

  • Alex Aiken
  • Jeffrey S. Foster

Organizations

  • University of California, Berkeley

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • C Programming Language
  • Calculus
  • California
  • Compilers
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Construction
  • Language
  • Linguistics
  • Programming Languages
  • Semantics
  • Software Development
  • Standards

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Database Systems and Applications

Technology Areas

  • AI & ML