Line data    Source code

       1             : /*
       2             :  */
       3             : 
       4             : #include <aws/common/byte_buf.h>
       5             : #include <aws/common/private/byte_buf.h>
       6             : 
       7             : #include <seahorn/seahorn.h>
       8             : #include <nondet.h>
       9             : 
      10       50000 : int main() {
      11       50000 :     /* parameters */
      12       50000 :     size_t index = nd_size_t();
      13       50000 :     size_t bound = nd_size_t();
      14       50000 : 
      15       50000 :     /* operation under verification */
      16       50000 :     size_t rval = aws_nospec_mask(index, bound);
      17       50000 : 
      18       50000 :     /* assertions */
      19       50000 :     if (rval == 0) {
      20       35065 :         sassert((index >= bound) || (bound > (SIZE_MAX / 2)) || (index > (SIZE_MAX / 2)));
      21       35065 :     } else {
      22       14935 :         sassert(rval == UINTPTR_MAX);
      23       14935 :         sassert(!((index >= bound) || (bound > (SIZE_MAX / 2)) || (index > (SIZE_MAX / 2))));
      24       14935 :     }
      25       50000 :     return 0;
      26       50000 : }