`sbi_cppc_write` is never passed the full 64-bit value when `__riscv_xlen == 32`

[repnop]

https://github.com/riscv-software-src/opensbi/blob/791704cd09c019decf438f6e4f56423cc95cb66a/lib/sbi/sbi_ecall_cppc.c#L36

Unless there's something I've missed in the SBI specification about CPPC register values never exceeding 32-bits when XLEN is 32, this line is wrong whenever the code is compiled for __riscv_xlen == 32, as it implicitly promotes the unsigned long (32-bits) to a uint64_t instead of reading the full 64-bit value out of a1 and a2 and combining them into a 64-bit value.

[avpatel]

Yes, this line needs to be fixed for RV32. Please send a patch to the OpenSBI mailing list.