--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on March 2009 ---
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.