found esbmc failing verifications

and fixed tndma

GNUmakefile

@@ -108,7 +108,7 @@ verify/%.vfy: source/algos/%.c $(ALGOSINC) algocfg GNUmakefile
 	b=`basename $@ .vfy`; echo -n "cmd="; ./algocfg $$b cbmc; \
 	  cmd=`./algocfg $$b cbmc`; \
 	  echo $$cmd $(CBMC_ARGS) $< > $@; \
-	  $$cmd $(CBMC_ARGS) $< | tee -a $@
+	  $$cmd $(CBMC_ARGS) $< 2>&1 | tee -a $@
 	if grep UNSATISFIABLE $@ >/dev/null; then \
 	  echo | tee -a $@; b=`basename $@ .vfy`; \
 	  echo goto-analyzer -Isource/algos -DCBMC --verify --recursive-interprocedural source/algos/$$b.c | tee -a $@; \
@@ -120,7 +120,7 @@ verify/%.vfy-trace: source/algos/%.c $(ALGOSINC) algocfg GNUmakefile
 	b=`basename $@ .vfy-trace`; echo -n "cmd="; ./algocfg $$b cbmc; \
 	  cmd=`./algocfg $$b cbmc`; \
 	  echo $$cmd $(CMBC_TRACE_ARGS) $(CBMC_ARGS) $< > $@; \
-	  $$cmd $(CMBC_TRACE_ARGS) $(CBMC_ARGS) $< | tee -a $@
+	  $$cmd $(CMBC_TRACE_ARGS) $(CBMC_ARGS) $< 2>&1 | tee -a $@
 	if grep UNSATISFIABLE $@ >/dev/null; then \
 	  echo | tee -a $@; b=`basename $@ .vfy`; \
 	  echo goto-analyzer -Isource/algos -DCBMC --verify --recursive-interprocedural source/algos/$$b.c | tee -a $@; \

source/algocfg.c

@@ -153,7 +153,7 @@ const struct algocfg ALGOCFGS[] = {
   //[_BMH2] = {_BMH2, GOOD, ASAN, VFY_PASS, 2, 0, 0, 0, 0, 0},
   //[_BMH4] = {_BMH4, GOOD, ASAN, VFY_PASS, 4, 0, 0, 0, 0, 0},
   [_GRASPm] = {_GRASPm, FAIL, FAIL, VFY_PASS, 2, 0, 0, 0, 0, 0},
-  [_SSEF] = {_SSEF, X64_ONLY, FAIL, VFY_PASS, 32, 0, 0, 0, 0, 0},
+  [_SSEF] = {_SSEF, X64_ONLY, FAIL, VFY_FAIL, 32, 0, 0, 0, 0, 0},
   [_AUT] = {_AUT, GOOD, ASAN, VFY_PASS, 0, 0, 0, 0, 0, 0},
   [_RF] = {_RF, GOOD, ASAN, VFY_PASS, 0, 0, 0, 0, 0, 0},
   [_TRF] = {_TRF, GOOD, ASAN, VFY_PASS, 0, 0, 0, 0, 0, 0},
@@ -335,14 +335,14 @@ const struct algocfg ALGOCFGS[] = {
   [_BRAM7] = {_BRAM7, GOOD, ASAN, VFY_PASS, 7, 0, 0, 0, 0, 0},
   [_FT3]   = {_FT3,   GOOD, ASAN, VFY_PASS, 0, 0, 0, 0, 0, 0},
   //[_HPBM] = {_HPBM, GOOD, ASAN, VFY_PASS, 0, 0, 0, 0, 0, 0},
-  [_SSECP] = {_SSECP, FAIL, ASAN, VFY_PASS, 0, 0, 0, 0, 0, 0}, // no cbmc simd support yet
-  [_SIMDKR] = {_SIMDKR, FAIL, RNDCRASH, VFY_PASS, 0, 0, 0, 0, 0, 0}, // no cbmc simd support yet
+  [_SSECP] = {_SSECP, FAIL, ASAN, VFY_FAIL, 0, 0, 0, 0, 0, 0}, // not cbmc, but esbmc
+  [_SIMDKR] = {_SIMDKR, FAIL, RNDCRASH, VFY_FAIL, 0, 0, 0, 0, 0, 0}, // not cbmc, but esbmc
   [_LIBC]  = {_LIBC,  GOOD, ASAN, VFY_PASS, 0, 0, 0, 0, 0, 0}, // no \0
-  [_LIBC1] = {_LIBC1, GOOD, ASAN, VFY_PASS, 0, 0, 0, 0, 0, 0},
+  [_LIBC1] = {_LIBC1, GOOD, ASAN, VFY_PASS, 0, 0, 0, 0, 0, 0}, // esbmc fails
   [_MUSL]  = {_MUSL,  GOOD, ASAN, VFY_PASS, 0, 0, 0, 0, 0, 0}, // no \0
   [_MUSL1] = {_MUSL1, GOOD, ASAN, VFY_PASS, 0, 0, 0, 0, 0, 0}, //7s, upto d=820 ok
   [_MUSL2] = {_MUSL2, FAIL, ASAN, VFY_PASS, 0, 0, 0, 0, 0, 0},
-  [_EPSM]  = {_EPSM,  GOOD, FAIL, VFY_PASS, 0, 0, 0, 0, 0, 0}, // no cbmc simd support yet
+  [_EPSM]  = {_EPSM,  GOOD, FAIL, VFY_FAIL, 0, 0, 0, 0, 0, 0}, // not cbmc, but esbmc
     // clang-format on
 };
 

source/algos/tndma.c

@@ -116,7 +116,7 @@ int search_large(unsigned char *x, int m, unsigned char *y, int n) {
   BEGIN_PREPROCESSING
   //NOLINTBEGIN(clang-analyzer-security.insecureAPI.DeprecatedOrUnsafeBufferHandling)
   memset(B, 0, SIGMA * sizeof(unsigned int));
-  memset(restore, 0, 32 * sizeof(int));
+  memset(restore, 0, (XSIZE + 1) * sizeof(int));
   //NOLINTEND(clang-analyzer-security.insecureAPI.DeprecatedOrUnsafeBufferHandling)
   s = 1;
   for (i = m - 1; i >= 0; i--) {