Skip to content

Commit 2d02d6e

Browse files
authored
Merge pull request #5421 from danpoe/fixes/goto-cc-filenames
Fix goto-cc same filename bug
2 parents 7697748 + 573fe09 commit 2d02d6e

File tree

8 files changed

+87
-5
lines changed

8 files changed

+87
-5
lines changed
Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
default: tests.log
2+
3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
ifeq ($(BUILD_ENV_),MSVC)
7+
exe=../../../src/goto-cc/goto-cl
8+
is_windows=true
9+
else
10+
exe=../../../src/goto-cc/goto-cc
11+
is_windows=false
12+
endif
13+
14+
test:
15+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
16+
17+
tests.log:
18+
pwd
19+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
20+
21+
show:
22+
@for dir in *; do \
23+
if [ -d "$$dir" ]; then \
24+
vim -o "$$dir/*.c" "$$dir/*.out"; \
25+
fi; \
26+
done;
27+
28+
clean:
29+
@for dir in *; do \
30+
rm -f tests.log; \
31+
if [ -d "$$dir" ]; then \
32+
cd "$$dir"; \
33+
rm -f *.out *.gb; \
34+
cd ..; \
35+
fi \
36+
done
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#!/usr/bin/env bash
2+
3+
goto_cc=$1
4+
cbmc=$2
5+
is_windows=$3
6+
7+
args=${*:4:$#-4}
8+
name=${*:$#}
9+
name=${name%.c}
10+
11+
if [[ "${is_windows}" == "true" ]]; then
12+
${goto_cc} ${name}.c ${args}
13+
mv ${name}.exe ${name}.gb
14+
else
15+
${goto_cc} ${name}.c ${args} -o ${name}.gb
16+
fi
17+
18+
${cbmc} --show-goto-functions ${name}.gb
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
void f1()
2+
{
3+
}
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
void f2()
2+
{
3+
}
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
int main()
2+
{
3+
return 0;
4+
}
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
dir1/test.c dir2/test.c
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^f1
7+
^f2
8+
--
9+
^warning: ignoring

src/goto-cc/gcc_mode.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -655,7 +655,7 @@ int gcc_modet::doit()
655655

656656
// We now iterate over any input files
657657

658-
temp_dirt temp_dir("goto-cc-XXXXXX");
658+
std::vector<temp_dirt> temp_dirs;
659659

660660
{
661661
std::string language;
@@ -688,7 +688,9 @@ int gcc_modet::doit()
688688

689689
std::string new_name=
690690
get_base_name(arg_it->arg, true)+new_suffix;
691-
std::string dest=temp_dir(new_name);
691+
692+
temp_dirs.emplace_back("goto-cc-XXXXXX");
693+
std::string dest = temp_dirs.back()(new_name);
692694

693695
int exit_code=
694696
preprocess(language, arg_it->arg, dest, act_as_bcc);

src/util/tempdir.h

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,14 +19,21 @@ std::string get_temporary_directory(const std::string &name_template);
1919
class temp_dirt
2020
{
2121
public:
22-
std::string path;
22+
explicit temp_dirt(const std::string &name_template);
23+
~temp_dirt();
24+
25+
temp_dirt(const temp_dirt &) = delete;
26+
27+
temp_dirt(temp_dirt &&other)
28+
{
29+
path.swap(other.path);
30+
}
2331

2432
std::string operator()(const std::string &file);
2533

2634
void clear();
2735

28-
explicit temp_dirt(const std::string &name_template);
29-
~temp_dirt();
36+
std::string path;
3037
};
3138

3239
#endif // CPROVER_UTIL_TEMPDIR_H

0 commit comments

Comments
 (0)