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
