File tree Expand file tree Collapse file tree 6 files changed +73
-0
lines changed
regression/goto-cc-multi-file Expand file tree Collapse file tree 6 files changed +73
-0
lines changed Original file line number Diff line number Diff line change 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
Original file line number Diff line number Diff line change 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
Original file line number Diff line number Diff line change 1+ void f1 ()
2+ {
3+ }
Original file line number Diff line number Diff line change 1+ void f2 ()
2+ {
3+ }
Original file line number Diff line number Diff line change 1+ int main ()
2+ {
3+ return 0 ;
4+ }
Original file line number Diff line number Diff line change 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
You can’t perform that action at this time.
0 commit comments