search

ApproxSymate / klee

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

Keep track of error expressions of all program variables in a global map #71

Closed Himeshi closed 6 years ago

Himeshi commented 6 years ago

At present, to get the error expressions out for the program variables, klee_bound_error calls must be inserted into the program. To reduce manual intervention and automate the process even further, keep track of program variables (with their local allocation) and their error expressions and for each path output the final expression when the klee execution has finished.

domainexpert commented 6 years ago

@Himeshi Do you have an example for testing if one is to implement this feature?

Himeshi commented 6 years ago

@domainexpert Sorry, saw this comment only today. I was working on this and I tested it with add_test.c and it seems to be working fine. However for arrays it doesn't seem to be producing the expressions correctly, which is what I'm debugging now.

There is a WIP pull request here: https://github.com/fp-analysis/klee/pull/80

domainexpert commented 6 years ago

Resolved via #80.