Hi,
I switched to using klee-replay instead of setting the env, and now the test
case seem to run correctly, but I'm a bit confused by some of the output.
test case:
#include <stdlib.h>
#include <string.h>
#include <fcntl.h>
#include <unistd.h>
void func(char *userInput) {
char arr[8];
strcpy(arr, userInput);
}
int main(int argc, char *argv[]){
int res, fd = -1;
char arr[16];
if(argc < 2)
goto label;
fd = open(argv[1], O_RDONLY);
if(fd < 0)
goto label;
res = read(fd, arr, 16);
func(arr);
return 0;
label:
printf("err\n");
return 0;
}
I'm using --sym-arg 10 --sym-files 1 20 20
This generates a bunch of test cases that all pretty much act as expected,
except for the one that "overruns" the buffer in func. That test case
generates a .ptr.err file that shows what I expect: overruning the buffer in
func.
However, ktest-tool on that test case indicates that the file (A data) is
all nulls, which would clearly not cause this error. Additionally, when I
run klee-replay, it generates a file A which in all test cases matches what
ktest-tool claims for that test case. Thus if I run the compiled binary on
the file A generated by klee-replay for the crashing test case, it does NOT
crash, whereas with klee-replay it DOES crash where expected (after copying
outside of the buffer in func, the signal depends on what particular value
was written over the buffer)
What am I missing?
Thanks,
On Tue, Feb 9, 2010 at 2:31 AM, Daniel Dunbar <daniel at zuster.org> wrote:
> Hi David,
>
> Without more information its hard for me to know what might be happening
> here.
>
> Is it possible to find a small test case?
>
> - Daniel
>
> On Sun, Feb 7, 2010 at 1:40 PM, David <dkohlbre at cmu.edu> wrote:
> > Hi,
> > I've been doing some work with analyzing the predicates for certain test
> > cases that Klee generates and I've noticed some odd behavior with
> sym-files.
> >
> > When I set the klee run to use sym-files and during one of the paths it
> > encounters a pointer error, the .pc file and the .ktest file generated
> for
> > that test case are incorrect.
> > Specifically, the kquery for the actual data in the symbolic file is
> blank,
> > and the test case data for the file is all nulls. If I run the test case,
> > the program does not crash (as the test case claims to cause.)
> >
> > On that same run of klee, test cases that did not encounter a pointer
> error
> > have correct kquery and test case data for the symbolic file; only test
> > cases that purport to result in a crash are 'empty'.
> >
> > Any pointers as to whats going wrong?
> >
> >
> > Thanks,
> > --
> > -David Kohlbrenner
> >
> > _______________________________________________
> > klee-dev mailing list
> > klee-dev at keeda.stanford.edu
> > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
> >
> >
>
--
-David Kohlbrenner
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100215/962fd651/attachment.html
