Discussion:
KLEE doesn't work properly at loop statement.
(too old to reply)
last first
2014-10-15 02:55:09 UTC
Permalink
Hello guys.
I'm trying to learn and test some codes. and I just got a problem at loop
statements.
It seems like a bug since KLEE couldn't stop at the for_loop condition.
check it first :
Loading Image...
No need to understand much of codes, but the condition was given definitely.
and result :
Loading Image...
This picture is part of process that when KLEE is running.
i and width Two values are same type and I can make this process work
properly by editing some codes but I think that's not a good solution since
it happened and don't know where it could show up.
Any idea or suggestions please?

Thanks.
Daniel Liew
2014-10-15 10:04:27 UTC
Permalink
Post by last first
Hello guys.
I'm trying to learn and test some codes. and I just got a problem at loop
statements.
It seems like a bug since KLEE couldn't stop at the for_loop condition.
http://i.imgur.com/ixzVlt2.png
Please don't send pictures of code or terminal output. It's not very
helpful. Attach the output as files (if they are small) or use
pastebin, Gist or a similar service instead.
Post by last first
No need to understand much of codes, but the condition was given definitely.
http://i.imgur.com/9p67EE0.png
Seeing as you sent me a picture of code rather than the code itself I
tried reconstructed the program from the picture (see attached) and I
cannot reproduce the issue. The loop terminates.

Note I'm using Clang (LLVM3.4).

To diagnose further you need to send us the program with the loop that
does not terminate.

Loading...