+- Inf during klee test generation

[Urmas Repinski]

Hello.

I have test cases generated using klee, when values like 2147483647 and -2147483136 are appear in test cases, those are equivalents for +Inf and -Inf for integer numbers.

I want to disable this +- Infs, for example instead of -2147483136 klee can generate highest possible number, not smallest, and instead of 2147483647 lowest possible number.

klee options

-enable-no-infs-fp-math - Enable FP math optimizations that assume no +-Infs
-enable-no-nans-fp-math - Enable FP math optimizations that assume no NaNs

give no result, still values 2147483647 and -2147483136 appear in generated values.

Tried to use --enable-no-infs-fp-math and --enable-no-nans-fp-math - no result.

Maybe somebody has any suggestions?

Urmas Repinski

[Cristian Cadar]

Hi Urmas,

Those options are inherited from LLVM and don't affect the values
generated by KLEE through STP. (We need to reorganize the way KLEE
options are displayed; Dan Liew is currently looking into this.)

There is currently no support for generating the smallest or largest
possible value.

Cristian

Post by Urmas Repinski
Hello.
I have test cases generated using klee, when values like 2147483647 and
-2147483136 are appear in test cases, those are equivalents for +Inf and
-Inf for integer numbers.
I want to disable this +- Infs, for example instead of -2147483136 klee
can generate highest possible number, not smallest, and instead of
2147483647 lowest possible number.
klee options
-enable-no-infs-fp-math - Enable FP math
optimizations that assume no +-Infs
-enable-no-nans-fp-math - Enable FP math
optimizations that assume no NaNs
give no result, still values 2147483647 and -2147483136 appear in generated values.
Tried to use --enable-no-infs-fp-math and --enable-no-nans-fp-math - no
result.
Maybe somebody has any suggestions?
Urmas Repinski
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev