[klee-dev] KLEE doesn't work properly at loop statement.

[Daniel Liew]

On 15 October 2014 03:55, last first <idnrfc at gmail.com> wrote:
> 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 :
> 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.

> No need to understand much of codes, but the condition was given definitely.
> and result :
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.c
Type: text/x-csrc
Size: 421 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20141015/8aa4837a/attachment.bin>