1  ==== Number of leading zeroes
 2  
 3  .Implementation
 4  [source]
 5  ----
 6  inline int nlz(unsigned x) {
 7      static char table[64] =
 8      {32,31,-1,16,-1,30, 3,-1,  15,-1,-1,-1,29,10, 2,-1,
 9       -1,-1,12,14,21,-1,19,-1,  -1,28,-1,25,-1, 9, 1,-1,
10       17,-1, 4,-1,-1,-1,11,-1,  13,22,20,-1,26,-1,-1,18,
11        5,-1,-1,23,-1,27,-1, 6,  -1,24, 7,-1, 8,-1, 0,-1};
12      x = x | (x >> 1);     // Propagate leftmost
13      x = x | (x >> 2);     // 1-bit to the right.
14      x = x | (x >> 4);
15      x = x | (x >> 8);
16      x = x | (x >>16);
17      x = x*0x06EB14F9;     // Multiplier is 7*255**3.
18      return table[x >> 26];
19  }
20  
21  inline int nlz(uint64_t x) {
22      unsigned i = x >> 32;
23      if(i) return nlz(i);
24      return 32+nlz(unsigned(x));
25  }
26  ----
27  
28  .Proof
29  [source]
30  ----
31  #include <pop.h>
32  template<class T>
33  int nlz_simple(T x) {
34      x = x | (x >> 1);
35      x = x | (x >> 2);
36      x = x | (x >> 4);
37      x = x | (x >> 8);
38      if(sizeof(T) > 2) {
39          x = x | (x >>16);
40      }
41      if(sizeof(T) > 4) {
42          x = x | (x >>32);
43      }
44      return proof_popcnt(~x);
45  }
46  
47  template<class T> void prove(T x) {
48      assert(nlz(x) == nlz_simple(x));
49  }
50  
51  int main() {
52      prove(nondet_unsigned());
53      prove(nondet_u64());
54  }
55  ----