1  ==== Find leftmost 0-byte 
 2  
 3  .Implementation
 4  [source]
 5  ----
 6  #include "nlz.h"
 7  inline int zbytel(unsigned x) {
 8      unsigned y;
 9      int n;
10      y = (x & 0x7f7f7f7f) + 0x7f7f7f7f;
11      y = ~(y | x | 0x7f7f7f7f);
12      n = nlz(y) >> 3;
13      return n;
14  }
15  
16  inline int zbytel_nonlz(unsigned x) {
17      unsigned y;
18      int n;
19      y = (x & 0x7f7f7f7f) + 0x7f7f7f7f;
20      y = ~(y | x | 0x7f7f7f7f);
21      if(y == 0) return 4;
22      if(y > 0xffff) return (y >> 31) ^ 1;
23      return (y >> 15) ^ 3;
24  }
25  
26  ----
27  
28  .Proof
29  [source]
30  ----
31  int zbytel_ref(unsigned x) {
32      if((x >> 24) == 0) return 0;
33      if((x & 0x00ff0000) == 0) return 1;
34      if((x & 0x0000ff00) == 0) return 2;
35      if((x & 0x000000ff) == 0) return 3;
36      return 4;
37  }
38  
39  int main() {
40      unsigned x = nondet_unsigned();
41      assert(zbytel(x) == zbytel_ref(x));
42      assert(zbytel_nonlz(x) == zbytel_ref(x));
43  }
44  ----