Copyright (c) the Selfie Project authors. All rights reserved. Please see the AUTHORS file for details. Use of this source code is governed by a BSD license that can be found in the LICENSE file.
Selfie is a project of the Computational Systems Group at the Department of Computer Sciences of the University of Salzburg in Austria. For further information and code please refer to:
selfie.cs.uni-salzburg.at
This document provides an overview of the differences in semantics between the programming language C* in which selfie is written and the programming language C. Syntactically, C* is a strict subset of C. Semantically, however, C* differs from C in, for example, how integer literals and strings are handled. Note that the results presented here were obtained with tools that implement C11 semantics.
Integer literals in C* are interpreted as unsigned 64-bit integers (uint64_t). In C, however, integer literals are interpreted as signed 32-bit integers (int). As a result, an expression may evaluate to different values in C* and C if the expression involves integer literals and operators with different semantics for signed and unsigned operands, that is, /, %, <, <=, >, and >=.
uint64_t x;
uint64_t y;
x = 1 / -1;
y = 1 % -1;
C*:
x == 0
y == 1
C:
x == -1
y == 0
uint64_t a;
uint64_t b;
uint64_t c;
uint64_t d;
a = 1 < -1;
b = 1 <= -1;
c = 1 > -1;
d = 1 >= -1;
C*:
a == 1
b == 1
c == 0
d == 0
C:
a == 0
b == 0
c == 1
d == 1
String literals in C* are interpreted as uint64_t*, that is, pointers to uint64_t whereas string literals in C are interpreted as arrays of type char. Thus dereferencing a string literal in C* results in an uint64_t value containing up to eight characters rather than just a char value containing only one character as in C.
uint64_t x;
x = *"Hello World!";
C*:
x == 0x6F57206F6C6C6548
C:
x == 0x48
Note that 0x48 is ASCII for H. Moreover, 0x65, 0x6C, 0x6F, 0x20, and 0x57 are ASCII for e, l, o, , and W, respectively.
Per C standard, consecutive calls to the procedure malloc() always have to return unique addresses independent of the actual size parameter. However, allocating memory in C* with 0 as size parameter results in no memory allocation at all. Therefore, consecutive calls to malloc() do always return the same address.
C*:
malloc(0) == malloc(0)
C:
malloc(0) != malloc(0)