return_value32_token
table_init(AUT_RETURN32, "return", return_value32_token, T_ENCLOSED);
extern int return_value32_token();
extern void return_value32_token();