1  #ifndef HDELIGHT_PROOFS_COMMON_H
 2  #define HDELIGHT_PROOFS_COMMON_H
 3  
 4  #include <inttypes.h>
 5  
 6  #define BITS(T)  (sizeof(T) * 8)
 7  
 8  #ifdef __CPROVER__
 9  #define assume(x) __CPROVER_assume((x))
10  #define assert(x) __CPROVER_assert((x), #x)
11  #else
12  #define assume(x)
13  #include <assert.h>
14  #endif
15  
16  int nondet_int();
17  unsigned nondet_unsigned();
18  
19  uint8_t nondet_u8();
20  uint16_t nondet_u16();
21  uint32_t nondet_u32();
22  uint64_t nondet_u64();
23  
24  int8_t nondet_s8();
25  int16_t nondet_s16();
26  int32_t nondet_s32();
27  int64_t nondet_s64();
28  
29  inline int proof_popcnt(uint64_t u)
30  {
31      int r = 0;
32      for(int i=0; i<64; i++)
33          if(u & (1ull << i)) r ++;
34      return r;
35  }
36  
37  template<class T>
38  T nondet() { return (T)(nondet_u64()); }
39  
40  #endif