File tree Expand file tree Collapse file tree 5 files changed +57
-2
lines changed
goto-bmc-non-symex-ready-goto
goto-bmc-symex-ready-goto Expand file tree Collapse file tree 5 files changed +57
-2
lines changed Original file line number Diff line number Diff line change @@ -30,6 +30,9 @@ DIRS = cbmc-shadow-memory \
3030 goto-diff \
3131 test-script \
3232 goto-analyzer-taint \
33+ goto-bmc/goto-bmc-symex-ready-goto \
34+ goto-bmc/goto-bmc-non-symex-ready-goto \
35+ goto-bmc \
3336 goto-gcc \
3437 goto-cl \
3538 goto-cc-cbmc \
Original file line number Diff line number Diff line change 1+ default : tests.log
2+
3+ test :
4+ @../test.pl -e -p -c ../../../src/goto-bmc/goto-bmc
5+
6+ tests.log : ../test.pl
7+ @../test.pl -e -p -c ../../../src/goto-bmc/goto-bmc
8+
9+ clean :
10+ find . -name ' *.out' -execdir $(RM ) ' {}' \;
11+ find . -name ' *.gb' -execdir $(RM ) ' {}' \;
12+ $(RM ) tests.log
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+ GOTO_BMC_EXE =../../../../src/goto-bmc/goto-bmc
7+
8+ ifeq ($(BUILD_ENV_ ) ,MSVC)
9+ GOTO_CC_EXE=../../../../src/goto-cc/goto-cl
10+ is_windows=true
11+ else
12+ GOTO_CC_EXE=../../../../src/goto-cc/goto-cc
13+ is_windows=false
14+ endif
15+
16+ test :
17+ @../../test.pl -e -p -c " ../chain.sh $( GOTO_CC_EXE) $( GOTO_BMC_EXE) $( is_windows) "
18+
19+ tests.log : ../test.pl
20+ @../../test.pl -e -p -c " ../chain.sh $( GOTO_CC_EXE) $( GOTO_BMC_EXE) $( is_windows) "
21+
22+ clean :
23+ find . -name ' *.out' -execdir $(RM ) ' {}' \;
24+ find . -name ' *.gb' -execdir $(RM ) {} \;
25+ $(RM ) tests.log
Original file line number Diff line number Diff line change 1+ default : tests.log
2+
3+ CBMC_EXE =../../../../src/cbmc/cbmc
4+ GOTO_BMC_EXE =../../../../src/goto-bmc/goto-bmc
5+
6+ test :
7+ @../../test.pl -e -p -c " ../chain.sh $( CBMC_EXE) $( GOTO_BMC_EXE) "
8+
9+ tests.log : ../test.pl
10+ @../../test.pl -e -p -c " ../chain.sh $( CBMC_EXE) $( GOTO_BMC_EXE) "
11+
12+ clean :
13+ find . -name ' *.out' -execdir $(RM ) ' {}' \;
14+ find . -name ' *.gb' -execdir $(RM ) {} \;
15+ $(RM ) tests.log
Original file line number Diff line number Diff line change @@ -9,5 +9,5 @@ options=${*:3:$#-3}
99name=${*: $# }
1010base_name=${name% .c}
1111
12- " ${cbmc} " --export-symex-ready-goto " ${base_name} .goto.symex_ready " " ${name} "
13- " ${goto_bmc} " " ${base_name} .goto.symex_ready " ${options}
12+ " ${cbmc} " --export-symex-ready-goto " ${base_name} .gb " " ${name} "
13+ " ${goto_bmc} " " ${base_name} .gb " ${options}
You can’t perform that action at this time.
0 commit comments