File tree 8 files changed +76
-31
lines changed 8 files changed +76
-31
lines changed Original file line number Diff line number Diff line change @@ -61,16 +61,6 @@ test_script:
61
61
- cmd : |
62
62
cd regression
63
63
64
- sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-cbmc/chain.sh || true
65
- sed -i "11s/.*/$GC $NAME.c/" goto-cc-cbmc/chain.sh || true
66
- sed -i "12i mv $NAME.exe $NAME.gb" goto-cc-cbmc/chain.sh || true
67
- cat goto-cc-cbmc/chain.sh || true
68
-
69
- sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-goto-analyzer/chain.sh || true
70
- sed -i "11s/.*/$gc $name.c/" goto-cc-goto-analyzer/chain.sh || true
71
- sed -i "12i mv $name.exe $name.gb" goto-cc-goto-analyzer/chain.sh || true
72
- cat goto-cc-goto-analyzer/chain.sh || true
73
-
74
64
rem HACK disable failing tests
75
65
rmdir /s /q ansi-c\arch_flags_mcpu_bad
76
66
rmdir /s /q ansi-c\arch_flags_mcpu_good
Original file line number Diff line number Diff line change @@ -27,6 +27,8 @@ add_subdirectory(cbmc-java)
27
27
add_subdirectory (cbmc-java-inheritance)
28
28
add_subdirectory (cpp)
29
29
add_subdirectory (goto-analyzer)
30
+ add_subdirectory (goto-cc-cbmc)
31
+ add_subdirectory (goto-cc-goto-analyzer)
30
32
add_subdirectory (goto-diff)
31
33
add_subdirectory (goto-instrument)
32
34
add_subdirectory (goto-instrument-typedef)
Original file line number Diff line number Diff line change
1
+ if (WIN32 )
2
+ set (is_windows true )
3
+ else ()
4
+ set (is_windows false )
5
+ endif ()
6
+
7
+ add_test_pl_tests(
8
+ "goto-cc-cbmc"
9
+ "${CMAKE_CURRENT_SOURCE_DIR} /chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> ${is_windows} "
10
+ )
Original file line number Diff line number Diff line change 1
1
default : tests.log
2
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
+
3
14
test :
4
- @if ! ../test.pl -c ../chain.sh ; then \
15
+ @if ! ../test.pl -c ' ../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows) ' ; then \
5
16
../failed-tests-printer.pl ; \
6
17
exit 1; \
7
18
fi
8
19
9
20
tests.log :
10
- @if ! ../test.pl -c ../chain.sh ; then \
21
+ @if ! ../test.pl -c ' ../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows) ' ; then \
11
22
../failed-tests-printer.pl ; \
12
23
exit 1; \
13
24
fi
Original file line number Diff line number Diff line change 1
- #! /bin/bash
1
+ #! /usr/ bin/env bash
2
2
3
- SRC=../../../src
3
+ goto_cc=$1
4
+ cbmc=$2
5
+ is_windows=$3
4
6
5
- GC=$SRC /goto-cc/goto-cc
6
- CBMC=$SRC /cbmc/cbmc
7
+ options=${*: 4: $# -4}
8
+ name=${*: $# }
9
+ name=${name% .c}
7
10
8
- OPTS=$1
9
- NAME=${2% .c}
11
+ if [[ " ${is_windows} " == " true" ]]; then
12
+ " ${goto_cc} " " ${name} .c"
13
+ mv " ${name} .exe" " ${name} .gb"
14
+ else
15
+ " ${goto_cc} " " ${name} .c" -o " ${name} .gb"
16
+ fi
10
17
11
- $GC $NAME .c -o $NAME .gb
12
- $CBMC $NAME .gb $OPTS
18
+ " ${cbmc} " " ${name} .gb" ${options}
Original file line number Diff line number Diff line change
1
+ if (WIN32 )
2
+ set (is_windows true )
3
+ else ()
4
+ set (is_windows false )
5
+ endif ()
6
+
7
+ add_test_pl_tests(
8
+ "goto-cc-goto-analyzer"
9
+ "${CMAKE_CURRENT_SOURCE_DIR} /chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-analyzer> ${is_windows} "
10
+ )
Original file line number Diff line number Diff line change 1
-
2
1
default : tests.log
3
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
+
4
14
test :
5
- @if ! ../test.pl -c ../chain.sh ; then \
15
+ @if ! ../test.pl -c ' ../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows) ' ; then \
6
16
../failed-tests-printer.pl ; \
7
17
exit 1; \
8
18
fi
9
19
10
20
tests.log :
11
21
pwd
12
- @if ! ../test.pl -c ../chain.sh ; then \
22
+ @if ! ../test.pl -c ' ../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows) ' ; then \
13
23
../failed-tests-printer.pl ; \
14
24
exit 1; \
15
25
fi
Original file line number Diff line number Diff line change 1
- #! /bin/bash
1
+ #! /usr/ bin/env bash
2
2
3
- src=../../../src
3
+ goto_cc=$1
4
+ goto_analyzer=$2
5
+ is_windows=$3
4
6
5
- gc=$src /goto-cc/goto-cc
6
- goto_analyzer=$src /goto-analyzer/goto-analyzer
7
+ options=${*: 4: $# -4}
8
+ name=${*: $# }
9
+ name=${name% .c}
7
10
8
- options=$1
9
- name=${2% .c}
11
+ if [[ " ${is_windows} " == " true" ]]; then
12
+ " ${goto_cc} " " ${name} .c"
13
+ mv " ${name} .exe" " ${name} .gb"
14
+ else
15
+ " ${goto_cc} " " ${name} .c" -o " ${name} .gb"
16
+ fi
10
17
11
- $gc $name .c -o $name .gb
12
- $goto_analyzer $name .gb $options
18
+ " ${goto_analyzer} " " ${name} .gb" ${options}
You can’t perform that action at this time.
0 commit comments