How to restrict the character space of symbolic string

[Loi Luu]

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,

[Daniel Liew]

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.

Post by Loi Luu
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]

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

Regards,

Post by Daniel Liew
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.

Post by Loi Luu
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

Post by Loi Luu
be only normal characters and numbers?
Thank you,