1  ==== Add Odd Parity in MSB
 2  
 3  .Implementation
 4  [source]
 5  ----
 6  inline uint8_t parodd(uint8_t x) {
 7      return (((unsigned)x * 0x204081u) | 0x3db6db00u) % 1152;
 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 = parodd(x);
19      assert((y & 0x7f) == x);
20      assert(parity(y));
21  }
22  ----