int get_return_value() { return 10; }