File tree 1 file changed +1
-12
lines changed
1 file changed +1
-12
lines changed Original file line number Diff line number Diff line change @@ -178,25 +178,14 @@ jobs:
178
178
179
179
install :
180
180
- ccache --max-size=1G
181
- - cmake -H. -Bbuild "-DCMAKE_CXX_COMPILER=${COMPILER}" "-Denable_security_tests=true" "-Denable_cbmc_tests=false"
182
- - cmake --build build -- -j4
181
+ - cmake . -Bbuild "-DCMAKE_CXX_COMPILER=${COMPILER}" "-Denable_security_tests=true" "-Denable_cbmc_tests=false"
183
182
- ( cd build; make install )
184
- # - make -C cbmc/src minisat2-download
185
- # - make -C cbmc/src boost-download
186
- # - make -C cbmc/src/ansi-c library_check
187
- # - make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g -DUSE_BOOST ${EXTRA_CXXFLAGS}" -j2
188
- # - make -C cbmc/src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2 goto-analyzer.dir goto-cc.dir goto-diff.dir clobber.dir memory-models.dir
189
183
190
184
# LOCAL CHANGES: Added cbmc/ prefix, and added unit and regression tests to the end of the list.
191
185
192
186
script :
193
187
- ( cd build; ctest -V -L CORE )
194
188
- scripts/travis_run_regression_tests.sh
195
- # - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
196
- # - env UBSAN_OPTIONS=print_stacktrace=1 make -C cbmc/regression test "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}"
197
- # - make -C cbmc/unit "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
198
- # - make -C cbmc/unit test
199
- # - make -C unit test "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g -DUSE_BOOST ${EXTRA_CXXFLAGS}"
200
189
201
190
before_cache :
202
191
- ccache -s
You can’t perform that action at this time.
0 commit comments