search

ApproxSymate / klee

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

Symbolic indices/pointers support #46

Closed domainexpert closed 6 years ago

domainexpert commented 7 years ago

This can be supported by having the error expression represented using ite expression.

domainexpert commented 7 years ago

@Himeshi One of the examples that crashes due to the inability to handle symbolic indices is jpeg.c of fp-analysis/fp-examples#20. The symbolic read is at Line 2341 of jpeg.c.

domainexpert commented 6 years ago

@Himeshi #58 fixed the crash, but as mentioned in the meeting, we would need to add an option to disable approximability of symbolic indices.

domainexpert commented 6 years ago

The issue of disabling of symbolic indices approximability should be a separate PR/issue. Closing this one for now.