Add regression tests for filtering of illegal characters from typename.

Author: NlightNFotis

regression/CMakeLists.txt

@@ -38,6 +38,7 @@ add_subdirectory(smt2_strings)
 add_subdirectory(strings)
 add_subdirectory(invariants)
 add_subdirectory(goto-diff)
+add_subdirectory(goto-cc-instrument-cbmc)
 add_subdirectory(test-script)
 add_subdirectory(goto-analyzer-taint)
 if(NOT WIN32)

regression/goto-cc-instrument-cbmc/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> $<TARGET_FILE:goto-instrument> ${is_windows}"
+)

regression/goto-cc-instrument-cbmc/Makefile

@@ -0,0 +1,38 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
+cbmc=../../../src/cbmc/cbmc
+goto-instrument=../../../src/goto-instrument/goto-instrument
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) $(cbmc) $(goto-instrument) $(is_windows)'
+
+tests.log:
+	@../test.pl -e -p -c '../chain.sh $(exe) $(cbmc) $(goto-instrument) $(is_windows)'
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/goto-cc-instrument-cbmc/chain.sh

@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+
+goto_cc=$1
+cbmc=$2
+goto_instrument=$3
+is_windows=$4
+
+name=${*:$#}
+base_name=${name%.c}
+modified_name=${base_name}.modified.c
+
+if [[ "${is_windows}" == "true" ]]; then
+  "${goto_cc}" "${name}"
+  mv "${base_name}.exe" "${base_name}.gb"
+else
+  "${goto_cc}" "${name}" -o "${base_name}.gb"
+fi
+
+"${goto_instrument}" "${base_name}.gb" --dump-c "${modified_name}"
+
+"${cbmc}" "${modified_name}"

regression/goto-cc-instrument-cbmc/identifier_names_illegal_characters/test.c

@@ -0,0 +1,7 @@
+int main(void)
+{
+  void *v, *x, *x_before;
+  x_before = x;
+  __atomic_store_n(&x, 42, 0);
+  __atomic_exchange_n(&x, 42, 0);
+}

regression/goto-cc-instrument-cbmc/identifier_names_illegal_characters/test.desc

@@ -0,0 +1,15 @@
+CORE
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^PARSING ERROR$
+^CONVERSION ERROR$
+--
+Example of an illegal identifier name we crashed on before:
+__atomic_compare_exchange_n_*{V}$V$
+
+Example of the substitutes we are producing now.
+__atomic_compare_exchange__ptr__start_sub_V_end_sub_