The XDR Float and Double decode functions in CubedOS.Lib.XDR haven't been fully proven by spark. They're pretty well tested and definitely work, but SPARK is complaining about some sort of type conversion technicality and we really should try to resolve it.
The Float and Double encode functions use Ada.Unchecked_Conversion instead of mathematically encoding the float. This appears to work on GNAT which uses 32 and 64 bit floats in its implementation, but I doubt this is a portable solution between compilers and platforms and it should be changed to something more correct.
The XDR Float and Double decode functions in CubedOS.Lib.XDR haven't been fully proven by spark. They're pretty well tested and definitely work, but SPARK is complaining about some sort of type conversion technicality and we really should try to resolve it.
The Float and Double encode functions use
Ada.Unchecked_Conversioninstead of mathematically encoding the float. This appears to work on GNAT which uses 32 and 64 bit floats in its implementation, but I doubt this is a portable solution between compilers and platforms and it should be changed to something more correct.