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

On 03/04/13 08:35, Urmas Repinski wrote:
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
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to