diff options
-rw-r--r-- | lib/Core/Executor.cpp | 2 | ||||
-rw-r--r-- | test/regression/2020-01-14-fabs-compare.c | 16 |
2 files changed, 17 insertions, 1 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 48252dbd..7fac4fa4 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1420,7 +1420,7 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, break; case Intrinsic::fabs: { ref<ConstantExpr> arg = - toConstant(state, eval(ki, 0, state).value, "floating point"); + toConstant(state, arguments[0], "floating point"); if (!fpWidthToSemantics(arg->getWidth())) return terminateStateOnExecError( state, "Unsupported intrinsic llvm.fabs call"); diff --git a/test/regression/2020-01-14-fabs-compare.c b/test/regression/2020-01-14-fabs-compare.c new file mode 100644 index 00000000..563a6609 --- /dev/null +++ b/test/regression/2020-01-14-fabs-compare.c @@ -0,0 +1,16 @@ +// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --exit-on-error --output-dir=%t.klee-out %t.bc + +#include <math.h> +#include <assert.h> + +int main(void) { + long double a = 0.25; + long double b = -a; + + long double b_abs = fabsl(b); + + assert(a == b_abs); + return 0; +} |