Hi Weiqi,
Note that such an assignment does not impose any constraints on the
input, which is why you don't see them in the path constraints
(otherwise a simple code snippet such as buf[1] = '9'; buf[2] = '0'
would be considered infeasible). You might want to check the initial
KLEE paper for more details.
Best,
Cristian
On 26/08/2021 14:55, Weiqi Wang wrote:
Hi,
I’m wondering whether klee generate constraints when a concrete value is
written to symbolic position? I tried a toy program and it seemed klee
doesn’t. Specifically, I added a `buf[1] = ‘9’ before the password check
in check_password(). But I only get constraint: (Eq 104 (Read w8 0
A-data)) due to short-circuit evaluation. What I would like to see are
two constriants: (Eq 104 (Read w8 0 A-data)) and (Eq 57 (Read w8 1 A-data))
Is there an easy way to add this feature? Could you give me some hint on
which file to modify?
Best,
Weiqi
_______________________________________________
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
