[klee-dev] How to restrict the character space of symbolic string

Loi Luu loi.luuthe at gmail.com
Mon Sep 16 10:16:34 BST 2013


Thank you Daniel. I think we should insert | (c == '\0') in the above
example. Anw, that's a great help.

Regards,


On Mon, Sep 16, 2013 at 5:13 PM, Daniel Liew <daniel.liew at imperial.ac.uk>wrote:

> Couldn't you just do this...?
>
> // Restrict to alphanumeric passwords
> char c;
> for (unsigned int x=0; x < sizeof(password)/sizeof(char); ++x)
> {
>    c = password[x];
>    klee_assume( (c >= '0' & c <= '9') | (c >= 'A' & c <= 'Z') | (c >=
> 'a' & c <= 'z') );
> }
>
>
> You could probably do something a bit nicer by using the functions in
> ctype.h
>
> Thanks,
> Dan Liew.
>
> On 16 September 2013 08:43, Loi Luu <loi.luuthe at gmail.com> wrote:
> > I make a string variable as symbolic as:
> >
> > unsigned char password[12];
> > klee_make_symbolic(password, sizeof(password),"password");
> >
> > Is there any way like klee_assume to restrict all characters of password
> to
> > be only normal characters and numbers?
> >
> > Thank you,
> >
>



-- 
Loi, Luu The (Mr.)
RA at Security Lab, SoC, NUS
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list