missing __sym_sitofp

[tkratochvila]

While for example in divine 4.1.6+43d9a505081f was able to convert int to float: divine verify --symbolic test.c
test.c:
extern int VERIFIER_nondet_int();
int main() {

float a =VERIFIER_nondet_int();

}

divine versions from 4.1.20 till 4.2.7 miss a function to do it:

compiling Lift.c
loading bitcode … LART … E: missing function in domain: sym_uitofp
Aborted (core dumped)

[tkratochvila]

It seems that even older version 4.1.6 have some problems if there is an assert on float variable added:

E: .../lart/abstract/substitution.cpp: 307:

encountered Unhandled lifter.

test.c:
#include<assert.h>
extern int VERIFIER_nondet_int();

int main() {

float a =VERIFIER_nondet_int();
assert (a < 222);

}

[Henrich Lauko]

Implementation of nondeterministic floats in DIVINE is currently quite experimental and not well tested. It should be fixed in the near future.

The conversion to/from integers has never worked; what has changed is the detection of unsupported functions. Previously divine proceeded silently.