Merge pull request #5421 from danpoe/fixes/goto-cc-filenames

Fix goto-cc same filename bug

Author: danpoe

regression/goto-cc-multi-file/Makefile

@@ -0,0 +1,36 @@
+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
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
+
+tests.log:
+	pwd
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(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 -f tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			rm -f *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/goto-cc-multi-file/chain.sh

@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+
+goto_cc=$1
+cbmc=$2
+is_windows=$3
+
+args=${*:4:$#-4}
+name=${*:$#}
+name=${name%.c}
+
+if [[ "${is_windows}" == "true" ]]; then
+  ${goto_cc} ${name}.c ${args}
+  mv ${name}.exe ${name}.gb
+else
+  ${goto_cc} ${name}.c ${args} -o ${name}.gb
+fi
+
+${cbmc} --show-goto-functions ${name}.gb

regression/goto-cc-multi-file/same-name/dir1/test.c

@@ -0,0 +1,3 @@
+void f1()
+{
+}

regression/goto-cc-multi-file/same-name/dir2/test.c

@@ -0,0 +1,3 @@
+void f2()
+{
+}

regression/goto-cc-multi-file/same-name/main.c

@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}

regression/goto-cc-multi-file/same-name/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+dir1/test.c dir2/test.c
+^EXIT=0$
+^SIGNAL=0$
+^f1
+^f2
+--
+^warning: ignoring

src/goto-cc/gcc_mode.cpp

@@ -655,7 +655,7 @@ int gcc_modet::doit()
 
   // We now iterate over any input files
 
-  temp_dirt temp_dir("goto-cc-XXXXXX");
+  std::vector<temp_dirt> temp_dirs;
 
   {
     std::string language;
@@ -688,7 +688,9 @@ int gcc_modet::doit()
 
           std::string new_name=
             get_base_name(arg_it->arg, true)+new_suffix;
-          std::string dest=temp_dir(new_name);
+
+          temp_dirs.emplace_back("goto-cc-XXXXXX");
+          std::string dest = temp_dirs.back()(new_name);
 
           int exit_code=
             preprocess(language, arg_it->arg, dest, act_as_bcc);

src/util/tempdir.h

@@ -19,14 +19,21 @@ std::string get_temporary_directory(const std::string &name_template);
 class temp_dirt
 {
 public:
-  std::string path;
+  explicit temp_dirt(const std::string &name_template);
+  ~temp_dirt();
+
+  temp_dirt(const temp_dirt &) = delete;
+
+  temp_dirt(temp_dirt &&other)
+  {
+    path.swap(other.path);
+  }
 
   std::string operator()(const std::string &file);
 
   void clear();
 
-  explicit temp_dirt(const std::string &name_template);
-  ~temp_dirt();
+  std::string path;
 };
 
 #endif // CPROVER_UTIL_TEMPDIR_H