Support float presence

[RaitoBezarius]

Code snippet that is not correctly supported:

struct Something;
impl Something {
   fn from_slice_f32(n: &mut [f32]) { }
   fn from_slice_u32(n: &mut [u32]) { }
}

Current Charon output:

On rustyguard-types crate which makes no use of f(32|64): https://github.com/conradludgate/rustyguard.

error: Floats are not supported yet
    --> /home/raito/.cargo/registry/src/index.crates.io-6f17d22bba15001f/byteorder-1.5.0/src/lib.rs:1786:5
     |
1786 |     fn from_slice_f32(numbers: &mut [f32]);
     |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Expected behavior: In practice, rustyguard-types makes no use of floats, so being able to skip over them if they end up not being used seems relevant.

[sonmarcho]

This is not difficult actually, put aside the model for floating point numbers (but we can start by modelling them as real numbers, then refine later, or simply fail in Aeneas - Charon at least should not fail on those).

[Nadrieril]

Done in https://github.com/AeneasVerif/charon/pull/333