Hi,
I've noticed one strange effect when caling special functions
with empty parameter list from interpreted code in KLEE.
Assume we add klee_warning2() which print a string to cerr.
lib/Core/SpecialFunctionHandler.h:
HANDLER(handleWarning2);
lib/Core/SpecialFunctionHandler.cpp:
add("klee_warning2", handleWarning2, false),
[..]
void SpecialFunctionHandler::handleWarning2(ExecutionState &state,
KInstruction *target,
std::vector<ref<Expr> >
&arguments) {
assert(arguments.size()==0 && "invalid number of arguments to
klee_warning2");
llvm::cerr << "klee warning 2\n";
}
Now let's take this example:
int main() {
int x = klee_int("x");
int y = klee_int("y");
if (x > 0) {
/* nop */
} else {
if (y > 0) {
klee_warning2();
} else {
klee_warning2();
}
}
return 0;
}
# klee test.o
KLEE: output directory = "klee-out-0"
KLEE: WARNING: undefined reference to function: klee_warning2
klee warning 2
KLEE: done: total instructions = 44
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
The function klee_warning2 is executed only once.
Let's make a small modification:
...
if (y > 0) {
++x;
klee_warning2();
} else {
...
# klee test.o
KLEE: output directory = "klee-out-2"
KLEE: WARNING: undefined reference to function: klee_warning2
klee warning 2
klee warning 2
KLEE: done: total instructions = 62
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3
Any ideas where it comes from?
I have many special functions with empty parameter list
and this issue does not occur in the older KLEE version.
Thanks,
Raimondas
--
Raimondas Sasnauskas, PhD Student
Distributed Systems Group
RWTH Aachen University
http://ds.cs.rwth-aachen.de/members/sasnauskas
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2498 bytes
Desc: not available
Url :
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20090611/74b95819/attachment.bin
