gpio_init_mask does not initialize GPIOs 32-47 on RP2350B

[romain145]

https://github.com/raspberrypi/pico-sdk/blob/a1438dff1d38bd9c65dbd693f0e5db4b9ae91779/src/rp2_common/hardware_gpio/gpio.c#L283

The gpio_mask is a uint, which is 32 bits. I suspect GPIOs above 31 are initialized incorrectly on RP2350B.

[lurch]

Hmmm, maybe there ought to be a gpio_init_mask64 function, similar to the various other *_masked64 functions in that file? (Also, perhaps it makes sense to change void gpio_init_mask(uint gpio_mask) to a more explicit void gpio_init_mask(uint32_t gpio_mask), in order to be consistent with all the other functions that take a gpio_mask parameter?)