Jun 22, 2011 at 7:33 PM
Edited Jun 23, 2011 at 4:57 PM

Hello,
I am having some trouble coming up with a suitable contract for a sign_extend function. The function is:
static i32 sign_extend(u32 value, u32 sign_bit)
_(requires sign_bit < 31)
_(requires value < (1<<sign_bit+1))
{
if(IS_BIT_SET(value, sign_bit))
value = value  (0xffffffff << sign_bit);
return (i32) _(unchecked) value;
}
And I used this function on elements from a wrapped object that have invariants set on the maximum size. The preconditions I have set work well if I use a sign bit that is too small (and in fact already found a bug in my code that did exactly that),
but I would also like to know that there exists a value that could be equal to (1<<(sign_bit+1))1 for a particular invocation of this function to catch any uses of this function where I use a sign bit that is too large.
struct control {
u32 inst;
u32 K; _(invariant \this>K == (\this>inst & 0xffff))
};
sign_extend(cont>K, 15); // correct
sign_extend(cont>K, 14); // bug I found
sign_extend(cont>K, 16); // bugs I would like to find
Thanks!
Sam

