I don't think the regress test cases have much value. They take a while to run and don't really contain much in the way of checking actual correctness. I would prefer that they turn into proper tests which actually check features, or are killed off.
Mass "test that we simulate paths correctly" style testing is better left to larger application suites anyway. - Daniel 2009/2/7 Philip Guo <pg at cs.stanford.edu>: > when i try running 'make regress' in klee/, it doesn't work at all. all it > seems to do is to go into klee/regression and run 'make' in there. is that > a regression suite that you guys have been actively maintaining, or is it > deprecated? thanks. > > there are lots of errors of the following form: > > $ make regress > make -C regression > make[1]: Entering directory `/home/pgbovine/klee-uc/regression' > -- Testing: alias-to-symbolic-01 -- > make[2]: *** No rule to make target `Output/alias-to-symbolic-01.runtest', > needed by `test'. Stop. > fail: alias-to-symbolic-01 -- make failed > -- Testing: apr-snprintf -- > make[2]: *** No rule to make target `Output/apr-snprintf.runtest', needed by > `test'. Stop. > fail: apr-snprintf -- make failed > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.Stanford.EDU > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > >
