What loop invariants to use for an integer logarithm?

As I am having my first steps in C formal verification with Frama-C, I am trying to formally verify an integer binary logarithm function written as follows:

//@ logic integer pow2(integer n) = (n == 0)? 1 : 2 * pow2(n - 1);

/*@
    requires n > 0;
    assigns \nothing;
    ensures pow2(\result) <= \old(n) < pow2(\result + 1);
 */
unsigned int log2(size_t n)
{
    unsigned int res = 0;
    while (n > 1) {
        n /= 2;
        ++res;
    }
    return res;
}

I am using Frama-C 20.0 (Calcium), with the command frama-c-gui -rte -wp file.c (I do not have the Jessie plugin for some reason). I have checked the post-condition to hold for up to n = 100,000,000 (using standard-library asserts), but this function fails to verify formally despite my best efforts, and Frama-C tutorials typically involve trivial loop variants that decrement (instead of halving) every iteration, thus not that close to what I am trying to do.

I have tried the following code annotations, some of which are likely unnecessary:

//@ logic integer pow2(integer n) = (n == 0)? 1 : 2 * pow2(n - 1);

/*@
    requires n > 0;
    assigns \nothing;
    ensures pow2(\result) <= \old(n) < pow2(\result + 1);
 */
unsigned int log2(size_t n)
{
    unsigned int res = 0;
    /*@
        loop invariant 0 < n <= \at(n, Pre);
        loop invariant \at(n, Pre) < n * pow2(res + 1);
        loop invariant pow2(res) <= \at(n, Pre);
        loop invariant res > 0 ==> 2 * n <= \at(n, Pre);
        loop invariant n > 1 ==> pow2(res + 1) <= \at(n, Pre);
        loop invariant res <= pow2(res);
        loop assigns n, res;
        loop variant n;
     */
    while (n > 1) {
    L:
        n /= 2;
        //@ assert 2 * n <= \at(n, L);
        ++res;
        //@ assert res == \at(res, L) + 1;
    }
    //@ assert n == 1;
    return res;
}

The annotations that fail to verify are loop invariants 2 and 5 (both Alt-Ergo 2.3.0 and Z3 4.8.7 timeout). As far as invariant 2 is concerned, the difficulty appears to be linked to integer division, but I am not sure what to add to make WP able to prove it. As for invariant 5, WP can prove that it’s established, but not that it’s preserved. It may require a property able to capture what happens when n becomes 1, but I am not sure what could work.

How may I specify the missing information to verify these loop invariants, and is there another Frama-C analysis that could allow me to find loop invariants more easily?

Thank you for your consideration.

As a general remark, it is often a good idea to name your annotations, especially when you start having several loop invariants for the same loop. It will allow you to more quickly pinpoint the ones that are failing (see below for an example, although you're free to disagree with the names I have chosen).

Now back to your issues: the main point is that your invariant 2 is a bit too weak. In case n in the current loop is odd, you can't establish that the inequality holds at next step. With a tighter bound, namely \at(n,Pre) < (n+1) * pow2(res), the hypothesis at the start of the current step is strong enough to prove that the invariant holds at the end of the step, provided we know that res will not overflow (otherwise 1+res will eventually become 0, and the inequality won't hold anymore).

For that, I've use an intermediate ghost function to prove that n < pow2(n) for any unsigned, which allows me, thanks to the pow2_lower invariant below, to ensure that res_bound is preserved by any loop step.

Finally, a minor remark on pow2: it doesn't matter here, since arguments are unsigned, hence non-negative, but in the general case, an integer argument can be negative, hence you might want to make the definition more robust by returning 1 whenever n<=0.

All in all, the following program is entirely proved with Frama-C 20 and Alt-Ergo (frama-c -wp -wp-rte file.c). There are still two assertions that seem to be needed to guide Alt-Ergo in its proof search.

#include "stddef.h"

/*@ logic integer pow2(integer n) = n<=0?1:2*pow2(n-1); */

/*@ ghost
/@ assigns \nothing;
   ensures n < pow2(n);
@/
void lemma_pow2_bound(unsigned n) {
  if (n == 0) return;
  lemma_pow2_bound(n-1);
  return;
}
*/

/*@
    requires n > 0;
    assigns \nothing;
    ensures pow2(\result) <= \old(n) < pow2(\result + 1);
 */
unsigned int log2(size_t n)
{
    unsigned int res = 0;
    /*@
        loop invariant n_bound: 0 < n <= \at(n, Pre);
        loop invariant pow2_upper: \at(n, Pre) < (n+1) * pow2(res);
        loop invariant pow2_lower: n*pow2(res) <= \at(n, Pre);
        loop invariant res_bound: 0 <= res < \at(n,Pre);
        loop assigns n, res;
        loop variant n;
     */
    while (n > 1) {
    L:
        /*@ assert n % 2 == 0 || n % 2 == 1; */
        n /= 2;
        /*@ assert 2*n <= \at(n,L); */
        res++;
        /*@ ghost lemma_pow2_bound(res); */
    }
    //@ assert n == 1;
    return res;
}