cast from floatbv to fixedbv not implemented

[polgreen]

The cast from floatbv to fixedbv is not implemented. This example gives the following warning:

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

The cast the other way round, from fixedbv to floatbv, does seem to be implemented.

[lucasccordeiro]

@polgreen: Try to talk to @martin-cs about this example and explain the reason by which we need this for the control synthesis project. @martin-cs might give some suggestions of how to proceed in CBMC.

[tautschnig]

@lucasccordeiro @polgreen Isn't the solution to just implement that typecast?

[martin-cs]

On Wed, 2017-02-01 at 05:43 -0800, Michael Tautschnig wrote: @lucasccordeiro @polgreen Isn't the solution to just implement that typecast?

Yes; I have the code for it in symfpu and it is only of the key things needed to turn my SV-COMP hack into a real patch. Will do when I'm back. Cheers, - Martin

[martin-cs]

On Wed, 2017-02-01 at 05:43 -0800, Michael Tautschnig wrote: @lucasccordeiro @polgreen Isn't the solution to just implement that typecast?

Yes. Will do.

[polgreen]

This type case is still missing

[polgreen]

closing this issue as it is duplicate to #2158