[klee-dev] using KLEE with read()/write() instead of fread()/fwrite() or fscanf/fprintf

[ANAS faruqui]

I actually need KLEE to be working with read() function. Any ideas on how i
can achieve that.

I am trying to run KLEE on gzip.

The version of klee i am using is

 $ klee --version
Low Level Virtual Machine (http://llvm.org/):
  llvm version 2.9
  Optimized build with assertions.
  Built Jul 13 2013 (13:46:13).
  Host: i386-pc-linux-gnu
  Host CPU: i686

  Registered Targets:
    x86    - 32-bit X86: Pentium-Pro and above
    x86-64 - 64-bit X86: EM64T and AMD64

Thanks.





On Sun, Sep 15, 2013 at 1:45 PM, Daniel Liew <daniel.liew at imperial.ac.uk>wrote:

> I've seen klee hang before when fscanf is called but I forgot about
> it. Thanks for reminding me. I don't have time to look into it now but
> I've filled the fscanf hang bug on KLEE's new issue tracker on GitHub
> ( https://github.com/ccadar/klee/issues/30 ).
>
> I afraid I can't help you with the read() issue as I currently can't
> run KLEE (uclibc no longer compiles :( ) but hopefully someone else
> can.
>
> Thanks,
> Dan Liew.
>
> On 10 September 2013 22:53, ANAS faruqui <anas.faruqui at gmail.com> wrote:
> > Hi all,
> >
> > I am trying to run KLEE on gzip with symbolic files but klee seems to
> just
> > get stuck (even when giving the max-time parameter).
> >
> > So i wrote a small toy program to run klee on.
> >
> > At first trial i used fscanf function an klee got stuck on it as well.
> Then
> > when i changed the read function to fread(), everything worked fine and
> klee
> > generated the test cases.
> >
> > Then i used the read() function (which is used by gzip), and the klee
> just
> > prints one test case with all 0's.
> >
> > The command i am using is
> > klee --libc=uclibc --posix-runtime ./de.bc --sym-files 1 160 A
> >
> >
> >
> >
> > Any ideas how i can get the klee to work with  read() / gzip.
> >
> > I am attaching both the versions of my toy program.
> >
> > Thanks
> >
>
-------------- next part --------------
HTML attachment scrubbed and removed