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

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