conversion fixed-point <-> floating-point numbers missing

[kroening]

Conversions from fixed-point numbers to floating-point numbers and the other direction aren't implemented in any of the solver backends

[polgreen]

This is the same as the issue I filed in January 2017:
#482

[polgreen]

Related: casts between different lengths of fixed point bit vectors are broken in goto-cc.
#2177

[polgreen]

Closed the duplicate issue. The test case for this, in the duplicate issue was:

void main()
{
__CPROVER_floatbv[32][23] float_a;
__CPROVER_fixedbv[24][12] fixed_b;

float_a = 2.14;
fixed_b = 2.5;
float_a = (__CPROVER_floatbv[32][23])fixed_b;
__CPROVER_assert(0, "");
}

warning: ignoring typecast

type: floatbv
width: 32
f: 23
#source_location:
file: floatcast.c
line: 10

[martin-cs]

I have the code for this in SymFPU. I can try to schedule some time to get this done but it is unlikely to be this month due to deadlines. Is that a problem?

[polgreen]

Nope, no hard deadline, I was just tidying my issue list.