Hi, all,
I have followed the tutorial below which is used to test the function
"match" , but i found that the generated tests cannot cause memory errors.
Second tutorial: Testing a simple regular expression library.
(the website is: http://klee.github.io/tutorials/testing-regex/)
the main code is:
int main() {
// The input regular expression.
char re[SIZE];
// Make the input symbolic.
klee_make_symbolic(re, sizeof re, "re");
// Try to match against a constant string "hello".
match(re, "hello");
return 0;
}
the output is:
KLEE: Using STP solver backend
KLEE: ERROR:
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp.c:23: memory
error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR:
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp.c:25: memory
error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 4598603
KLEE: done: completed paths = 7438
KLEE: done: generated tests = 16
As reported, there are two errors occured.
And the error information is in two files in the below:
The data in test000007.ktest is:
I read the source code of ktest-tool and know the following bytes in red circle
are the data which are generated to assign the array "re".
So I change the file Regexp.c as below
int main() {
// The input regular expression.
char re[SIZE];
re[0]=0x5E;
re[1]=0x01;
re[2]=0x2A;
re[3]=0x01;
re[4]=0x2A;
re[5]=0x01;
re[6]=0x2A;
// Make the input symbolic.
//klee_make_symbolic(re, sizeof re, "re");
//klee_assume(re[SIZE - 1] == '\0');
// Try to match against a constant string "hello".
match(re, "hello");
return 0;
}
After compiling using gcc, i use valgrind to check it, the result is:
valgrind --tool=memcheck --leak-check=full ./Regexp3
==19827== Memcheck, a memory error detector
==19827== Copyright (C) 2002-2015, and GNU GPL'd, by Julian Seward et al.
==19827== Using Valgrind-3.12.0 and LibVEX; rerun with -h for copyright info
==19827== Command: ./Regexp3
==19827==
==19827== Conditional jump or move depends on uninitialised value(s)
==19827== at 0x4005EF: matchhere (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
==19827== by 0x400680: matchhere (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
==19827== by 0x400582: matchstar (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
==19827== by 0x400610: matchhere (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
==19827== by 0x400582: matchstar (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
==19827== by 0x400610: matchhere (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
==19827== by 0x4006BB: match (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
==19827== by 0x400739: main (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
==19827==
==19827==
==19827== HEAP SUMMARY:
==19827== in use at exit: 0 bytes in 0 blocks
==19827== total heap usage: 0 allocs, 0 frees, 0 bytes allocated
==19827==
==19827== All heap blocks were freed -- no leaks are possible
==19827==
==19827== For counts of detected and suppressed errors, rerun with: -v
==19827== Use --track-origins=yes to see where uninitialised values come from
==19827== ERROR SUMMARY: 1 errors from 1 contexts (suppressed: 0 from 0)
klee@ubuntu:~/xiaojiework/kleeexperiment/examples/regexp$
Nothing about out of bound pointer is found. only one error which is about
using uninitialised value(s).
I doubt that maybe I was wrong in some steps. So I use the following script
which is offered by the klee website
export
LD_LIBRARY_PATH=/home/klee/xiaojiework/klee-xiaojie/build/debug/lib/:$LD_LIBRARY_PATH
gcc -L /home/klee/xiaojiework/klee-xiaojie/build/debug/lib/ Regexp.c
-lkleeRuntest
valgrind --tool=memcheck ./a.out
During execution, it needs to type in the ktest file path manually.
The result is as below and nothing wrong about out of bound pointer is found.
==19176== Memcheck, a memory error detector
==19176== Copyright (C) 2002-2015, and GNU GPL'd, by Julian Seward et al.
==19176== Using Valgrind-3.12.0 and LibVEX; rerun with -h for copyright info
==19176== Command: ./a.out KTEST_FILE=klee-last/test000007.ktest
==19176==
KLEE-RUNTIME: KTEST_FILE not set, please enter .ktest path:
klee-last/test000007.ktest
==19176== Conditional jump or move depends on uninitialised value(s)
==19176== at 0x400796: matchhere (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/a.out)
==19176== by 0x400742: matchstar (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/a.out)
==19176== by 0x4007D0: matchhere (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/a.out)
==19176== by 0x400742: matchstar (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/a.out)
==19176== by 0x4007D0: matchhere (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/a.out)
==19176== by 0x400742: matchstar (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/a.out)
==19176== by 0x4007D0: matchhere (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/a.out)
==19176== by 0x40087B: match (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/a.out)
==19176== by 0x4008F3: main (in
/home/klee/xiaojiework/kleeexperiment/examples/regexp/a.out)
==19176==
==19176==
==19176== HEAP SUMMARY:
==19176== in use at exit: 92 bytes in 6 blocks
==19176== total heap usage: 7 allocs, 1 frees, 660 bytes allocated
==19176==
==19176== LEAK SUMMARY:
==19176== definitely lost: 0 bytes in 0 blocks
==19176== indirectly lost: 0 bytes in 0 blocks
==19176== possibly lost: 0 bytes in 0 blocks
==19176== still reachable: 92 bytes in 6 blocks
==19176== suppressed: 0 bytes in 0 blocks
==19176== Rerun with --leak-check=full to see details of leaked memory
==19176==
==19176== For counts of detected and suppressed errors, rerun with: -v
==19176== Use --track-origins=yes to see where uninitialised values come from
==19176== ERROR SUMMARY: 1 errors from 1 contexts (suppressed: 0 from 0)
Am I wrong?Maybe i was too uncareful in some steps, but i cannot found where i
operate wrongly by myself. Hope for your help!
7FF9E532@1A9ED30C.17D90E59.png
Description: Binary data
ED774A2A@761B3E10.17D90E59.png
Description: Binary data
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
