I wonder if KLEE provides an easy way to verify that a code change doesn't actually change any functionality. That is, that given some input output would remain the same. This would be very useful to check changes that are non-trivial but which are supposed to only clean up or refactor code without changing its logic.
A practical example. It seems that a regression was introduced in this change: http://cgit.freedesktop.org/xorg/driver/xf86-video-ati/commit/?id=53ac06161eb2 I've looked through the tutorials but I am not sure what kind of test harness I need to create here. Mostly I am not sure how to mark the shared state structure radeon_accel_state as having symbolic values. Any help will be greatly appreciated. Thank you in advance! -- Andriy Gapon
