Opened 5 years ago

Last modified 5 years ago

#107 assigned defect

unreachable executed: unknown binary operation fp.leq

Reported by: P. Berger Owned by: Henrich Lauko
Priority: minor Milestone: 4.4
Component: DiOS Keywords:
Cc:

Description

I tested DIVINE on an example program and it fails with the error message: "unreachable executed: unknown binary operation fp.leq".

The program is:

extern void VERIFIER_assume(int);
extern float VERIFIER_nondet_float();

float a;
float VERIFIER_nondet_float();
int main() {

a = VERIFIER_nondet_float();
VERIFIER_assume(a <= 0);

}

The version of DIVINE is DIVINE 4, version 4.4.0+32c9761c4eb1, and my commandline was "./divine check --symbolic --svcomp example.c".

Is this expected behavior?

Change History (3)

comment:1 Changed 5 years ago by Henrich Lauko

Component: other → DiOS
Owner: changed from mornfall to Henrich Lauko
Status: new → assigned

Hi,

The current divine does not provide symbolic verification with floating-point values. If you want to use it, you can try experimental implementation from SV-COMP 2020: ​https://divine.fi.muni.cz/2020/sv-comp/

Floating-point support should be merged into the current in the following weeks.

Version 0, edited 5 years ago by Henrich Lauko (next)

comment:2 Changed 5 years ago by P. Berger

The version I used is exactly the version of SV-COMP 2020 ($ sha1sum divine-binary.zip
4a873bf8b46e2d6ab774e7a6809344c4d6cc77ff divine-binary.zip).

comment:3 Changed 5 years ago by Henrich Lauko

You have to run DIVINE with '--solver z3', because DIVINE's default smt solver (STP) does not support floating points.

Note: See TracTickets for help on using tickets.