|
Last change
on this file since f2898df was 7972603, checked in by Michael Brooks <mlbrooks@…>, 23 months ago |
|
Missing files from last thesis push
|
-
Property mode
set to
100644
|
|
File size:
1.8 KB
|
| Rev | Line | |
|---|
| [7972603] | 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.