source: doc/theses/mike_brooks_MMath/programs/bkgd-c-tyerr.c @ 7972603

Last change on this file since 7972603 was 7972603, checked in by Michael Brooks <mlbrooks@…>, 5 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
11int 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.