Hi Mario, This is a really interesting project. I’m wondering about two things: 1. How do you introduce symbolic data? Does the Haskell program need to be manually instrumented with klee_make_symbolic calls? grep-ing through your repo, I didn’t find any --sym-arg(s) or klee_make_symbolic 2. How do you make KLEE behave concolically? While the terminology is not standardised, I think there’s some agreement that KLEE itself is not a concolic execution tool (despite what Wikipedia might suggest).
Paul > On 15 Jun 2015, at 02:04, Mario Alvarez Picallo <[email protected]> > wrote: > > Hello all, > > As a part of my Master's Thesis, I'm currently working on scher, a prototype > concolic testing framework for Haskell code that uses Klee under the hood. > > It uses the JHC haskell compiler, that compiles Haskell to surprisingly small > C programs that are then compiled to LLVM via llvm-gcc to be analyzed by Klee. > > Feel free to take a look at the current work, that you can find here > <https://github.com/m-alvarez/scher>, and tell me what you think, ask > questions, make requests or point out bugs (either via github's integrated > issue tracker or via mail). > > Cheers! > > -- > Now I do not know whether I was then a lambda expression emulating a Turing > machine, or whether I am a Turing machine emulating a lambda expression. > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
