Hi Cristi, That's indeed how we replay things, only that we have some additional wrappers to make sure that we replay in the very same environment (same sandbox directory, same environment variables etc.) Maybe you're running into such an inconsistency? Other than that, I'm not sure what the problem could be. Unfortunately, using gdb w/ ptrace it's indeed tricky. There's the --no-fail option to run-bout, for the common non-failing case, but I don't think it's still working (but that should be easy to fix).
If you're not using the environment, I recommend replaying by linking with klee-runtest.o, and setting the environment variable KLEE_RUNTEST to point to the .bout file you want to run. --Cristian On Wed, 2009-01-28 at 00:09 +0100, Cristian Zamfir wrote: > > Hi, > > I am playing with the replay environment and I have a few questions. > First of all, how do you run? For instance for cat, do you run with > run-bout ../cat testxyz.bout ? > > When I run this way, I get the ERROR: make_symbolic mismatch, > different sizes so I assume the first parameter is not correct. > > Also, your replay environment runs the program with the same program > arguments as in the test case, initializes the symbolic environment > (at the moment these are the files from the symbolic file system) and > uses ptrace to handle file related syscalls and fail system calls. > Since you are already using ptrace and gdb uses ptrace too, I am > wondering if it is still possible to replay inside gdb and valgrind. > Did you experiment with that? I think this should still be possible if > I attach gdb after running run-bout but I cannot try this at the > moment because of the above error. > > Thanks for the help. > > Cristi > > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.Stanford.EDU > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
