An abstract dynamic semantics for C

Michael Norrish

Computer Laboratory, University of Cambridge

May 6, 1997

Abstract

This report is a presentation of a formal semantics for the C programming language. The semantics has been defined operationally in a structured semantics style and covers the bulk of the core of the language. The semantics has been developed in a theorem prover (HOL), where some expected consequences of the language definition have been proved.

Contents

1 Introduction 2

1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2 The C language 4

2.1 What has been omitted . . . . . . . . . . . . . . . . . . . . . . . 4

2.2 Basic definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2.2.1 Degrees of under-specification . . . . . . . . . . . . . . . . 5

2.2.2 Program states and side effects . . . . . . . . . . . . . . . 6

2.2.3 Notation|general observations . . . . . . . . . . . . . . . 7

2.3 Expression evaluation . . . . . . . . . . . . . . . . . . . . . . . . 8

2.3.1 Extra syntactic forms and undefined expressions . . . . . 8

2.3.2 Expression evaluation contexts . . . . . . . . . . . . . . . 9

2.3.3 Base cases|values out of memory . . . . . . . . . . . . . 10

2.3.4 Value producing operators . . . . . . . . . . . . . . . . . . 13

2.3.5 Side effect operators . . . . . . . . . . . . . . . . . . . . . 16

2.3.6 Function calls|the interface with statement evaluation . 19