Re: [klee-dev] Asking for Help about Klee3.4 on docker

*After I terminated ptx.bc, I got* ^CKLEE: ctrl-c detected, requesting interpreter to halt. KLEE: halting execution, dumping remaining states KLEE: done: total instructions = 115911 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 *I am sure the number of total instructions is

Re: [klee-dev] Asking for Help about Klee3.4 on docker

*Hi Andrea,* *Thank you for your help, I have fixed the problem.* *But I have a question, about testing the coreuitls.* *Usually when I run the test for some .bc files, klee will return the result.* *Like seq.bc :* klee@3cc1aa045534:~/test/coreutils-6.11/obj-llvm/src$ klee --libc=uclibc

Re: [klee-dev] Asking for Help about Klee3.4 on docker

Hi, please remember to always include the mailing list address when replying. I would try to run configure and run by explicitly saying what compiler you want to use: klee@00934a05ada8:obj-llvm$ LLVM_COMPILER=clang CC=/home/klee/whole-program-llvm/wllvm ../configure --disable-nls CFLAGS="-g”

Re: [klee-dev] how to know if variable is symbolic

On 17 March 2016 at 17:18, Sumit Kumar wrote: > Hi, > I want to know if there is a way to know if a variable is symbolic or not in > KLEE when KLEE is executing an instruction involving the variable. Within the application it self you can call ``klee_is_symbolic()``.

[klee-dev] how to get this constraint in klee

Hi, Can anyone please help me. This is what I want to do in KLEE: 'x', 'y' are integer symbolic variables. Now the following statement is executed: x = y; If after this statement any constraint in KLEE involves x then the value of x is taken as: "ReadLSB w32 0 y" but I want that

Re: [klee-dev] How can I get KLEE to generate constraints from within function calls

On 18 March 2016 at 15:00, Sumit Kumar wrote: > Hi, > > My test program is this: I declare 'x' as symbolic and then pass the address > / value of x as argument to function foo like foo(x) or foo(). Inside the > function foo no variables have been explicitly made symbolic.

Re: [klee-dev] "search" text box in this page does not work

Please use this website: http://mailman.ic.ac.uk/pipermail/klee-dev/ Andrea > On 19 Mar 2016, at 09:15, Sumit Kumar wrote: > > "search" text box in this page does not work: > > http://klee-dev.keeda.stanford.narkive.com/ >

Re: [klee-dev] how to get this constraint in klee

I think you can't.In KLEE, each state is represented as a mapping of program variables to an expression in terms of initial symbolic values.This is probably better in terms of performance as the number of program variables is likely to be smaller than the length of the path. Storingthe