diff --git a/src/include/deepstate/DeepState.h b/src/include/deepstate/DeepState.h index 5938adf..2204a2f 100644 --- a/src/include/deepstate/DeepState.h +++ b/src/include/deepstate/DeepState.h @@ -295,6 +295,11 @@ DEEPSTATE_INLINE static void DeepState_Check(int expr) { } \ if ((x < low) || (x > high)) { \ const tname size = (high - low) + 1; \ + if (FLAGS_verbose_reads) { \ + if (x != (low + ((x % size + size) % size))) { \ + printf("Converting out-of-range value to %u\n", (unsigned int)(low + ((x % size + size) % size))); \ + } \ + } \ return low + ((x % size + size) % size); \ } \ return x; \