On 15 October 2014 03:55, last first <[email protected]> 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.
#include <stdio.h>
int main(int argc, char** argv)
{
int width = 96;
int* sample_ptr=0;
int channels=1;
int alpha_row=0;
for (int i=0; i < width; ++i, sample_ptr += channels, ++alpha_row)
{
printf("i = %d, width = %d, ", i, width);
if (i < width) { printf("and (i < width) = %d\n", i < width); }
if (i > width) { printf("and (i > width) = %d\n", i > width); }
}
}
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
