Re: [klee-dev] Error while replaying .path file

2020-02-18 Thread Awanish Pandey

***
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",);
> >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


Re: [klee-dev] Error while replaying .path file

2020-02-18 Thread Cadar, Cristian
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",);
>    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

2020-02-17 Thread Awanish Pandey

***
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",);  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