Last change
on this file since 7a29392f was
7972603,
checked in by Michael Brooks <mlbrooks@…>, 9 months ago
|
Missing files from last thesis push
|
-
Property mode set to
100644
|
File size:
1.8 KB
|
Line | |
---|
1 | #include <stdio.h> |
---|
2 | #include <assert.h> |
---|
3 | #include <stdlib.h> |
---|
4 | |
---|
5 | #ifdef ERRS |
---|
6 | #define ERR(...) __VA_ARGS__ |
---|
7 | #else |
---|
8 | #define ERR(...) |
---|
9 | #endif |
---|
10 | |
---|
11 | int main() { |
---|
12 | |
---|
13 | /* |
---|
14 | These attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed. |
---|
15 | */ |
---|
16 | float * x; // x points at a floating-point number |
---|
17 | void (*y)(void); // y points at a function |
---|
18 | ERR( |
---|
19 | x = y; // wrong |
---|
20 | y = x; // wrong |
---|
21 | ) |
---|
22 | |
---|
23 | /* |
---|
24 | The first gets |
---|
25 | warning: assignment to `float *' from incompatible pointer type `void (*)(void)' |
---|
26 | and the second gets the opposite. |
---|
27 | |
---|
28 | Similarly, |
---|
29 | */ |
---|
30 | |
---|
31 | float pi = 3.14; |
---|
32 | void f( void (*g)(void) ) { |
---|
33 | g(); |
---|
34 | } |
---|
35 | ERR( |
---|
36 | f( & pi ); // wrong |
---|
37 | ) |
---|
38 | /* |
---|
39 | gets |
---|
40 | warning: passing argument 1 of `f' from incompatible pointer type |
---|
41 | with a segmentation fault at runtime. |
---|
42 | |
---|
43 | That @f@'s attempt to call @g@ fails is not due to 3.14 being a particularly unlucky choice of value to put in the variable @pi@. |
---|
44 | Rather, it is because obtaining a program that includes this essential fragment, yet exhibits a behaviour other than "doomed to crash," is a matter for an obfuscated coding competition. |
---|
45 | |
---|
46 | A "tractable syntactic method for proving the absence of certain program behaviours |
---|
47 | by classifying phrases according to the kinds of values they compute"*1 |
---|
48 | rejected the program. The behaviour (whose absence is unprovable) is neither minor nor unlikely. |
---|
49 | The rejection shows that the program is ill-typed. |
---|
50 | |
---|
51 | Yet, the rejection presents as a GCC warning. |
---|
52 | |
---|
53 | In the discussion following, ``ill-typed'' means giving a nonzero @gcc -Werror@ exit condition with a message that discusses typing. |
---|
54 | |
---|
55 | *1 TAPL-pg1 definition of a type system |
---|
56 | */ |
---|
57 | |
---|
58 | } |
---|
Note: See
TracBrowser
for help on using the repository browser.