The current format supported is in smt2, so use --write-smt2s which will produce a smt2 file
On Tue, Mar 23, 2021 at 6:46 PM Bharat Garhewal <b.garhe...@cs.ru.nl> wrote: > I used: > > klee -write-kqueries --libc=uclibc --posix-runtime --external-calls=all > --seed-out=file.bout example.bc > On 23/03/2021 11:43, Ridwan Shariffdeen wrote: > > Hi > What's the Klee command you used > > On Tue, Mar 23, 2021, 6:40 PM Bharat Garhewal <b.garhe...@cs.ru.nl> wrote: > >> Dear Ridwan, >> >> Thank you for the link! I'm trying to use your KLEE fork (from GitHub, >> not the DockerHub), but I'm unable to capture the information that I want. >> >> For instance, I've consider the following code: >> >> #include <stdio.h> >> #include <stdlib.h> >> #include </klee/source/include/klee/klee.h> >> >> int main(){ >> int k; >> klee_make_symbolic(&k, sizeof(k), "k"); >> if (k == 20) >> printf("Statement Five\n"); >> else >> printf("Statement Six\n"); >> >> printf("\nk=%d\n", k); >> return 0; >> >> } >> >> I generate the seed file with: gen-bout --second-var model_version 4 01 >> --second-var k 4 20 >> >> However, the kquery file I get is: >> >> array k[4] : w32 -> w8 = symbolic >> array model_version[4] : w32 -> w8 = symbolic >> (query [(Eq 1 >> (ReadLSB w32 0 )) >> (Eq 20 <---------- I would >> expect 'k' here >> (ReadLSB w32 0 ))] >> false) >> >> Is this the expected behaviour, or perhaps I am doing something wrong? >> >> Regards, >> >> Bharat >> On 13/03/2021 12:33, Ridwan Shariffdeen wrote: >> >> Hi, >> >> What you are looking for is for a concolic execution. I have a modified >> version of KLEE to get what you want. >> You can refer to the repo >> https://github.com/rshariffdeen/klee/tree/concolic and build KLEE. There >> is also a docker image hosted at dockerhub rshariffdeen/klee:concolic which >> is already built. >> >> Then using seed-file, you can feed the concrete input and it willl be >> executed concretely but capturing the symbolic constraints you need. If you >> are not familiar with see-file setting, I can let you know how to use for >> one example. >> Let me know, if you have any questions or if this works for you >> >> Regards >> >> On Fri, Mar 12, 2021 at 9:42 PM Bharat Garhewal <b.garhe...@cs.ru.nl> >> wrote: >> >>> Dear all, >>> >>> I'm working on (white-box/grey-box) Active Automata Learning for >>> programs with data parameters >>> (i.e., our automata contain data parameters in guards and in i/o). >>> We require that for each concrete query, we can extract data (i.e., >>> path) constraints for that query. >>> For instance, consider that we have a one-element FIFO buffer with two >>> actions: PUSH(p) and POP(p): >>> Given a query of the form ``PUSH(p1=5) POP(p2=3)'' (where p1 and p2 are >>> the "markers"/"names" given >>> to 5 and 3), we want to retrieve the constraint "p1 =/= p2" from the >>> path followed by the program >>> (assuming that the comparison between 5 and 3 actually happens in the >>> program). We're trying >>> to obtain these PC using KLEE. >>> >>> I've been trying to get concrete inputs working with KLEE (latest docker >>> build) and Zesti (docker, from https://github.com/rshariffdeen/zesti), >>> but I guess I'm doing something wrong. >>> For instance, consider the "Tutorial One" example, get_sign, with no >>> changes to the source code. >>> If I run it with klee-zesti, as "klee-zesti -posix-runtime -libc=uclibc >>> get_sign.bc 22", It would expect to explore only one branch, but I somehow >>> end up exploring 10? >>> >>> With Zesti (if anyone has any idea), I still end up exploring all 3 >>> branches of the function. >>> Does anyone have any clues on how to get this working? (Either KLEE or >>> Zesti would be fine :)) >>> >>> Thank you, >>> Regards, >>> Bharat Garhewal, >>> ICIS - SWS, >>> Radboud University >>> _______________________________________________ >>> klee-dev mailing list >>> klee-dev@imperial.ac.uk >>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >>> >>
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev