search

ApproxSymate / klee

KLEE Symbolic Virtual Machine for Numerical Precision Analysis
Other
0 stars 0 forks source link

Treat symbolic floating point as symbolic int #11

Closed domainexpert closed 7 years ago

domainexpert commented 7 years ago

@Himeshi Added -floating-point-error option and renamed -debug-fp-error to -debug-floating-point-error. The -floating-point-error option enables the treatment of floating-point values as int values, including symbolic floating points. Although not semantically correct, this allows conditional branchings with conditions that depend on floating-point values to be explored.

domainexpert commented 7 years ago

@Himeshi From the examples of fp-examplesin fp-analysis/fp-examples#2, now both paths of get_sign_float.c and 6 paths of sterbenz.c are traversed.

domainexpert commented 7 years ago

@Himeshi This resolves issue #10 .

domainexpert commented 7 years ago

To check the semantics conformity (or measure divergence) to the actual floating-point interpretation of the code.

domainexpert commented 7 years ago

@Himeshi Maybe I'll merge this myself for now, but please check later.