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
comment:2 Changed 5 years ago by
Owner: | changed from mornfall to Henrich Lauko |
---|---|
Status: | new → assigned |
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.
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:
test.c:
#include<assert.h>
extern int VERIFIER_nondet_int();
int main() {
}