1  ==== Add Even Parity in MSB
 2  
 3  .Implementation
 4  [source]
 5  ----
 6  inline uint8_t pareven(uint8_t x) {
 7      return (((unsigned)x * 0x10204081u) & 0x888888ffu) % 1920;
 8  }
 9  ----
10  
11  .Proof
12  [source]
13  ----
14  #include <parity.h>
15  
16  int main() {
17      uint8_t x = nondet<uint8_t>() & 0x7f;
18      uint8_t y = pareven(x);
19      assert((y & 0x7f) == x);
20      assert(!parity(y));
21  }
22  ----