Hi Fatih, I think you have only one option if the symbolic value is manipulated by the library function. You have to compile your external library to LLVM and link using llvm- ld. However, if this happens just for a function, maybe you can write a model for what the library function does and replace the real function with the model (see the filesystem model).
You can probably take a look at previous threads on a slightly similar topic such as this one: http://keeda.stanford.edu/pipermail/klee-dev/2009-February/000016.html Hope this helps. Cristi On Jul 21, 2009, at 12:07 AM, M. Fatih BOYACI wrote: > Hi all; > > When i want to symbolically execute a program in which a symbolic > variable is manipulated by an external library function call, how > should i link the external library as part of > the llvm compilation process for this program. > > for example: > given a symbolic variable lets say "msg". > > it is manipulated like msg = dn_comp (...) where dn_comp is part of > an external library. > i get the error "KLEE: ERROR: failed external call:__dn_comp" > > -- > Mehmet Fatih BOYACI > UIllinois at Urbana-Champaign > PhD Candidate, Computer Science > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
