Floating Point Literals

[ArquintL]

Gobra currently does not support floating point literals, and reports a type error instead.

Supporting floating point literals poses the following challenges:

• type checker / desugarer / encoding needs to figure out at what point an untyped floating point literal is implicitly casted to float32 or float64. As discussed with @jcp19, it might be best to do this in a new stage between type checking and desugaring, e.g., by inserting an explicit cast operation into the PAST.
• Floating point literals and the casting operation mentioned above need to be added to the encoding. Currently, Gobra encodes floating points as Ints in Viper. Depending on the operations we want to support for floats (e.g., inequality comparisons), we might not be able to use Int any longer and would need to switch, e.g., to bit vectors.

Some preliminary work can be found on branch float-literals.

[ArquintL]

Regarding the encoding, one could connect to the floating point SMT-LIB theory