Re: [klee-dev] Error while replaying .path file
***
This email originates from outside Imperial. Do not click on links and
attachments unless you recognise the sender.
If you trust the sender, add them to your safe senders list
https://spam.ic.ac.uk/SpamConsole/Senders.aspx to disable email stamping for
this address.
***
Thanks Cristian for this information. Klee reply will not work in my case
because
I have to replay the test case with path files only.
On Tue, Feb 18, 2020, 5:06 PM Cadar, Cristian
wrote:
> Hi Awanish,
>
> Unfortunately that feature has not been maintained -- we need to fix it,
> but there are no immediate plans to do so.
>
> You may be able to achieve something similar via seeding (-seed-file).
> Or if you just want to replay the test case, use klee-replay or link
> with the libkleeRuntest library (see the tutorials).
>
> Best,
> Cristian
>
> On 18/02/2020 07:47, Awanish Pandey wrote:
> > Dear all,
> > I want to replay a path file, but I am getting an assertion
> > violation "hit an invalid branch in replay path mode".
> >
> > This is my toy program
> > /int main(int argc, char *argv[]){
> >if (argc != 2){
> > printf("error:");
> >}
> >int a;
> >FILE *fp = fopen(argv[1], "r");
> >fscanf(fp,"%d",&a);
> >if (a == 10)
> > assert(0);
> >fclose(fp);
> >return 0;
> > }/
> >
> > I run klee "/klee --libc=uclibc --posix-runtime --write-paths file.bc
> > --sym-arg 1 --sym-files 1 5/".
> > It finds an assertion violation (at test case number 19) and when I
> > replayed it by command
> > /klee --libc=uclibc --posix-runtime
> > --replay-path=klee-out-0/test19.path file.bc/
> >
> > Klee crashes on assertion violation in Executor.cpp
> >
> > What is the issue? It will be very helpful.
> > --
> > Thanking You
> > Awanish Pandey
> >
>
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Error while replaying .path file
***
This email originates from outside Imperial. Do not click on links and
attachments unless you recognise the sender.
If you trust the sender, add them to your safe senders list
https://spam.ic.ac.uk/SpamConsole/Senders.aspx to disable email stamping for
this address.
***
Dear all,
I want to replay a path file, but I am getting an assertion violation "hit
an invalid branch in replay path mode".
This is my toy program
*int main(int argc, char *argv[]){ if (argc != 2){printf("error:");
} int a; FILE *fp = fopen(argv[1], "r"); fscanf(fp,"%d",&a); if (a ==
10)assert(0); fclose(fp); return 0;}*
I run klee "*klee --libc=uclibc --posix-runtime --write-paths file.bc
--sym-arg 1 --sym-files 1 5*".
It finds an assertion violation (at test case number 19) and when I
replayed it by command
*klee --libc=uclibc --posix-runtime
--replay-path=klee-out-0/test19.path file.bc*
Klee crashes on assertion violation in Executor.cpp
What is the issue? It will be very helpful.
--
Thanking You
Awanish Pandey
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Running SPEC benchmarks with klee
*** This email originates from outside Imperial. Do not click on links and attachments unless you recognise the sender. If you trust the sender, add them to your safe senders list https://spam.ic.ac.uk/SpamConsole/Senders.aspx to disable email stamping for this address. *** Dear all, I tried to run SPEC benchmarks with klee but I found that they require highly formatted input. Is there any way to handle these situations? Does anyone have previously rewritten the parsing code of SPEC benchmarks with insertion of klee_assume for removing useless execution. Any other different way to tackle this situation is welcomed. -- Thanks and Regards Awanish Pandey PhD, CSE IIT Kanpur ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Replay ktestfile directory
Hi, I run klee over the coreutils using the command mentioned in coreutils experiments. When I replay the using -replay-ktest-dir="---" it is giving warning "KLEE: WARNING ONCE: replay did not consume all objects in test input. " Out of 156 test cases in ptx replay was able to run only 6 test cases. What is the problem or I am doing something wrong -- Thanking You Awanish Pandey PhD, CSE IIT Kanpur ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Branch on data of symbolic file
Hi everyone, I have written a code like this fp = fopen(argv[1],"r") read(fp,c,1); if(c == 48) assert(0) I compiled this and run it arg sym-file 1 10 allow-external-sym-calls and libc=uclibc. But klee is not able to find the crash. What I am missing due to which crash is not found? -- Thanking You Awanish Pandey PhD, CSE IIT Kanpur ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Getting path formula in dimacs format
Hi, I want to get/convert path constraint into dimacs/SAT format. Is there any way to convert in the desired form? -- Thanks and Regards Awanish Pandey PhD, CSE IIT Kanpur ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Running latest coreutils with klee build on llvm3.4
Hi everyone, I used wllvm and it works. But it creates binary then extract-bc provide us bitcode. If I am adding klee_make_symbolic() in coreutils source code wllvm can't produce binary so unable to generate bitcode file. Is there any way to generate bc file for coreutils which contain klee_make_symbolic from llvm3.4 version? -- Thanking You Awanish Pandey PhD, CSE IIT Kanpur ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Running grep with klee
Hi Everyone, I compiled grep source code with both llvm2.9 and llvm-3.4, then try to run on corresponding klee. In both the cases output is same but not the desired one. LLVM ERROR: invalid argument to evalConstant(). Anyone have Idea what I am doing wrong in this? Complete output is this. KLEE: NOTE: Using klee-uclibc : /home/awanish/git/duklee/build/Release+Asserts/lib/klee-uclibc.bca KLEE: WARNING: undefined reference to function: __ctype_b_loc KLEE: WARNING: undefined reference to function: __ctype_tolower_loc KLEE: WARNING: undefined reference to function: __ctype_toupper_loc KLEE: WARNING: undefined reference to function: __fxstat KLEE: WARNING: undefined reference to function: __fxstatat KLEE: WARNING: undefined reference to function: __getdents KLEE: WARNING: undefined reference to function: __lxstat KLEE: WARNING: undefined reference to function: __overflow KLEE: WARNING: undefined reference to function: __strdup KLEE: WARNING: undefined reference to function: __strtol_internal KLEE: WARNING: undefined reference to function: __uflow KLEE: WARNING: undefined reference to function: __xstat KLEE: WARNING: undefined reference to function: access KLEE: WARNING: undefined reference to function: bindtextdomain KLEE: WARNING: undefined reference to function: chdir KLEE: WARNING: undefined reference to function: close KLEE: WARNING: undefined reference to function: creat KLEE: WARNING: undefined reference to function: dcgettext KLEE: WARNING: undefined reference to function: fchdir KLEE: WARNING: undefined reference to function: fcntl KLEE: WARNING: undefined reference to function: fdopendir KLEE: WARNING: undefined reference to function: fstat KLEE: WARNING: undefined reference to function: fstatfs KLEE: WARNING: undefined reference to function: iconv KLEE: WARNING: undefined reference to function: iconv_close KLEE: WARNING: undefined reference to function: iconv_open KLEE: WARNING: undefined reference to function: ioctl KLEE: WARNING: undefined reference to function: lseek KLEE: WARNING: undefined reference to function: lseek64 KLEE: WARNING: undefined reference to function: open KLEE: WARNING: undefined reference to function: openat KLEE: WARNING: undefined reference to function: pcre_assign_jit_stack KLEE: WARNING: undefined reference to function: pcre_compile KLEE: WARNING: undefined reference to function: pcre_exec KLEE: WARNING: undefined reference to function: pcre_fullinfo KLEE: WARNING: undefined reference to function: pcre_jit_stack_alloc KLEE: WARNING: undefined reference to function: pcre_jit_stack_free KLEE: WARNING: undefined reference to function: pcre_maketables KLEE: WARNING: undefined reference to function: pcre_study KLEE: WARNING: undefined reference to function: pipe KLEE: WARNING: undefined reference to function: pthread_mutex_init KLEE: WARNING: undefined reference to function: pthread_mutexattr_destroy KLEE: WARNING: undefined reference to function: pthread_mutexattr_init KLEE: WARNING: undefined reference to function: pthread_mutexattr_settype KLEE: WARNING: undefined reference to function: read KLEE: WARNING: undefined reference to function: splice KLEE: WARNING: undefined reference to function: textdomain KLEE: WARNING: undefined reference to function: write LLVM ERROR: invalid argument to evalConstant() -- Thanks and Regards Awanish Pandey PhD, CSE IIT Kanpur ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Running Apache server with KLEE
Hi, I compiled apache with llvm2.9 and when I am running it with command klee --libc=uclibc --posix-runtime httpd.bc It emitting error which says KLEE: ERROR: /home/awanish/git/angelix/build/klee-uclibc/libc/inet/socketcalls.c:362: inline assembly is unsupported Can anyone please suggest me where I am doing wrong? -- Thanks and Regards Awanish Pandey PhD, CSE IIT Kanpur ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Error in make check
Hi, I configured klee with this command ../configure --with-llvmsrc=/home/awanish/llvm-2.9/llvm-2.9 --with-llvmobj=/home/awanish/llvm-2.9/llvm-2.9/build --with-stp=/usr/local --with-uclibc=/home/awanish/klee-uclibc/ --enable-posix-runtime then did make DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 ENABLE_SHARED=0 -j2 which ends without error. But when I did make check it says Expected Passes: 93 Expected Failures : 2 Unsupported Tests : 4 Unexpected Failures: 84 is it correct or I am missing something. Please help me out and thanks in advance. -- Thanks and Regards Awanish Pandey PhD, CSE IIT Kanpur ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
