Add string literal regression test

diffblue · Jul 18, 2023 · 3f7e416 · 3f7e416
1 parent 6bef976
commit 3f7e416
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 0 deletions.
diff --git a/regression/cbmc-incr-smt2/arrays/string_literal.c b/regression/cbmc-incr-smt2/arrays/string_literal.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  const char *my_string = "hello!";
+  uint8_t index;
+  __CPROVER_assume(index < 6);
+  char element = my_string[index];
+  assert(element != 'o');
+}
diff --git a/regression/cbmc-incr-smt2/arrays/string_literal.desc b/regression/cbmc-incr-smt2/arrays/string_literal.desc
@@ -0,0 +1,13 @@
+CORE
+string_literal.c
+--trace
+Passing problem to incremental SMT2 solving
+line 10 assertion element \!\= \'o\'\: FAILURE
+index=4
+element='o'
+VERIFICATION FAILED
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of indexing into a string literal.