extern int rpathx_value (void);
int rpathy_value () { return 10 * rpathx_value () + 7; }