int foo_system_value (void) { return 42; }