Hi,
I've run into a strange problem after implementing a Klee model for
the __ctype_b_loc library call, responsible with delivering locale
information to the <ctype.h> library functions.
Whenever I set the --optimize flag in Klee, I start getting (false)
memory errors. After analyzing the generated assembly.ll file, I saw
that Klee inlined the call to this function, and replaced it with just
a memory access to a static variable that I use in the function body.
However, that static variable is also initialized in the function, but
the initialization code ends up not being there, hence the systematic
memory errors.
The offending code is the following:
static const unsigned short *b_locale = NULL;
const unsigned short model__ctype_b_loc(void) {
??if (b_locale != NULL)
?? ?return &b_locale;
??unsigned short *cached = (unsigned short*)malloc(384*sizeof(unsigned short));
??const unsigned short **locale = __ctype_b_loc();
??memcpy(cached, &((*locale)[-128]), 384*sizeof(unsigned short));
??b_locale = &cached[128];
??return &b_locale;
}
Basically, the function simply returns the address of b_locale, unless
b_locale was not initialized. The initialization part seems to be
skipped after the optimizations.
Do you have any idea what could be wrong?
Thank you,
Stefan
