[klee-dev] +- 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
 		 	   		  
-------------- next part --------------
HTML attachment scrubbed and removed