1  ==== Integer log 10
 2  
 3  .Implementation
 4  [source]
 5  ----
 6  #include "nlz.h"
 7  
 8  // "one table lookup, branch free" (figure 11-12)
 9  inline int ilog10(unsigned x) {
10      int y;
11      static unsigned table[11] = {0, 9, 99, 999, 9999,
12  	99999, 999999, 9999999, 99999999, 999999999, 0xFFFFFFFF};
13      
14      y = (19*(31 - nlz(x))) >> 6;
15      return y + ((table[y+1]-x) >> 31);
16  }
17  ----
18  
19  
20  .Proof
21  [source]
22  ----
23  // "simple table search" (figure 11-7)
24  int ilog10_simple(unsigned x) {
25      int i;
26      static unsigned table[11] = {0, 9, 99, 999, 9999,
27  	99999, 999999, 9999999, 99999999, 999999999, 0xFFFFFFFF};
28      for(i = -1; i < 11; i++)
29  	if(x <= table[i+1]) return i;
30      assert(0);
31  }
32  
33  int main() {
34      unsigned u = nondet_unsigned();
35      assume(u);
36      assert(ilog10_simple(u) == ilog10(u));
37  }
38  ----