[klee-dev] How to solve silently concretizing in Klee

2015-01-25 Thread Peidong Chen
KLEE: WARNING ONCE: silently concretizing (reason: floating point) expression (ReadLSB w32 0 a) to value 0 (/home/admin-ubuntu/Development/Project/Klee/struct-test1.c:17) This is my source code: #include klee/klee.h #include stdio.h #include stdlib.h typedef struct{ int n; char c; float f;

[klee-dev] About klee error while compiling

2015-01-21 Thread Peidong Chen
Hello, I installed llvm-3.4 following the instructions in http://klee.github.io/experimental/ . And I followed the instructions in tutorial. The error is $clang-3.4 get_sign.c /tmp/get_sign-2a1cd5.o: In function `main': get_sign.c:(.text+0x78): undefined reference to `klee_make_symbolic' clang:

[klee-dev] klee test failures

2015-01-21 Thread Peidong Chen
I tried the No.9 step http://klee.github.io/experimental/ and it showed me Expected Passes: 155Expected Failures : 2Unsupported Tests : 1 It has 2 failures and 1 unsupported test. Does it matter? ___

[klee-dev] about struct klee test

2015-01-21 Thread Peidong Chen
Hello, I tried this .c file, but with many errors. This is my file. struct_test1.c #include klee/klee.h #include stdio.h typedef struct{ int n; char c; float f; }simple_struct; int struct_test1(simple_struct *s) { int ret; simple_struct *p; if(s-c=='a'){