[klee-dev] Write to symbolic position

[Cristian Cadar]

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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>