Hi Neha, The symbolic model options are parsed by the modeling bitcode, not the KLEE VM itself. So, you need to place these options *after* the .bc file. KLEE inserts a new main() function that reads these options, sets up the symbolic environment, and then invokes the test program's main() function. It might be helpful to examine runtime/POSIX/klee_init_env.c, which is where the options are parsed.
I believe this interface was changed shortly after the 2008 OSDI paper. The new invocation would be something like: $ klee -max-time 2 tr.bc -sym-args 1 10 10 -sym-files 2 2000 -max-fail 1 -David On Oct 10, 2012, at 12:44 PM, Neha Rungta wrote: > We did try that as well and klee says it does not understand -sym-args > -sym-files > > Neha > > On Wed, Oct 10, 2012 at 12:13 PM, Jonathan Neuschäfer <[email protected]> > wrote: > On Wed, Oct 10, 2012 at 11:38:03AM -0700, Neha Rungta wrote: > > Hi > > > > Is there some documentation to handle symbolic file I/O in klee? The > > commands that I found online do not seem to work as I would expect them to. > > > > http://static.usenix.org/event/osdi08/tech/full_papers/cadar/cadar_html/ > > > > says to use* > > * > > > > * klee -max-time 2 -sym-args 1 10 10 -sym-files 2 2000 -max-fail 1 tr.bc > > * > > > > * > > 4<http://static.usenix.org/event/osdi08/tech/full_papers/cadar/cadar_html/#foot1113>The > > option -sym-files 2 2000 says to use standard input and one file, each > > holding 2000 bytes of symbolic data.* > > > > I am looking to specify the above in the latest klee version. Pointers for > > that would be much appreciated. > > > > Neha > > AFAIK you'll also need to pass "-libc=uclibc" and "-posix-runtime" to > klee (see "klee --help" output). > > HTH, > Jonathan Neuschäfer > > > > -- > ------------------------------------------------- > Neha Rungta, Ph.D > SGT/NASA Ames Research Center > http://ti.arc.nasa.gov/profile/nrungta/ > -------------------------------------------------- > _______________________________________________ > klee-dev mailing list > [email protected] > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
