Bug in the handling of rounding around underflow
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3598 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
parent
af57b4231c
commit
84a414ccef
|
@ -0,0 +1,13 @@
|
|||
#include <assert.h>
|
||||
|
||||
int main (int argc, char **argv) {
|
||||
float f = 0x1.9e0c22p-101f;
|
||||
float g = -0x1.3c9014p-50f;
|
||||
float target = -0x1p-149f;
|
||||
|
||||
float result = f * g;
|
||||
|
||||
assert(result == target);
|
||||
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
--floatbv --no-simplify
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
||||
^warning: ignoring
|
Loading…
Reference in New Issue