Hi Andriy, We have an upcoming CAV paper on this topic. Check it out at http://keeda.stanford.edu/~daramos/ucklee-cav-2011.pdf. Unfortunately, our UC-KLEE repository is unstable and not currently released to the public. Hopefully that will change at some point.
-David On Jun 8, 2011, at 12:10 AM, Andriy Gapon wrote: > > 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 > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
