Typecast from double to __CPROVER_fixedbv not implemented

[polgreen]

Small example and accompanying warning message:

smallexample.c:
int main(){
__CPROVER_fixedbv[24][12] A;
A = 0.7;
assert(0);
return 0;
}

warning: ignoring typecast

• type: fixedbv
  • width: 24
  • integer_bits: 12
    0: constant
  • type: floatbv
    • width: 64
    • f: 52
    • #c_type: double
  • value: 0011111111100110011001100110011001100110011001100110011001100110
  • #source_location:
    • file: smalltest.c
    • line: 4
    • function: main

[martin-cs]

Yeah... this is what I meant about untested. Sorry. Setting to 7 (integer) and then dividing by 10 might give a work around. I can fix this; how urgently do you need it done? Cheers, - Martin

[polgreen]

Hmm really soon? I'll see if I can just use the work around though, will let you know. Not sure if it's just me using it: @pkesseli, @dcattaruzza ?

[polgreen]

This seems weird?

int main(){
__CPROVER_fixedbv[24][12] A;
A = 7;
A = A/10;
assert(0);
return 0;
}

warning: ignoring typecast

• type: floatbv
  • width: 32
  • f: 23
  • #c_type: float
    0: constant
  • type: fixedbv
    • width: 24
    • integer_bits: 12
  • value: 000000000111000000000000
    warning: ignoring typecast
• type: fixedbv
  • width: 24
  • integer_bits: 12
    0: floatbv_div
  • type: floatbv
    • width: 32
    • f: 23
    • #c_type: float
  • #source_location:
    • file: smalltest.c
    • line: 5
    • function: main

[polgreen]

Hi Martin,

Pascal has pointed out that if we run with --fixedbv, it automatically replaced the numbers with bvs and so we don't need the cast from double -> fixedbv.

The cast from 2 different precision of fixedbv does work =)

[kroening]

There are two separate problems here:

1. The missing implementation of the fixedbv -> floatbv and floatbv -> fixedbv casts.
2. The front-end should not generate a cast from fixedbv to floatbv on any of the arithmetic operations during arithmetic promotion. This would make --fixedbv unnecessary.

[kroening]

Please try 9908b6e. This implements arithmetic promotion for fixed-point arithmetic.

This has profound implications for the control synthesis. On the positive side, this may avoid a lot of conversions to bigger types, which may improve performance. On the negative side, this may reduce precision.

Note that there still isn't conversion from double/float to fixedbv.

[kroening]

There is now conversion of float constants to fixedbv constants, i.e., you can assign a double/float literal to a fixed-point variable.

To do comparison with a constant, convert the double/float literal to the fixedbv type, or otherwise the fixedbv gets promoted to the floating-point type.