From c04168437b5d093f5d72297ea348cc98c0506850 Mon Sep 17 00:00:00 2001 From: Alex Groce Date: Wed, 5 Dec 2018 20:54:11 -0700 Subject: [PATCH] go back to simple fix, but wrap when out of bounds and not symbolic --- src/include/deepstate/DeepState.h | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/include/deepstate/DeepState.h b/src/include/deepstate/DeepState.h index ba0afb7..bbcf1bb 100644 --- a/src/include/deepstate/DeepState.h +++ b/src/include/deepstate/DeepState.h @@ -261,13 +261,14 @@ DEEPSTATE_INLINE static void DeepState_Check(int expr) { return DeepState_ ## Tname ## InRange(high, low); \ } \ const tname x = DeepState_ ## Tname(); \ - const tname size = (high - low) + 1; \ if (DeepState_UsingSymExec) { \ - (void) DeepState_Assume(0 <= x && x < size); \ - return low + x; \ + (void) DeepState_Assume(low <= x && x <= high); \ } else { \ - return low + (x % size); \ + if ((x < low) || (x > high)) { \ + const tname size = (high - low) + 1; \ + x = low + (x % size); \ } \ + return x; \ } DEEPSTATE_MAKE_SYMBOLIC_RANGE(Size, size_t)