[klee-dev] FilePerm.c test fails

[Emil Rakadjiev]

Hello Cristian and Daniel,

Thank you for the replies!

The -no-truncate-source-lines argument fixes the issue with the assembly files, and opt generates nice CFGs. KCachegrind seems to show the same results with and without that argument (I checked for FilePerm.c and FD_Fail2.c).

What are the 3 FilePerm.c test cases that KLEE generates for you? Should close() on a symbolic file branch? If yes, then this would indeed result in 3 test cases:
1) open() == -1
2) open() != -1 && close() == -1
3) open() != -1 && close() == 0
For me only 1) and 3) are explored.

Also, could you explain please why stdout is declared symbolic? What effect does this have?

> But I noticed that you run the test with uclibc enabled, while the default configuration is to run w/o uclibc. Have you changed some of the default options?

Cristian, yes, I was trying various things, and the output I posted in my first message was with uclibc included. I noticed this later and in the PS of my second message I mentioned it, and attached the output with the default parameters (results are the same, though).

Thanks and best regards,
Emil