I do not know the scope of the group. The subject was originally posted to the KLEE mailing list. It probably is appropriate to maintain it within the list
Below is my comment to the blog post at ( http://blog.regehr.org/archives/388 ) You seem to be describing in the blog post what in the world of ARINC DO-178 are called robustness tests. In a sense they server to probe the fidelity limits of the algorithm as opposed to the logic of the implementation. That is (in my opinion) the behavior of the algorithm as the assumption limits are approached. Were the algorithm intended to perform a numeric integration, one might wonder about the behavior when applied against the inverse function (1/x) on the integration range [0,1]. Hopefully the computation would yield a numeric overflow or a divide by 0 error. (What does it mean if the result is just a large but finite floating point number?) I am not a compiler writer type, but suspect that code transformation rewrite strategies may be useful here. That is in your example add_and_shift can either be treated as an op code of a virtual machine, or as a macro of a preprocessor By treating it as a macro it can be used to prepare any algorithm which serves to consistently implement the instruction. Conceivably the macro could generate C code with implements a very robust error evaluation of the computation (ie includes if statements which check all those nasty computation errors). One might even consider a family of macros, each imposing different degrees of rigor in the error checks. Naturally when that code is compiled and then run thru a path runner like KLEE additional test cases would be generated. (because there are now additional paths) One might even consider having pragmas to selectively control the rigor of the path analysis considered. dbl > -----Original Message----- > From: klee-dev-bounces at keeda.stanford.edu [mailto:klee-dev- > bounces at keeda.stanford.edu] On Behalf Of John Regehr > Subject: [klee-dev] blog post about combining klee with integer undefined > behavior checks > > Possibly interesting to folks here: > > http://blog.regehr.org/archives/388 > > John > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
