[klee-dev] +- Inf during klee test generation

[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

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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>