[CN] Make defining constants (and lifted pure functions easier)

[dc-mak]

This is too verbose

#define CONST 1
    /*@ function (i32) CONST () @*/
    static int c_CONST() /*@ cn_function CONST; @*/ { return CONST; }

Save some pre-processor engineering, this could at least be simplified to

#define CONST 1
    static int c_CONST() /*@ define CONST; @*/ { return CONST; }

Or even just this where it derives that name from the C function according to some scheme.

#define CONST 1
    static int c_CONST() /*@ define; @*/ { return CONST; }

Keyword "define" up for debate.

[peterohanley]

If we are considering adding syntax, is it possible to use an attribute or something else that survives preprocessing (or, does cn do preprocessing with comments kept?). We are very close to this working:

#define CONST 1
#define cn_definer(ty, def) static ty cn_##def () /*@ something here @*/ { return def ; }
cn_definer(int,CONST)

% gcc -E -P -CC constant_defines.c 
static int cn_CONST () /*@ something here @*/ { return 1 ; }

My motivation here is no duplication of the define name.