Opened 5 years ago

Last modified 5 years ago

#60 assigned defect

missing __sym_sitofp

Reported by: tkratochvila Owned by: Henrich Lauko
Priority: major Milestone: 4.3
Component: other Keywords: symbolic floats
Cc:

Description

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)

Change History (2)

comment:1 Changed 5 years ago by 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);

}

comment:2 Changed 5 years ago by Henrich Lauko

Owner: changed from mornfall to Henrich Lauko
Status: newassigned

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.

Note: See TracTickets for help on using tickets.