--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Jessie] Issue with offset in static strings



Hello,

In my code, I have a function of following form:

/*@ requires rand_fd >= 0;
    ensures \result >= 'a' && \result <= 'z';
 */
static int randletter(int rand_fd)
{
        int tmp = randval(rand_fd, 26);
	//@ assert tmp >= 0 && tmp <= 26;
        return "abcdefghijklmnopqrstuvwxyz"[tmp];
}

I am able to correctly prove the "assert tmp >= 0 && tmp <= 26;" assertion.

However, Alt-Ergo is not able to prove the randletter() postcondition.
I assume this is because some steps are missing between the assertion
and the postcondition. Any idea of what should I provide?

I have attempted following code, with no luck:

/*@ requires rand_fd >= 0;
    ensures \result >= 'a' && \result <= 'z';
 */
static int randletter(int rand_fd)
{
        char str[] = "abcdefghijklmnopqrstuvwxyz";
        int tmp = randval(rand_fd, 26);

	//@ assert tmp >= 0 && tmp <= 26;
	//@ assert str[0] == 'a';
        return str[tmp];
}

Alt-Ergo fails to prove "assert str[0] == 'a';". Is it because Frama-C
/ Jessie do not "look into" "str"?

Sincerely yours,
d.

PS : The C code is the same as in my previous email regarding another
issue with Jessie.