From 16847a2b223ac7b4cca25abff645fd3ae8fac4da Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 11 Nov 2020 11:58:08 +0000 Subject: [PATCH 1/4] Remove `make` based CI jobs So that we can remove the `make` build entirely. --- .github/workflows/pull-request-checks.yaml | 60 ----------------- buildspec-windows.yml | 78 ---------------------- 2 files changed, 138 deletions(-) delete mode 100644 buildspec-windows.yml diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 4451ee1820b..c629833f8f7 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -4,42 +4,6 @@ on: branches: [ develop ] jobs: - check-ubuntu-20_04-make-gcc: - runs-on: ubuntu-20.04 - steps: - - uses: actions/checkout@v2 - with: - submodules: true - - name: Fetch dependencies - env: - # This is needed in addition to -yq to prevent apt-get from asking for - # user input - DEBIAN_FRONTEND: noninteractive - TESTPL_JOBS: 4 - run: | - sudo apt-get install -yq gcc gdb g++ maven jq flex bison libxml2-utils cpanminus - make -C src minisat2-download - cpanm Thread::Pool::Simple - - name: Build with make - run: | - make -C src CXX='/usr/bin/g++' -j2 - make -C unit CXX='/usr/bin/g++' -j2 - make -C jbmc/src CXX='/usr/bin/g++' -j2 - make -C jbmc/unit CXX='/usr/bin/g++' -j2 - - name: Run unit tests - run: | - make -C unit test - make -C jbmc/unit test - echo "Running expected failure tests" - make TAGS="[!shouldfail]" -C unit test - make TAGS="[!shouldfail]" -C jbmc/unit test - - name: Run regression tests - run: | - make -C regression test - make -C regression/cbmc test-paths-lifo - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 - make -C jbmc/regression test - check-ubuntu-20_04-cmake-gcc: runs-on: ubuntu-20.04 steps: @@ -71,30 +35,6 @@ jobs: env: TESTPL_JOBS: 2 - check-macos-10_15-make-clang: - runs-on: macos-10.15 - steps: - - uses: actions/checkout@v2 - with: - submodules: true - - name: Fetch dependencies - run: brew install maven flex bison - - name: Build using Make - run: | - make -C src minisat2-download - make -C src - make -C jbmc/src - make -C unit - make -C jbmc/unit - - name: Run unit tests - run: cd unit; ./unit_tests - - name: Run JBMC unit tests - run: cd jbmc/unit; ./unit_tests - - name: Run regression tests - run: cd regression; make - - name: Run JBMC regression tests - run: cd jbmc/regression; make - check-macos-10_15-cmake-clang: runs-on: macos-10.15 steps: diff --git a/buildspec-windows.yml b/buildspec-windows.yml deleted file mode 100644 index 47e8dc3c31c..00000000000 --- a/buildspec-windows.yml +++ /dev/null @@ -1,78 +0,0 @@ -version: 0.2 - -env: - variables: - # CodeBuild console doesn't display color codes correctly - TESTPL_COLOR_OUTPUT: 0 - -phases: - install: - commands: - - choco install cyg-get -y --no-progress - - cyg-get bash patch bison flex make wget perl jq - - nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0 - - build: - commands: - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - bash -c "make -C src minisat2-download DOWNLOADER=wget" - - - | - $env:Path = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$env:Path" - $env:CLCACHE_DIR = "C:\clcache" - $env:CLCACHE_BASEDIR = (Get-Item -Path ".\").FullName - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make CXX=clcache.exe -j4 -C src BUILD_ENV=MSVC" ' - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make CXX=clcache.exe -j4 -C unit all BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$env:Path" - $env:CLCACHE_DIR = "C:\clcache" - $env:CLCACHE_BASEDIR = (Get-Item -Path ".\").FullName - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/src setup-submodules" && bash -c "make CXX=clcache.exe -j4 -C jbmc/src BUILD_ENV=MSVC" ' - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make CXX=clcache.exe -j4 -C jbmc/unit all BUILD_ENV=MSVC" ' - - - | - # display cache stats - $env:Path = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$env:Path" - $env:CLCACHE_DIR = "C:\clcache" - $env:CLCACHE_BASEDIR = (Get-Item -Path ".\").FullName - cmd /c 'clcache -s' - - post_build: - commands: - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression test BUILD_ENV=MSVC" ' - - - | - $env:Path = "$pwd\src\solvers;C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression/cbmc test-cprover-smt2 BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression/cbmc test-paths-lifo BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C unit test BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make TAGS=[!shouldfail] -C unit test BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/regression test BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/unit test BUILD_ENV=MSVC" ' - - - | - $env:Path = "C:\tools\cygwin\bin;$env:Path" - cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make TAGS=[!shouldfail] -C jbmc/unit test BUILD_ENV=MSVC" ' - -cache: - paths: - - 'c:\clcache\**\*' From f8c492ff903142453129c7bd55bd090f9367ba59 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 11 Nov 2020 11:58:09 +0000 Subject: [PATCH 2/4] Remove `make` build files Removing the `make` build will reduce the amount of maintenance work required, as it means only one build will need to be maintained, rather than 2. This will have benefits not only in reduced maintenance, but remove problems relating to the two builds being desynchronised. --- jbmc/regression/Makefile | 50 ---- jbmc/regression/janalyzer-taint/Makefile | 21 -- jbmc/regression/janalyzer/Makefile | 21 -- jbmc/regression/jbmc-concurrency/Makefile | 34 --- jbmc/regression/jbmc-generics/Makefile | 36 --- jbmc/regression/jbmc-inheritance/Makefile | 34 --- jbmc/regression/jbmc-json-ui/Makefile | 37 --- jbmc/regression/jbmc-strings/Makefile | 31 --- jbmc/regression/jbmc/Makefile | 44 ---- jbmc/regression/jbmc/lvt-unexpected/Makefile | 7 - jbmc/regression/jdiff/Makefile | 20 -- jbmc/regression/strings-smoke-tests/Makefile | 31 --- jbmc/src/Makefile | 67 ----- jbmc/src/janalyzer/Makefile | 50 ---- jbmc/src/java_bytecode/Makefile | 82 ------ jbmc/src/java_bytecode/library/Makefile | 37 --- jbmc/src/jbmc/Makefile | 64 ----- jbmc/src/jdiff/Makefile | 57 ---- jbmc/src/miniz/Makefile | 14 - jbmc/unit/Makefile | 156 ----------- jbmc/unit/java-testing-utils/Makefile | 20 -- src/Makefile | 166 ------------ src/analyses/Makefile | 54 ---- src/ansi-c/Makefile | 128 --------- src/assembler/Makefile | 25 -- src/cbmc/Makefile | 76 ------ src/cpp/Makefile | 83 ------ src/goto-analyzer/Makefile | 51 ---- src/goto-cc/Makefile | 73 ----- src/goto-checker/Makefile | 34 --- src/goto-diff/Makefile | 55 ---- src/goto-harness/Makefile | 44 ---- src/goto-instrument/Makefile | 123 --------- src/goto-programs/Makefile | 90 ------- src/goto-symex/Makefile | 53 ---- src/jsil/Makefile | 42 --- src/json-symtab-language/Makefile | 17 -- src/json/Makefile | 33 --- src/langapi/Makefile | 18 -- src/linking/Makefile | 18 -- src/memory-analyzer/Makefile | 38 --- src/pointer-analysis/Makefile | 25 -- src/solvers/Makefile | 264 ------------------- src/solvers/bdd/miniBDD/Makefile | 23 -- src/statement-list/Makefile | 55 ---- src/symtab2gb/Makefile | 35 --- src/util/Makefile | 141 ---------- src/xmllang/Makefile | 35 --- unit/Makefile | 243 ----------------- unit/testing-utils/Makefile | 23 -- 50 files changed, 2978 deletions(-) delete mode 100644 jbmc/regression/Makefile delete mode 100644 jbmc/regression/janalyzer-taint/Makefile delete mode 100644 jbmc/regression/janalyzer/Makefile delete mode 100644 jbmc/regression/jbmc-concurrency/Makefile delete mode 100644 jbmc/regression/jbmc-generics/Makefile delete mode 100644 jbmc/regression/jbmc-inheritance/Makefile delete mode 100644 jbmc/regression/jbmc-json-ui/Makefile delete mode 100644 jbmc/regression/jbmc-strings/Makefile delete mode 100644 jbmc/regression/jbmc/Makefile delete mode 100644 jbmc/regression/jbmc/lvt-unexpected/Makefile delete mode 100644 jbmc/regression/jdiff/Makefile delete mode 100644 jbmc/regression/strings-smoke-tests/Makefile delete mode 100644 jbmc/src/Makefile delete mode 100644 jbmc/src/janalyzer/Makefile delete mode 100644 jbmc/src/java_bytecode/Makefile delete mode 100644 jbmc/src/java_bytecode/library/Makefile delete mode 100644 jbmc/src/jbmc/Makefile delete mode 100644 jbmc/src/jdiff/Makefile delete mode 100644 jbmc/src/miniz/Makefile delete mode 100644 jbmc/unit/Makefile delete mode 100644 jbmc/unit/java-testing-utils/Makefile delete mode 100644 src/Makefile delete mode 100644 src/analyses/Makefile delete mode 100644 src/ansi-c/Makefile delete mode 100644 src/assembler/Makefile delete mode 100644 src/cbmc/Makefile delete mode 100644 src/cpp/Makefile delete mode 100644 src/goto-analyzer/Makefile delete mode 100644 src/goto-cc/Makefile delete mode 100644 src/goto-checker/Makefile delete mode 100644 src/goto-diff/Makefile delete mode 100644 src/goto-harness/Makefile delete mode 100644 src/goto-instrument/Makefile delete mode 100644 src/goto-programs/Makefile delete mode 100644 src/goto-symex/Makefile delete mode 100644 src/jsil/Makefile delete mode 100644 src/json-symtab-language/Makefile delete mode 100644 src/json/Makefile delete mode 100644 src/langapi/Makefile delete mode 100644 src/linking/Makefile delete mode 100644 src/memory-analyzer/Makefile delete mode 100644 src/pointer-analysis/Makefile delete mode 100644 src/solvers/Makefile delete mode 100644 src/solvers/bdd/miniBDD/Makefile delete mode 100644 src/statement-list/Makefile delete mode 100644 src/symtab2gb/Makefile delete mode 100644 src/util/Makefile delete mode 100644 src/xmllang/Makefile delete mode 100644 unit/Makefile delete mode 100644 unit/testing-utils/Makefile diff --git a/jbmc/regression/Makefile b/jbmc/regression/Makefile deleted file mode 100644 index 4a052c618d7..00000000000 --- a/jbmc/regression/Makefile +++ /dev/null @@ -1,50 +0,0 @@ -# For the best possible utilisation of multiple cores when -# running tests in parallel, it is important that these directories are -# listed with decreasing runtimes (i.e. longest running at the top) -DIRS = janalyzer \ - janalyzer-taint \ - jbmc \ - jbmc-concurrency \ - jbmc-inheritance \ - jbmc-json-ui \ - jbmc-strings \ - jdiff \ - strings-smoke-tests \ - jbmc-generics \ - # Empty last line - -# Run all test directories in sequence -.PHONY: test -test: - @for dir in $(DIRS); do \ - $(MAKE) "$$dir" || exit 1; \ - done; - -# Pattern to execute a single test suite directory -.PHONY: $(DIRS) -$(DIRS): - @echo "Running $@..." ; - $(MAKE) -C "$@" test || exit 1; - -# Run all test directories using GNU Parallel -.PHONY: test-parallel -.NOTPARALLEL: test-parallel -test-parallel: - @echo "Building with $(JOBS) jobs" - parallel \ - --halt soon,fail=1 \ - --tag \ - --tagstring '{#}:' \ - --linebuffer \ - --jobs $(JOBS) \ - $(MAKE) "{}" \ - ::: $(DIRS) - - -.PHONY: clean -clean: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - $(MAKE) -C "$$dir" clean; \ - fi; \ - done; diff --git a/jbmc/regression/janalyzer-taint/Makefile b/jbmc/regression/janalyzer-taint/Makefile deleted file mode 100644 index 0dc877cc72a..00000000000 --- a/jbmc/regression/janalyzer-taint/Makefile +++ /dev/null @@ -1,21 +0,0 @@ -default: tests.log - -include ../../src/config.inc - -test: - @../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/janalyzer/janalyzer - -tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/janalyzer/janalyzer - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.java" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log diff --git a/jbmc/regression/janalyzer/Makefile b/jbmc/regression/janalyzer/Makefile deleted file mode 100644 index 0dc877cc72a..00000000000 --- a/jbmc/regression/janalyzer/Makefile +++ /dev/null @@ -1,21 +0,0 @@ -default: tests.log - -include ../../src/config.inc - -test: - @../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/janalyzer/janalyzer - -tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/janalyzer/janalyzer - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.java" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log diff --git a/jbmc/regression/jbmc-concurrency/Makefile b/jbmc/regression/jbmc-concurrency/Makefile deleted file mode 100644 index 3d2b16bfdac..00000000000 --- a/jbmc/regression/jbmc-concurrency/Makefile +++ /dev/null @@ -1,34 +0,0 @@ -default: tests.log - -include ../../src/config.inc - -test: - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" - -tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.java" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log - -%.class: %.java ../../src/org.cprover.jar - javac -g -cp ../../src/org.cprover.jar:. $< - -nondet_java_files := $(shell find . -name "Nondet*.java") -nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files)) - -.PHONY: nondet-class-files -nondet-class-files: $(nondet_class_files) - -.PHONY: clean-nondet-class-files -clean-nondet-class-files: - -rm $(nondet_class_files) diff --git a/jbmc/regression/jbmc-generics/Makefile b/jbmc/regression/jbmc-generics/Makefile deleted file mode 100644 index e6541f77df2..00000000000 --- a/jbmc/regression/jbmc-generics/Makefile +++ /dev/null @@ -1,36 +0,0 @@ -default: tests.log - -include ../../src/config.inc - -test: - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading - -tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.java" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log tests-symex-driven-loading.log - -%.class: %.java ../../src/org.cprover.jar - javac -g -cp ../../src/org.cprover.jar:. $< - -nondet_java_files := $(shell find . -name "Nondet*.java") -nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files)) - -.PHONY: nondet-class-files -nondet-class-files: $(nondet_class_files) - -.PHONY: clean-nondet-class-files -clean-nondet-class-files: - -rm $(nondet_class_files) diff --git a/jbmc/regression/jbmc-inheritance/Makefile b/jbmc/regression/jbmc-inheritance/Makefile deleted file mode 100644 index 3d2b16bfdac..00000000000 --- a/jbmc/regression/jbmc-inheritance/Makefile +++ /dev/null @@ -1,34 +0,0 @@ -default: tests.log - -include ../../src/config.inc - -test: - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" - -tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.java" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log - -%.class: %.java ../../src/org.cprover.jar - javac -g -cp ../../src/org.cprover.jar:. $< - -nondet_java_files := $(shell find . -name "Nondet*.java") -nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files)) - -.PHONY: nondet-class-files -nondet-class-files: $(nondet_class_files) - -.PHONY: clean-nondet-class-files -clean-nondet-class-files: - -rm $(nondet_class_files) diff --git a/jbmc/regression/jbmc-json-ui/Makefile b/jbmc/regression/jbmc-json-ui/Makefile deleted file mode 100644 index df528766e1f..00000000000 --- a/jbmc/regression/jbmc-json-ui/Makefile +++ /dev/null @@ -1,37 +0,0 @@ -default: tests.log - -include ../../src/config.inc - -test: -ifeq (, $(shell which jq)) - echo "JBMC JSON-UI tests skipped (can't find 'jq' in your path)" -else - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../chain.sh ../../../src/jbmc/jbmc" -endif - -tests.log: ../$(CPROVER_DIR)/regression/test.pl test - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.java" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log tests-symex-driven-loading.log - -%.class: %.java ../../src/org.cprover.jar - javac -g -cp ../../src/org.cprover.jar:. $< - -nondet_java_files := $(shell find . -name "Nondet*.java") -nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files)) - -.PHONY: nondet-class-files -nondet-class-files: $(nondet_class_files) - -.PHONY: clean-nondet-class-files -clean-nondet-class-files: - -rm $(nondet_class_files) diff --git a/jbmc/regression/jbmc-strings/Makefile b/jbmc/regression/jbmc-strings/Makefile deleted file mode 100644 index 98ddf3b06e8..00000000000 --- a/jbmc/regression/jbmc-strings/Makefile +++ /dev/null @@ -1,31 +0,0 @@ -default: tests.log - -include ../../src/config.inc - -test: - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading - -testfuture: - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading - -testall: - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading - -tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.c" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log tests-symex-driven-loading.log diff --git a/jbmc/regression/jbmc/Makefile b/jbmc/regression/jbmc/Makefile deleted file mode 100644 index aaf7efdf539..00000000000 --- a/jbmc/regression/jbmc/Makefile +++ /dev/null @@ -1,44 +0,0 @@ -default: tests.log - -include ../../src/config.inc - -test: - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),) - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading -else - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading -endif - -tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),) - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading -else - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading -endif - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.java" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log tests-symex-driven-loading.log - -%.class: %.java ../../src/org.cprover.jar - javac -g -cp ../../src/org.cprover.jar:. $< - -nondet_java_files := $(shell find . -name "Nondet*.java") -nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files)) - -.PHONY: nondet-class-files -nondet-class-files: $(nondet_class_files) - -.PHONY: clean-nondet-class-files -clean-nondet-class-files: - -rm $(nondet_class_files) diff --git a/jbmc/regression/jbmc/lvt-unexpected/Makefile b/jbmc/regression/jbmc/lvt-unexpected/Makefile deleted file mode 100644 index 8fb160582c0..00000000000 --- a/jbmc/regression/jbmc/lvt-unexpected/Makefile +++ /dev/null @@ -1,7 +0,0 @@ - -T=unexpected - -all : $T.class - -%.class : %.j - jasmin $< diff --git a/jbmc/regression/jdiff/Makefile b/jbmc/regression/jdiff/Makefile deleted file mode 100644 index a84206a8d9a..00000000000 --- a/jbmc/regression/jdiff/Makefile +++ /dev/null @@ -1,20 +0,0 @@ -default: tests.log - -include ../../src/config.inc - -test: - @../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/jdiff/jdiff - -tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -e -p -c ../../../src/jdiff/jdiff - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.c" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - $(RM) tests.log diff --git a/jbmc/regression/strings-smoke-tests/Makefile b/jbmc/regression/strings-smoke-tests/Makefile deleted file mode 100644 index 98ddf3b06e8..00000000000 --- a/jbmc/regression/strings-smoke-tests/Makefile +++ /dev/null @@ -1,31 +0,0 @@ -default: tests.log - -include ../../src/config.inc - -test: - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading - -testfuture: - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading - -testall: - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading - -tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" - @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.c" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log tests-symex-driven-loading.log diff --git a/jbmc/src/Makefile b/jbmc/src/Makefile deleted file mode 100644 index 83dd32eee29..00000000000 --- a/jbmc/src/Makefile +++ /dev/null @@ -1,67 +0,0 @@ -DIRS = janalyzer jbmc jdiff java_bytecode miniz -ROOT = ../ - -include config.inc - -.PHONY: all -all: janalyzer.dir jbmc.dir jdiff.dir - -# building cbmc proper -.PHONY: cprover.dir -cprover.dir: - $(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/src - -.PHONY: java_bytecode.dir -java_bytecode.dir: miniz.dir - -.PHONY: janalyzer.dir -janalyzer.dir: java_bytecode.dir cprover.dir - -.PHONY: jbmc.dir -jbmc.dir: java_bytecode.dir cprover.dir - -.PHONY: jdiff.dir -jdiff.dir: java_bytecode.dir cprover.dir - -.PHONY: miniz.dir -miniz.dir: - -$(patsubst %, %.dir, $(DIRS)): - ## Entering $(basename $@) - $(MAKE) $(MAKEARGS) -C $(basename $@) - -# generate source files - -$(patsubst %, %_generated_files, $(DIRS)): - $(MAKE) $(MAKEARGS) -C $(patsubst %_generated_files, %, $@) generated_files - -.PHONY: generated_files -generated_files: $(patsubst %, %_generated_files, $(DIRS)) - -# cleaning - -.PHONY: clean -clean: $(patsubst %, %_clean, $(DIRS)) cprover_clean dist_clean - -$(patsubst %, %_clean, $(DIRS)): - $(MAKE) $(MAKEARGS) -C $(patsubst %_clean, %, $@) clean ; \ - -.PHONY: cprover_clean -cprover_clean: - $(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/src clean - -.PHONY: dist_clean -dist_clean: - rm -rf $(ROOT)dist - -setup-submodules: - git submodule update --init - -.PHONY: dist -dist: setup-submodules all - mkdir -p $(ROOT)dist/lib - cp ../lib/java-models-library/target/core-models.jar $(ROOT)dist/lib - mkdir -p $(ROOT)dist/bin - cp jbmc/jbmc $(ROOT)dist/bin - cp janalyzer/janalyzer $(ROOT)dist/bin - cp jdiff/jdiff $(ROOT)dist/bin diff --git a/jbmc/src/janalyzer/Makefile b/jbmc/src/janalyzer/Makefile deleted file mode 100644 index f1fc8fcf0fa..00000000000 --- a/jbmc/src/janalyzer/Makefile +++ /dev/null @@ -1,50 +0,0 @@ -SRC = janalyzer_main.cpp \ - janalyzer_parse_options.cpp \ - # Empty last line - -OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ - ../java_bytecode/java_bytecode$(LIBEXT) \ - ../$(CPROVER_DIR)/src/linking/linking$(LIBEXT) \ - ../$(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \ - ../$(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \ - ../$(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \ - ../$(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \ - ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \ - ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \ - ../$(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \ - ../$(CPROVER_DIR)/src/util/util$(LIBEXT) \ - ..//miniz/miniz$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-analyzer/static_show_domain$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-analyzer/static_simplifier$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-analyzer/static_verifier$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-analyzer/taint_analysis$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-analyzer/taint_parser$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-analyzer/unreachable_instructions$(OBJEXT) \ - # Empty last line - -INCLUDES= -I .. -I ../$(CPROVER_DIR)/src - -LIBS = - -include ../config.inc -include ../$(CPROVER_DIR)/src/config.inc -include ../$(CPROVER_DIR)/src/common - -CLEANFILES = janalyzer$(EXEEXT) - -all: janalyzer$(EXEEXT) - -ifneq ($(wildcard ../jsil/Makefile),) - OBJ += ../jsil/jsil$(LIBEXT) - CP_CXXFLAGS += -DHAVE_JSIL -endif - -############################################################################### - -janalyzer$(EXEEXT): $(OBJ) - $(LINKBIN) - -.PHONY: janalyzer-mac-signed - -janalyzer-mac-signed: janalyzer$(EXEEXT) - strip janalyzer$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) janalyzer$(EXEEXT) diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile deleted file mode 100644 index dd590274fd9..00000000000 --- a/jbmc/src/java_bytecode/Makefile +++ /dev/null @@ -1,82 +0,0 @@ -SRC = assignments_from_json.cpp \ - bytecode_info.cpp \ - character_refine_preprocess.cpp \ - ci_lazy_methods.cpp \ - ci_lazy_methods_needed.cpp \ - code_with_references.cpp \ - convert_java_nondet.cpp \ - create_array_with_type_intrinsic.cpp \ - expr2java.cpp \ - generic_parameter_specialization_map.cpp \ - generic_parameter_specialization_map_keys.cpp \ - jar_file.cpp \ - jar_pool.cpp \ - java_bmc_util.cpp \ - java_bytecode_convert_class.cpp \ - java_bytecode_convert_method.cpp \ - java_bytecode_concurrency_instrumentation.cpp \ - java_bytecode_instrument.cpp \ - java_bytecode_internal_additions.cpp \ - java_bytecode_language.cpp \ - java_bytecode_parse_tree.cpp \ - java_bytecode_parser.cpp \ - java_bytecode_typecheck.cpp \ - java_bytecode_typecheck_code.cpp \ - java_bytecode_typecheck_expr.cpp \ - java_bytecode_typecheck_type.cpp \ - java_class_loader.cpp \ - java_class_loader_base.cpp \ - java_class_loader_limit.cpp \ - java_enum_static_init_unwind_handler.cpp \ - java_entry_point.cpp \ - java_local_variable_table.cpp \ - java_multi_path_symex_checker.cpp \ - java_object_factory.cpp \ - java_object_factory_parameters.cpp \ - java_pointer_casts.cpp \ - java_qualifiers.cpp \ - java_root_class.cpp \ - java_single_path_symex_checker.cpp \ - java_static_initializers.cpp \ - java_string_library_preprocess.cpp \ - java_string_literals.cpp \ - java_trace_validation.cpp \ - java_types.cpp \ - java_utils.cpp \ - lambda_synthesis.cpp \ - lazy_goto_model.cpp \ - lift_clinit_calls.cpp \ - load_method_by_regex.cpp \ - mz_zip_archive.cpp \ - remove_exceptions.cpp \ - remove_instanceof.cpp \ - remove_java_new.cpp \ - replace_java_nondet.cpp \ - select_pointer_type.cpp \ - simple_method_stubbing.cpp \ - # Empty last line - -INCLUDES= -I .. -I ../$(CPROVER_DIR)/src - -include ../config.inc -include ../$(CPROVER_DIR)/src/config.inc -include ../$(CPROVER_DIR)/src/common - -CLEANFILES = java_bytecode$(LIBEXT) - -all: library java_bytecode$(LIBEXT) - -clean: clean_library - -.PHONY: clean_library -clean_library: - $(MAKE) clean -C library - -.PHONY: library -library: - $(MAKE) -C library - -############################################################################### - -java_bytecode$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/jbmc/src/java_bytecode/library/Makefile b/jbmc/src/java_bytecode/library/Makefile deleted file mode 100644 index 5d843042907..00000000000 --- a/jbmc/src/java_bytecode/library/Makefile +++ /dev/null @@ -1,37 +0,0 @@ -SRC = converter.cpp \ - # Empty last line - -OBJ += - -INCLUDES= - -LIBS = - -LIBRARY_DIR = ../../../lib/java-models-library - -include ../../config.inc -include ../../$(CPROVER_DIR)/src/config.inc -include ../../$(CPROVER_DIR)/src/common - -CLEANFILES = converter$(EXEEXT) - -all: library converter$(EXEEXT) - -clean: clean_library - -.PHONY: clean_library -clean_library: - rm -rf core-models.jar - if [ -d $(LIBRARY_DIR) ]; then cd $(LIBRARY_DIR); mvn --quiet clean; fi - -.PHONY: library -library: - if [ -d $(LIBRARY_DIR) ]; then \ - (cd $(LIBRARY_DIR); mvn --quiet -Dmaven.test.skip=true package); \ - cp $(LIBRARY_DIR)/target/core-models.jar .; \ - fi - -############################################################################### - -converter$(EXEEXT): $(OBJ) - $(LINKBIN) diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile deleted file mode 100644 index aa34a1f1810..00000000000 --- a/jbmc/src/jbmc/Makefile +++ /dev/null @@ -1,64 +0,0 @@ -SRC = jbmc_main.cpp \ - jbmc_parse_options.cpp \ - # Empty last line - -OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ - ../java_bytecode/java_bytecode$(LIBEXT) \ - ../$(CPROVER_DIR)/src/linking/linking$(LIBEXT) \ - ../$(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \ - ../$(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \ - ../$(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \ - ../$(CPROVER_DIR)/src/goto-symex/goto-symex$(LIBEXT) \ - ../$(CPROVER_DIR)/src/pointer-analysis/value_set$(OBJEXT) \ - ../$(CPROVER_DIR)/src/pointer-analysis/value_set_analysis_fi$(OBJEXT) \ - ../$(CPROVER_DIR)/src/pointer-analysis/value_set_domain_fi$(OBJEXT) \ - ../$(CPROVER_DIR)/src/pointer-analysis/value_set_fi$(OBJEXT) \ - ../$(CPROVER_DIR)/src/pointer-analysis/value_set_dereference$(OBJEXT) \ - ../$(CPROVER_DIR)/src/pointer-analysis/add_failed_symbols$(OBJEXT) \ - ../$(CPROVER_DIR)/src/pointer-analysis/rewrite_index$(OBJEXT) \ - ../$(CPROVER_DIR)/src/pointer-analysis/goto_program_dereference$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/full_slicer$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/reachability_slicer$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/nondet_static$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/source_lines$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_basic_blocks$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_filter$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_branch$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_condition$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_decision$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_location$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_mcdc$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_other$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_util$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \ - ../$(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \ - ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \ - ../$(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \ - ../$(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \ - ../$(CPROVER_DIR)/src/util/util$(LIBEXT) \ - ../miniz/miniz$(OBJEXT) \ - ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \ - # Empty last line - -INCLUDES= -I .. -I ../$(CPROVER_DIR)/src - -LIBS = - -include ../config.inc -include ../$(CPROVER_DIR)/src/config.inc -include ../$(CPROVER_DIR)/src/common - -CLEANFILES = jbmc$(EXEEXT) - -all: jbmc$(EXEEXT) - -############################################################################### - -jbmc$(EXEEXT): $(OBJ) - $(LINKBIN) - -.PHONY: jbmc-mac-signed - -jbmc-mac-signed: jbmc$(EXEEXT) - strip jbmc$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) jbmc$(EXEEXT) diff --git a/jbmc/src/jdiff/Makefile b/jbmc/src/jdiff/Makefile deleted file mode 100644 index 4ceab462591..00000000000 --- a/jbmc/src/jdiff/Makefile +++ /dev/null @@ -1,57 +0,0 @@ -SRC = jdiff_languages.cpp \ - jdiff_main.cpp \ - jdiff_parse_options.cpp \ - java_syntactic_diff.cpp \ - # Empty last line - -OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ - ..//java_bytecode/java_bytecode$(LIBEXT) \ - ../$(CPROVER_DIR)/src/linking/linking$(LIBEXT) \ - ../$(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \ - ../$(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \ - ../$(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \ - ../$(CPROVER_DIR)/src/goto-diff/syntactic_diff$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-diff/unified_diff$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-diff/change_impact$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-diff/goto_diff_base$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/source_lines$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_basic_blocks$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_filter$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_branch$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_condition$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_decision$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_location$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_mcdc$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_other$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/cover_util$(OBJEXT) \ - ../$(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \ - ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \ - ../$(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \ - ../$(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \ - ../$(CPROVER_DIR)/src/util/util$(LIBEXT) \ - ../miniz/miniz$(OBJEXT) \ - ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \ - # Empty last line - -INCLUDES= -I .. -I ../$(CPROVER_DIR)/src - -LIBS = - -include ../config.inc -include ../$(CPROVER_DIR)/src/config.inc -include ../$(CPROVER_DIR)/src/common - -CLEANFILES = jdiff$(EXEEXT) - -all: jdiff$(EXEEXT) - -############################################################################### - -jdiff$(EXEEXT): $(OBJ) - $(LINKBIN) - -.PHONY: jdiff-mac-signed - -jdiff-mac-signed: jdiff$(EXEEXT) - strip jdiff$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) jdiff$(EXEEXT) diff --git a/jbmc/src/miniz/Makefile b/jbmc/src/miniz/Makefile deleted file mode 100644 index d7c937a7dd1..00000000000 --- a/jbmc/src/miniz/Makefile +++ /dev/null @@ -1,14 +0,0 @@ -SRC = miniz.cpp \ - # Empty last line - -INCLUDES= -I ../$(CPROVER_DIR)/src - -include ../config.inc -include ../$(CPROVER_DIR)/src/config.inc -include ../$(CPROVER_DIR)/src/common - -CLEANFILES = miniz$(OBJEXT) - -all: miniz$(OBJEXT) - -############################################################################### diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile deleted file mode 100644 index d18567da013..00000000000 --- a/jbmc/unit/Makefile +++ /dev/null @@ -1,156 +0,0 @@ -.PHONY: all jprover.dir test java-testing-utils-clean - -# Source files for test utilities -SRC = $(CPROVER_DIR)/unit/unit_tests.cpp \ - # Empty last line - -# Test source files -SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ - java_bytecode/expr2java.cpp \ - java_bytecode/goto_program_generics/generic_bases_test.cpp \ - java_bytecode/goto_program_generics/generic_parameters_test.cpp \ - java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \ - java_bytecode/goto-programs/class_hierarchy_graph.cpp \ - java_bytecode/goto-programs/class_hierarchy_output.cpp \ - java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp \ - java_bytecode/inherited_static_fields/inherited_static_fields.cpp \ - java_bytecode/java_bytecode_convert_class/add_java_array_types.cpp \ - java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \ - java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp \ - java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp \ - java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \ - java_bytecode/java_bytecode_convert_method/convert_method.cpp \ - java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp \ - java_bytecode/java_bytecode_language/language.cpp \ - java_bytecode/java_bytecode_language/context_excluded.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_lvtt_generic_local_vars.cpp \ - java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \ - java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \ - java_bytecode/java_bytecode_parser/parse_class_without_instructions.cpp \ - java_bytecode/java_bytecode_parser/parse_inner_class.cpp \ - java_bytecode/java_bytecode_parser/parse_java_annotations.cpp \ - java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \ - java_bytecode/java_bytecode_parser/parse_java_class.cpp \ - java_bytecode/java_bytecode_parser/parse_java_field.cpp \ - java_bytecode/java_object_factory/gen_nondet_string_init.cpp \ - java_bytecode/java_object_factory/struct_tag_types.cpp \ - java_bytecode/java_replace_nondet/replace_nondet.cpp \ - java_bytecode/java_static_initializers/assignments_from_json.cpp \ - java_bytecode/java_static_initializers/java_static_initializers.cpp \ - java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \ - java_bytecode/java_trace_validation/java_trace_validation.cpp \ - java_bytecode/java_types/erase_type_arguments.cpp \ - java_bytecode/java_types/generic_type_index.cpp \ - java_bytecode/java_types/java_generic_symbol_type.cpp \ - java_bytecode/java_types/java_type_from_string.cpp \ - java_bytecode/java_string_literals.cpp \ - java_bytecode/java_utils_test.cpp \ - java_bytecode/java_virtual_functions/virtual_functions.cpp \ - java_bytecode/load_method_by_regex.cpp \ - pointer-analysis/custom_value_set_analysis.cpp \ - solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp \ - solvers/strings/string_refinement/dependency_graph.cpp \ - solvers/strings/string_refinement/string_symbol_resolution.cpp \ - util/expr_iterator.cpp \ - util/has_subtype.cpp \ - util/parameter_indices.cpp \ - util/simplify_expr.cpp \ - # Empty last line - -INCLUDES= -I ../src/ -I. -I $(CPROVER_DIR)/src -I $(CPROVER_DIR)/unit - -include ../src/config.inc -include $(CPROVER_DIR)/src/config.inc -include $(CPROVER_DIR)/src/common - -jprover.dir: - $(MAKE) $(MAKEARGS) -C ../src - -$(CPROVER_DIR)/unit/testing-utils/testing-utils$(LIBEXT): jprover.dir - $(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/unit/testing-utils - -java-testing-utils/java-testing-utils$(LIBEXT): jprover.dir - $(MAKE) $(MAKEARGS) -C java-testing-utils - -java-testing-utils-clean: - $(MAKE) $(MAKEARGS) -C java-testing-utils clean - -CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \ - ../src/miniz/miniz$(OBJEXT) \ - $(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ - $(CPROVER_DIR)/src/cpp/cpp$(LIBEXT) \ - $(CPROVER_DIR)/src/json/json$(LIBEXT) \ - $(CPROVER_DIR)/src/json-symtab-language/json-symtab-language$(LIBEXT) \ - $(CPROVER_DIR)/src/linking/linking$(LIBEXT) \ - $(CPROVER_DIR)/src/util/util$(LIBEXT) \ - $(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \ - $(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \ - $(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \ - $(CPROVER_DIR)/src/goto-symex/goto-symex$(LIBEXT) \ - $(CPROVER_DIR)/src/goto-instrument/source_lines$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/cover_basic_blocks$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/cover_filter$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/cover_instrument_branch$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/cover_instrument_condition$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/cover_instrument_decision$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/cover_instrument_location$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/cover_instrument_mcdc$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/cover_instrument_other$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/cover_util$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/reachability_slicer$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/nondet_static$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/full_slicer$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \ - $(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \ - $(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \ - $(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \ - $(CPROVER_DIR)/src/assembler/assembler$(LIBEXT) \ - $(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \ - $(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \ - # Empty last line - -OBJ += $(CPROVER_LIBS) \ - $(CPROVER_DIR)/unit/testing-utils/testing-utils$(LIBEXT) \ - java-testing-utils/java-testing-utils$(LIBEXT) - -CATCH_TEST = unit_tests$(EXEEXT) -N_CATCH_TESTS = $(shell \ - cat $$(find . -name "*.cpp" ) | \ - grep -c -E "(SCENARIO|TEST_CASE)") - -CLEANFILES = $(CATCH_TEST) java-testing-utils/java-testing-utils$(LIBEXT) - -# only add a dependency for libraries to avoid triggering implicit rules, which -# would cause unnecessary rebuilds -$(filter %$(LIBEXT), CPROVER_LIBS): jprover.dir - -all: $(CATCH_TEST) - -clean: java-testing-utils-clean - -test: $(CATCH_TEST) - # Include hidden tests by specifying "*,[.]" for tests to count - if ! ./$(CATCH_TEST) "*,[.]" -l | grep -q "^$(N_CATCH_TESTS) matching test cases" ; then \ - ./$(CATCH_TEST) "*,[.]" -l ; fi - ./$(CATCH_TEST) ${TAGS} - - -############################################################################### - -unit_tests$(EXEEXT): $(OBJ) - $(LINKBIN) diff --git a/jbmc/unit/java-testing-utils/Makefile b/jbmc/unit/java-testing-utils/Makefile deleted file mode 100644 index b564c11ad13..00000000000 --- a/jbmc/unit/java-testing-utils/Makefile +++ /dev/null @@ -1,20 +0,0 @@ -SRC = \ - load_java_class.cpp \ - require_goto_statements.cpp \ - require_parse_tree.cpp \ - require_type.cpp \ - # Empty last line (please keep above list sorted!) - -INCLUDES = -I .. -I . -I ../../src -I ../$(CPROVER_DIR)/src -I ../$(CPROVER_DIR)/unit - -include ../../src/config.inc -include ../$(CPROVER_DIR)/src/config.inc -include ../$(CPROVER_DIR)/src/common - -CLEANFILES = java-testing-utils$(LIBEXT) - -.PHONY: all -all: java-testing-utils$(LIBEXT) - -java-testing-utils$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/Makefile b/src/Makefile deleted file mode 100644 index 2bd3e7218c1..00000000000 --- a/src/Makefile +++ /dev/null @@ -1,166 +0,0 @@ -DIRS = analyses \ - ansi-c \ - assembler \ - big-int \ - cbmc \ - cpp \ - goto-analyzer \ - goto-cc \ - goto-checker \ - goto-diff \ - goto-instrument \ - goto-harness \ - goto-programs \ - goto-symex \ - jsil \ - json \ - json-symtab-language \ - langapi \ - linking \ - memory-analyzer \ - pointer-analysis \ - solvers \ - statement-list \ - symtab2gb \ - util \ - xmllang \ - # Empty last line - -all: cbmc.dir \ - goto-analyzer.dir \ - goto-cc.dir \ - goto-diff.dir \ - goto-instrument.dir \ - goto-harness.dir \ - symtab2gb.dir \ - # Empty last line - -ifeq ($(OS),Windows_NT) - detected_OS := Windows -else - detected_OS := $(shell sh -c 'uname 2>/dev/null || echo Unknown') -endif - -ifeq ($(detected_OS),Linux) - all: memory-analyzer.dir -else ifeq ($(WITH_MEMORY_ANALYZER),1) - all: memory-analyzer.dir -endif - -############################################################################### - -util.dir: big-int.dir - -# everything but big-int depends on util -$(patsubst %, %.dir, $(filter-out big-int util, $(DIRS))): util.dir - -.PHONY: languages -.PHONY: clean - -cpp.dir: ansi-c.dir linking.dir - -languages: util.dir langapi.dir \ - cpp.dir ansi-c.dir xmllang.dir assembler.dir \ - jsil.dir json.dir json-symtab-language.dir statement-list.dir - -solvers.dir: util.dir - -goto-harness.dir: util.dir goto-programs.dir langapi.dir linking.dir \ - json.dir json-symtab-language.dir \ - goto-instrument.dir - -goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \ - goto-symex.dir linking.dir analyses.dir solvers.dir - -goto-checker.dir: solvers.dir goto-symex.dir goto-programs.dir - -cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \ - pointer-analysis.dir goto-programs.dir linking.dir \ - goto-instrument.dir goto-checker.dir - -goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \ - goto-instrument.dir goto-checker.dir - -goto-diff.dir: languages goto-programs.dir pointer-analysis.dir \ - linking.dir analyses.dir goto-instrument.dir \ - solvers.dir goto-symex.dir - -goto-cc.dir: languages goto-programs.dir linking.dir - -memory-analyzer.dir: util.dir goto-programs.dir ansi-c.dir - -symtab2gb.dir: util.dir goto-programs.dir langapi.dir linking.dir \ - json.dir json-symtab-language.dir - -# building for a particular directory - -$(patsubst %, %.dir, $(DIRS)): - ## Entering $(basename $@) - $(MAKE) $(MAKEARGS) -C $(basename $@) - -# generate source files - -$(patsubst %, %_generated_files, $(DIRS)): - $(MAKE) $(MAKEARGS) -C $(patsubst %_generated_files, %, $@) generated_files - -generated_files: $(patsubst %, %_generated_files, $(DIRS)) - -# cleaning - -clean: $(patsubst %, %_clean, $(DIRS)) - -$(patsubst %, %_clean, $(DIRS)): - $(MAKE) $(MAKEARGS) -C $(patsubst %_clean, %, $@) clean ; \ - -# minisat2 and glucose download, for your convenience - -DOWNLOADER = lwp-download -TAR = tar - -minisat2-download: - @echo "Downloading Minisat 2.2.1" - @for i in $$(seq 1 3) ; do \ - $(DOWNLOADER) \ - http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz && \ - exit 0 ; \ - $(RM) minisat2_2.2.1.orig.tar.gz ; \ - if [ $$i -lt 3 ] ; then echo "Re-trying in 10 seconds" 1>&2 ; sleep 10 ; fi ; \ - done ; exit 1 - @$(TAR) xfz minisat2_2.2.1.orig.tar.gz - @rm -Rf ../minisat-2.2.1 - @mv minisat2-2.2.1 ../minisat-2.2.1 - @(cd ../minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch) - @rm minisat2_2.2.1.orig.tar.gz - -cudd-download: - @echo "Downloading Cudd 3.0.0" - @$(DOWNLOADER) https://sourceforge.net/projects/cudd-mirror/files/cudd-3.0.0.tar.gz/download cudd-3.0.0.tar.gz - @$(TAR) xfz cudd-3.0.0.tar.gz - @$(RM) -r ../cudd-3.0.0 - @mv cudd-3.0.0 ../ - @$(RM) cudd-3.0.0.tar.gz - @echo "Compiling Cudd 3.0.0" - @(cd ../cudd-3.0.0; ./configure; $(MAKE)) - -glucose-download: - @echo "Downloading glucose-syrup" - @$(DOWNLOADER) http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz - @$(TAR) xfz glucose-syrup.tgz - @rm -Rf ../glucose-syrup - @mv glucose-syrup ../ - @(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch) - @rm glucose-syrup.tgz - -cadical_release = rel-06w -cadical-download: - @echo "Downloading CaDiCaL $(cadical_release)" - @curl -L https://github.com/arminbiere/cadical/archive/$(cadical_release).tar.gz | tar xz - @rm -Rf ../cadical - @mv cadical-$(cadical_release) ../cadical - @(cd ../cadical; patch -p1 < ../scripts/cadical-patch) - @cd ../cadical && CXX=$(CXX) CXXFLAGS=-O3 ./configure --debug && make - -doc : - doxygen - -.PHONY: minisat2-download cudd-download glucose-download cadical-download diff --git a/src/analyses/Makefile b/src/analyses/Makefile deleted file mode 100644 index 510ab7646cd..00000000000 --- a/src/analyses/Makefile +++ /dev/null @@ -1,54 +0,0 @@ -SRC = ai.cpp \ - ai_domain.cpp \ - ai_history.cpp \ - call_graph.cpp \ - call_graph_helpers.cpp \ - call_stack_history.cpp \ - constant_propagator.cpp \ - custom_bitvector_analysis.cpp \ - dependence_graph.cpp \ - dirty.cpp \ - does_remove_const.cpp \ - escape_analysis.cpp \ - flow_insensitive_analysis.cpp \ - global_may_alias.cpp \ - goto_check.cpp \ - goto_rw.cpp \ - guard_bdd.cpp \ - guard_expr.cpp \ - interval_analysis.cpp \ - interval_domain.cpp \ - invariant_propagation.cpp \ - invariant_set.cpp \ - invariant_set_domain.cpp \ - is_threaded.cpp \ - local_bitvector_analysis.cpp \ - local_cfg.cpp \ - local_control_flow_history.cpp \ - local_may_alias.cpp \ - local_safe_pointers.cpp \ - locals.cpp \ - reaching_definitions.cpp \ - sese_regions.cpp \ - static_analysis.cpp \ - uncaught_exceptions_analysis.cpp \ - uninitialized_domain.cpp \ - # Empty last line - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = analyses$(LIBEXT) - -all: analyses$(LIBEXT) - -ifneq ($(CUDD),) - OBJ += $(CUDD)/cudd/.libs/libcudd$(LIBEXT) $(CUDD)/cplusplus/.libs/libobj$(LIBEXT) -endif - -############################################################################### - -analyses$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile deleted file mode 100644 index b4163349e4a..00000000000 --- a/src/ansi-c/Makefile +++ /dev/null @@ -1,128 +0,0 @@ -SRC = anonymous_member.cpp \ - ansi_c_convert_type.cpp \ - ansi_c_declaration.cpp \ - ansi_c_entry_point.cpp \ - ansi_c_internal_additions.cpp \ - ansi_c_language.cpp \ - ansi_c_lex.yy.cpp \ - ansi_c_parse_tree.cpp \ - ansi_c_parser.cpp \ - ansi_c_scope.cpp \ - ansi_c_typecheck.cpp \ - ansi_c_y.tab.cpp \ - builtin_factory.cpp \ - c_misc.cpp \ - c_nondet_symbol_factory.cpp \ - c_object_factory_parameters.cpp \ - c_preprocess.cpp \ - c_qualifiers.cpp \ - c_storage_spec.cpp \ - c_typecast.cpp \ - c_typecheck_base.cpp \ - c_typecheck_code.cpp \ - c_typecheck_expr.cpp \ - c_typecheck_gcc_polymorphic_builtins.cpp \ - c_typecheck_initializer.cpp \ - c_typecheck_type.cpp \ - c_typecheck_typecast.cpp \ - cprover_library.cpp \ - designator.cpp \ - expr2c.cpp \ - gcc_types.cpp \ - gcc_version.cpp \ - literals/convert_character_literal.cpp \ - literals/convert_float_literal.cpp \ - literals/convert_integer_literal.cpp \ - literals/convert_string_literal.cpp \ - literals/parse_float.cpp \ - literals/unescape_string.cpp \ - padding.cpp \ - preprocessor_line.cpp \ - type2name.cpp \ - # Empty last line - -INCLUDES= -I .. - -include ../config.inc -include ../common - -BUILTIN_FILES = \ - arm_builtin_headers.inc \ - clang_builtin_headers.inc \ - cprover_builtin_headers.inc \ - cw_builtin_headers.inc \ - gcc_builtin_headers_alpha.inc \ - gcc_builtin_headers_arm.inc \ - gcc_builtin_headers_generic.inc \ - gcc_builtin_headers_ia32-2.inc \ - gcc_builtin_headers_ia32-3.inc \ - gcc_builtin_headers_ia32-4.inc \ - gcc_builtin_headers_ia32.inc \ - gcc_builtin_headers_math.inc \ - gcc_builtin_headers_mem_string.inc \ - gcc_builtin_headers_mips.inc \ - gcc_builtin_headers_omp.inc \ - gcc_builtin_headers_power.inc \ - gcc_builtin_headers_tm.inc \ - gcc_builtin_headers_types.inc \ - gcc_builtin_headers_ubsan.inc \ - windows_builtin_headers.inc - -CLEANFILES = ansi-c$(LIBEXT) \ - ansi_c_y.tab.h ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.cpp.output \ - ansi_c_y.output \ - library/converter$(EXEEXT) cprover_library.inc \ - file_converter$(EXEEXT) library_check \ - $(BUILTIN_FILES) - -all: ansi-c$(LIBEXT) - -############################################################################### - -ansi_c_y.tab.cpp: parser.y - $(YACC) $(YFLAGS) $$flags -pyyansi_c parser.y --defines=ansi_c_y.tab.h -o $@ - -ansi_c_y.tab.h: ansi_c_y.tab.cpp - -ansi_c_lex.yy.cpp: scanner.l - $(LEX) -Pyyansi_c -o$@ scanner.l - -# extra dependencies -ansi_c_y.tab$(OBJEXT): ansi_c_y.tab.cpp ansi_c_y.tab.h -ansi_c_lex.yy$(OBJEXT): ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.h -cprover_library$(OBJEXT): cprover_library.inc - -############################################################################### - -library/converter$(EXEEXT): library/converter.cpp - $(LINKNATIVE) - -file_converter$(EXEEXT): file_converter.cpp - $(LINKNATIVE) - -ifeq ($(BUILD_ENV),MinGW) - platform_unavail = library/java.io.c library/err.c library/threads.c -else - platform_unavail = library/java.io.c library/threads.c -endif -library_check: library/*.c - ./library_check.sh $(CC) $(filter-out $(platform_unavail), $^) - touch $@ - -cprover_library.inc: library/converter$(EXEEXT) library/*.c - library/converter$(EXEEXT) library/*.c > $@ - -%.inc: %.h file_converter$(EXEEXT) - ./file_converter$(EXEEXT) $< > $@ - -ansi_c_internal_additions$(OBJEXT): $(BUILTIN_FILES) - -generated_files: \ - ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.h \ - cprover_library.inc \ - $(BUILTIN_FILES) - -############################################################################### - -ansi-c$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/assembler/Makefile b/src/assembler/Makefile deleted file mode 100644 index 57638617bdd..00000000000 --- a/src/assembler/Makefile +++ /dev/null @@ -1,25 +0,0 @@ -SRC = assembler_lex.yy.cpp \ - assembler_parser.cpp \ - remove_asm.cpp \ - # Empty last line -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = assembler$(LIBEXT) \ - assembler_lex.yy.cpp - -all: assembler$(LIBEXT) - -############################################################################### - -assembler_lex.yy.cpp: scanner.l - $(LEX) -Pyyassembler -o$@ scanner.l - -generated_files: assembler_lex.yy.cpp - -############################################################################### - -assembler$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile deleted file mode 100644 index f2e80d151a0..00000000000 --- a/src/cbmc/Makefile +++ /dev/null @@ -1,76 +0,0 @@ -SRC = c_test_input_generator.cpp \ - cbmc_languages.cpp \ - cbmc_main.cpp \ - cbmc_parse_options.cpp \ - # Empty last line - -OBJ += ../ansi-c/ansi-c$(LIBEXT) \ - ../cpp/cpp$(LIBEXT) \ - ../json/json$(LIBEXT) \ - ../json-symtab-language/json-symtab-language$(LIBEXT) \ - ../statement-list/statement-list$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ - ../big-int/big-int$(LIBEXT) \ - ../goto-checker/goto-checker$(LIBEXT) \ - ../goto-programs/goto-programs$(LIBEXT) \ - ../goto-symex/goto-symex$(LIBEXT) \ - ../pointer-analysis/value_set$(OBJEXT) \ - ../pointer-analysis/value_set_analysis_fi$(OBJEXT) \ - ../pointer-analysis/value_set_domain_fi$(OBJEXT) \ - ../pointer-analysis/value_set_fi$(OBJEXT) \ - ../pointer-analysis/value_set_dereference$(OBJEXT) \ - ../pointer-analysis/add_failed_symbols$(OBJEXT) \ - ../pointer-analysis/rewrite_index$(OBJEXT) \ - ../pointer-analysis/goto_program_dereference$(OBJEXT) \ - ../goto-instrument/source_lines$(OBJEXT) \ - ../goto-instrument/cover$(OBJEXT) \ - ../goto-instrument/cover_basic_blocks$(OBJEXT) \ - ../goto-instrument/cover_filter$(OBJEXT) \ - ../goto-instrument/cover_instrument_branch$(OBJEXT) \ - ../goto-instrument/cover_instrument_condition$(OBJEXT) \ - ../goto-instrument/cover_instrument_decision$(OBJEXT) \ - ../goto-instrument/cover_instrument_location$(OBJEXT) \ - ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ - ../goto-instrument/cover_instrument_other$(OBJEXT) \ - ../goto-instrument/cover_util$(OBJEXT) \ - ../goto-instrument/reachability_slicer$(OBJEXT) \ - ../goto-instrument/nondet_static$(OBJEXT) \ - ../goto-instrument/full_slicer$(OBJEXT) \ - ../goto-instrument/unwindset$(OBJEXT) \ - ../analyses/analyses$(LIBEXT) \ - ../langapi/langapi$(LIBEXT) \ - ../xmllang/xmllang$(LIBEXT) \ - ../assembler/assembler$(LIBEXT) \ - ../solvers/solvers$(LIBEXT) \ - ../util/util$(LIBEXT) \ - -INCLUDES= -I .. - -LIBS = - -include ../config.inc -include ../common - -CLEANFILES = cbmc$(EXEEXT) - -all: cbmc$(EXEEXT) - -ifneq ($(wildcard ../bv_refinement/Makefile),) - OBJ += ../bv_refinement/bv_refinement$(LIBEXT) - CP_CXXFLAGS += -DHAVE_BV_REFINEMENT -endif - -ifneq ($(wildcard ../jsil/Makefile),) - OBJ += ../jsil/jsil$(LIBEXT) - CP_CXXFLAGS += -DHAVE_JSIL -endif - -############################################################################### - -cbmc$(EXEEXT): $(OBJ) - $(LINKBIN) - -.PHONY: cbmc-mac-signed - -cbmc-mac-signed: cbmc$(EXEEXT) - strip cbmc$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) cbmc$(EXEEXT) diff --git a/src/cpp/Makefile b/src/cpp/Makefile deleted file mode 100644 index 8fb3215f584..00000000000 --- a/src/cpp/Makefile +++ /dev/null @@ -1,83 +0,0 @@ -SRC = cpp_constructor.cpp \ - cpp_convert_type.cpp \ - cpp_declaration.cpp \ - cpp_declarator.cpp \ - cpp_declarator_converter.cpp \ - cpp_destructor.cpp \ - cpp_enum_type.cpp \ - cpp_exception_id.cpp \ - cpp_id.cpp \ - cpp_instantiate_template.cpp \ - cpp_internal_additions.cpp \ - cpp_is_pod.cpp \ - cpp_language.cpp \ - cpp_name.cpp \ - cpp_namespace_spec.cpp \ - cpp_parse_tree.cpp \ - cpp_parser.cpp \ - cpp_scope.cpp \ - cpp_scopes.cpp \ - cpp_storage_spec.cpp \ - cpp_token_buffer.cpp \ - cpp_type2name.cpp \ - cpp_typecheck.cpp \ - cpp_typecheck_bases.cpp \ - cpp_typecheck_code.cpp \ - cpp_typecheck_compound_type.cpp \ - cpp_typecheck_constructor.cpp \ - cpp_typecheck_conversions.cpp \ - cpp_typecheck_declaration.cpp \ - cpp_typecheck_destructor.cpp \ - cpp_typecheck_enum_type.cpp \ - cpp_typecheck_expr.cpp \ - cpp_typecheck_fargs.cpp \ - cpp_typecheck_function.cpp \ - cpp_typecheck_initializer.cpp \ - cpp_typecheck_linkage_spec.cpp \ - cpp_typecheck_method_bodies.cpp \ - cpp_typecheck_namespace.cpp \ - cpp_typecheck_resolve.cpp \ - cpp_typecheck_static_assert.cpp \ - cpp_typecheck_template.cpp \ - cpp_typecheck_type.cpp \ - cpp_typecheck_using.cpp \ - cpp_typecheck_virtual_table.cpp \ - cpp_util.cpp \ - cprover_library.cpp \ - expr2cpp.cpp \ - parse.cpp \ - template_map.cpp \ - # Empty last line - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = cpp$(LIBEXT) cprover_library.inc library_check - -all: cpp$(LIBEXT) - -############################################################################### - -# extra dependencies -cprover_library$(OBJEXT): cprover_library.inc - -############################################################################### - -../ansi-c/library/converter$(EXEEXT): ../ansi-c/library/converter.cpp - $(MAKE) -C ../ansi-c library/converter$(EXEEXT) - -library_check: library/*.c - ../ansi-c/library_check.sh $(CC) $^ - touch $@ - -cprover_library.inc: ../ansi-c/library/converter$(EXEEXT) library/*.c - ../ansi-c/library/converter$(EXEEXT) library/*.c > $@ - -generated_files: cprover_library.inc - -############################################################################### - -cpp$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile deleted file mode 100644 index a41692727bc..00000000000 --- a/src/goto-analyzer/Makefile +++ /dev/null @@ -1,51 +0,0 @@ -SRC = goto_analyzer_main.cpp \ - goto_analyzer_parse_options.cpp \ - taint_analysis.cpp \ - taint_parser.cpp \ - unreachable_instructions.cpp \ - show_on_source.cpp \ - static_show_domain.cpp \ - static_simplifier.cpp \ - static_verifier.cpp \ - # Empty last line - -OBJ += ../ansi-c/ansi-c$(LIBEXT) \ - ../cpp/cpp$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ - ../big-int/big-int$(LIBEXT) \ - ../goto-checker/goto-checker$(LIBEXT) \ - ../goto-programs/goto-programs$(LIBEXT) \ - ../analyses/analyses$(LIBEXT) \ - ../pointer-analysis/pointer-analysis$(LIBEXT) \ - ../langapi/langapi$(LIBEXT) \ - ../json/json$(LIBEXT) \ - ../assembler/assembler$(LIBEXT) \ - ../solvers/solvers$(LIBEXT) \ - ../util/util$(LIBEXT) \ - # Empty last line - -INCLUDES= -I .. - -LIBS = - -include ../config.inc -include ../common - -CLEANFILES = goto-analyzer$(EXEEXT) - -all: goto-analyzer$(EXEEXT) - -ifneq ($(wildcard ../jsil/Makefile),) - OBJ += ../jsil/jsil$(LIBEXT) - CP_CXXFLAGS += -DHAVE_JSIL -endif - -############################################################################### - -goto-analyzer$(EXEEXT): $(OBJ) - $(LINKBIN) - -.PHONY: goto-analyzer-mac-signed - -goto-analyzer-mac-signed: goto-analyzer$(EXEEXT) - strip goto-analyzer$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) goto-analyzer$(EXEEXT) diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile deleted file mode 100644 index 8a70a3f6705..00000000000 --- a/src/goto-cc/Makefile +++ /dev/null @@ -1,73 +0,0 @@ -SRC = armcc_cmdline.cpp \ - armcc_mode.cpp \ - as86_cmdline.cpp \ - as_cmdline.cpp \ - as_mode.cpp \ - bcc_cmdline.cpp \ - cl_message_handler.cpp \ - compile.cpp \ - cw_mode.cpp \ - gcc_cmdline.cpp \ - gcc_message_handler.cpp \ - gcc_mode.cpp \ - goto_cc_cmdline.cpp \ - goto_cc_languages.cpp \ - goto_cc_main.cpp \ - goto_cc_mode.cpp \ - hybrid_binary.cpp \ - ld_cmdline.cpp \ - ld_mode.cpp \ - linker_script_merge.cpp \ - ms_cl_cmdline.cpp \ - ms_cl_mode.cpp \ - ms_cl_version.cpp \ - ms_link_cmdline.cpp \ - ms_link_mode.cpp \ - # Empty last line - -OBJ += ../big-int/big-int$(LIBEXT) \ - ../goto-programs/goto-programs$(LIBEXT) \ - ../util/util$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ - ../ansi-c/ansi-c$(LIBEXT) \ - ../cpp/cpp$(LIBEXT) \ - ../xmllang/xmllang$(LIBEXT) \ - ../assembler/assembler$(LIBEXT) \ - ../langapi/langapi$(LIBEXT) \ - ../json/json$(LIBEXT) - -INCLUDES= -I .. - -LIBS = - -CLEANFILES = goto-cc$(EXEEXT) goto-gcc$(EXEEXT) goto-cl$(EXEEXT) - -include ../config.inc -include ../common - -ifeq ($(BUILD_ENV_),MSVC) -all: goto-cl$(EXEEXT) -else -all: goto-gcc$(EXEEXT) -endif - -ifneq ($(wildcard ../jsil/Makefile),) - OBJ += ../jsil/jsil$(LIBEXT) - CP_CXXFLAGS += -DHAVE_JSIL -endif - -############################################################################### - -goto-gcc$(EXEEXT): goto-cc$(EXEEXT) - ln -sf goto-cc$(EXEEXT) goto-gcc$(EXEEXT) - -goto-cc$(EXEEXT): $(OBJ) - $(LINKBIN) - -goto-cl$(EXEEXT): $(OBJ) - $(LINKBIN) - -.PHONY: goto-cc-mac-signed - -goto-cc-mac-signed: goto-cc$(EXEEXT) - codesign -v -s $(OSX_IDENTITY) goto-cc$(EXEEXT) diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile deleted file mode 100644 index cb8243ecbc1..00000000000 --- a/src/goto-checker/Makefile +++ /dev/null @@ -1,34 +0,0 @@ -SRC = bmc_util.cpp \ - counterexample_beautification.cpp \ - cover_goals_report_util.cpp \ - incremental_goto_checker.cpp \ - goto_symex_fault_localizer.cpp \ - goto_symex_property_decider.cpp \ - goto_trace_storage.cpp \ - goto_verifier.cpp \ - multi_path_symex_checker.cpp \ - multi_path_symex_only_checker.cpp \ - properties.cpp \ - report_util.cpp \ - single_loop_incremental_symex_checker.cpp \ - single_path_symex_checker.cpp \ - single_path_symex_only_checker.cpp \ - solver_factory.cpp \ - symex_coverage.cpp \ - symex_bmc.cpp \ - symex_bmc_incremental_one_loop.cpp \ - # Empty last line - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = goto-checker$(LIBEXT) - -all: goto-checker$(LIBEXT) - -############################################################################### - -goto-checker$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile deleted file mode 100644 index 2b4ae9e9fea..00000000000 --- a/src/goto-diff/Makefile +++ /dev/null @@ -1,55 +0,0 @@ -SRC = change_impact.cpp \ - goto_diff_base.cpp \ - goto_diff_languages.cpp \ - goto_diff_main.cpp \ - goto_diff_parse_options.cpp \ - syntactic_diff.cpp \ - unified_diff.cpp \ - # Empty last line - -OBJ += ../ansi-c/ansi-c$(LIBEXT) \ - ../cpp/cpp$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ - ../big-int/big-int$(LIBEXT) \ - ../goto-programs/goto-programs$(LIBEXT) \ - ../assembler/assembler$(LIBEXT) \ - ../pointer-analysis/pointer-analysis$(LIBEXT) \ - ../goto-instrument/source_lines$(OBJEXT) \ - ../goto-instrument/cover$(OBJEXT) \ - ../goto-instrument/cover_basic_blocks$(OBJEXT) \ - ../goto-instrument/cover_filter$(OBJEXT) \ - ../goto-instrument/cover_instrument_branch$(OBJEXT) \ - ../goto-instrument/cover_instrument_condition$(OBJEXT) \ - ../goto-instrument/cover_instrument_decision$(OBJEXT) \ - ../goto-instrument/cover_instrument_location$(OBJEXT) \ - ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ - ../goto-instrument/cover_instrument_other$(OBJEXT) \ - ../goto-instrument/cover_util$(OBJEXT) \ - ../analyses/analyses$(LIBEXT) \ - ../langapi/langapi$(LIBEXT) \ - ../xmllang/xmllang$(LIBEXT) \ - ../util/util$(LIBEXT) \ - ../solvers/solvers$(LIBEXT) \ - ../json/json$(LIBEXT) \ - # Empty last line - -INCLUDES= -I .. - -LIBS = - -include ../config.inc -include ../common - -CLEANFILES = goto-diff$(EXEEXT) - -all: goto-diff$(EXEEXT) - -############################################################################### - -goto-diff$(EXEEXT): $(OBJ) - $(LINKBIN) - -.PHONY: goto-diff-mac-signed - -goto-diff-mac-signed: goto-diff$(EXEEXT) - strip goto-diff$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) goto-diff$(EXEEXT) diff --git a/src/goto-harness/Makefile b/src/goto-harness/Makefile deleted file mode 100644 index 83ba53039a8..00000000000 --- a/src/goto-harness/Makefile +++ /dev/null @@ -1,44 +0,0 @@ -SRC = \ - function_call_harness_generator.cpp \ - goto_harness_generator.cpp \ - goto_harness_generator_factory.cpp \ - goto_harness_main.cpp \ - goto_harness_parse_options.cpp \ - memory_snapshot_harness_generator.cpp \ - recursive_initialization.cpp \ - # Empty last line - -OBJ += \ - ../util/util$(LIBEXT) \ - ../goto-programs/goto-programs$(LIBEXT) \ - ../big-int/big-int$(LIBEXT) \ - ../langapi/langapi$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ - ../json/json$(LIBEXT) \ - ../json-symtab-language/json-symtab-language$(LIBEXT) \ - ../ansi-c/ansi-c$(LIBEXT) \ - ../cpp/cpp$(LIBEXT) \ - ../goto-instrument/dump_c$(OBJEXT) \ - ../goto-instrument/goto_program2code$(OBJEXT) \ - # Empty last line - -INCLUDES= -I .. - -LIBS = - -CLEANFILES = goto-harness$(EXEEXT) - -include ../config.inc -include ../common - -all: goto-harness$(EXEEXT) - -############################################################################### - -goto-harness$(EXEEXT): $(OBJ) - $(LINKBIN) - -.PHONY: goto-harness-mac-signed - -goto-harness-mac-signed: goto-harness$(EXEEXT) - codesign -v -s $(OSX_IDENTITY) goto-harness$(EXEEXT) diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile deleted file mode 100644 index 8cd5b3936b9..00000000000 --- a/src/goto-instrument/Makefile +++ /dev/null @@ -1,123 +0,0 @@ -SRC = accelerate/accelerate.cpp \ - accelerate/acceleration_utils.cpp \ - accelerate/all_paths_enumerator.cpp \ - accelerate/cone_of_influence.cpp \ - accelerate/disjunctive_polynomial_acceleration.cpp \ - accelerate/enumerating_loop_acceleration.cpp \ - accelerate/overflow_instrumenter.cpp \ - accelerate/path.cpp \ - accelerate/polynomial.cpp \ - accelerate/polynomial_accelerator.cpp \ - accelerate/sat_path_enumerator.cpp \ - accelerate/scratch_program.cpp \ - accelerate/trace_automaton.cpp \ - accelerate/util.cpp \ - aggressive_slicer.cpp \ - alignment_checks.cpp \ - branch.cpp \ - call_sequences.cpp \ - code_contracts.cpp \ - concurrency.cpp \ - count_eloc.cpp \ - cover.cpp \ - cover_basic_blocks.cpp \ - cover_filter.cpp \ - cover_instrument_branch.cpp \ - cover_instrument_condition.cpp \ - cover_instrument_decision.cpp \ - cover_instrument_location.cpp \ - cover_instrument_mcdc.cpp \ - cover_instrument_other.cpp \ - cover_util.cpp \ - document_properties.cpp \ - dot.cpp \ - dump_c.cpp \ - full_slicer.cpp \ - function.cpp \ - function_modifies.cpp \ - generate_function_bodies.cpp \ - goto_instrument_languages.cpp \ - goto_instrument_main.cpp \ - goto_instrument_parse_options.cpp \ - goto_program2code.cpp \ - havoc_loops.cpp \ - horn_encoding.cpp \ - insert_final_assert_false.cpp \ - interrupt.cpp \ - k_induction.cpp \ - loop_utils.cpp \ - mmio.cpp \ - model_argc_argv.cpp \ - nondet_static.cpp \ - nondet_volatile.cpp \ - object_id.cpp \ - points_to.cpp \ - race_check.cpp \ - reachability_slicer.cpp \ - remove_function.cpp \ - replace_calls.cpp \ - rw_set.cpp \ - show_locations.cpp \ - skip_loops.cpp \ - source_lines.cpp \ - splice_call.cpp \ - stack_depth.cpp \ - thread_instrumentation.cpp \ - undefined_functions.cpp \ - uninitialized.cpp \ - unwind.cpp \ - unwindset.cpp \ - value_set_fi_fp_removal.cpp \ - wmm/abstract_event.cpp \ - wmm/cycle_collection.cpp \ - wmm/data_dp.cpp \ - wmm/event_graph.cpp \ - wmm/fence.cpp \ - wmm/goto2graph.cpp \ - wmm/instrumenter_strategies.cpp \ - wmm/pair_collection.cpp \ - wmm/shared_buffers.cpp \ - wmm/weak_memory.cpp \ - # Empty last line - -OBJ += ../ansi-c/ansi-c$(LIBEXT) \ - ../cpp/cpp$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ - ../big-int/big-int$(LIBEXT) \ - ../goto-programs/goto-programs$(LIBEXT) \ - ../goto-symex/goto-symex$(LIBEXT) \ - ../assembler/assembler$(LIBEXT) \ - ../pointer-analysis/pointer-analysis$(LIBEXT) \ - ../analyses/analyses$(LIBEXT) \ - ../langapi/langapi$(LIBEXT) \ - ../xmllang/xmllang$(LIBEXT) \ - ../util/util$(LIBEXT) \ - ../solvers/solvers$(LIBEXT) \ - ../json/json$(LIBEXT) \ - # Empty last line - -INCLUDES= -I .. - -LIBS = - -CLEANFILES = goto-instrument$(EXEEXT) goto-instrument$(LIBEXT) - -include ../config.inc -include ../common - -all: goto-instrument$(EXEEXT) - -ifneq ($(LIB_GLPK),) - LIBS += $(LIB_GLPK) - CP_CXXFLAGS += -DHAVE_GLPK -endif - -############################################################################### - -goto-instrument$(EXEEXT): $(OBJ) - $(LINKBIN) - -.PHONY: goto-instrument-mac-signed - -goto-instrument-mac-signed: goto-instrument$(EXEEXT) - codesign -v -s $(OSX_IDENTITY) goto-instrument$(EXEEXT) diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile deleted file mode 100644 index 18a9129e7be..00000000000 --- a/src/goto-programs/Makefile +++ /dev/null @@ -1,90 +0,0 @@ -SRC = add_malloc_may_fail_variable_initializations.cpp \ - adjust_float_expressions.cpp \ - builtin_functions.cpp \ - class_hierarchy.cpp \ - class_identifier.cpp \ - compute_called_functions.cpp \ - destructor.cpp \ - destructor_tree.cpp \ - elf_reader.cpp \ - ensure_one_backedge_per_target.cpp \ - format_strings.cpp \ - goto_asm.cpp \ - goto_clean_expr.cpp \ - goto_convert.cpp \ - goto_convert_exceptions.cpp \ - goto_convert_function_call.cpp \ - goto_convert_functions.cpp \ - goto_convert_side_effect.cpp \ - goto_function.cpp \ - goto_functions.cpp \ - goto_inline_class.cpp \ - goto_inline.cpp \ - goto_program.cpp \ - goto_trace.cpp \ - graphml_witness.cpp \ - initialize_goto_model.cpp \ - instrument_preconditions.cpp \ - interpreter.cpp \ - interpreter_evaluate.cpp \ - json_expr.cpp \ - json_goto_trace.cpp \ - label_function_pointer_call_sites.cpp \ - link_goto_model.cpp \ - link_to_library.cpp \ - loop_ids.cpp \ - mm_io.cpp \ - name_mangler.cpp \ - osx_fat_reader.cpp \ - parameter_assignments.cpp \ - pointer_arithmetic.cpp \ - printf_formatter.cpp \ - read_bin_goto_object.cpp \ - read_goto_binary.cpp \ - rebuild_goto_start_function.cpp \ - remove_calls_no_body.cpp \ - remove_complex.cpp \ - remove_const_function_pointers.cpp \ - remove_function_pointers.cpp \ - remove_returns.cpp \ - remove_skip.cpp \ - remove_unreachable.cpp \ - remove_unused_functions.cpp \ - remove_vector.cpp \ - remove_virtual_functions.cpp \ - restrict_function_pointers.cpp \ - rewrite_union.cpp \ - resolve_inherited_component.cpp \ - safety_checker.cpp \ - set_properties.cpp \ - show_goto_functions.cpp \ - show_goto_functions_json.cpp \ - show_goto_functions_xml.cpp \ - show_properties.cpp \ - show_symbol_table.cpp \ - slice_global_inits.cpp \ - string_abstraction.cpp \ - string_instrumentation.cpp \ - structured_trace_util.cpp \ - system_library_symbols.cpp \ - validate_goto_model.cpp \ - vcd_goto_trace.cpp \ - wp.cpp \ - write_goto_binary.cpp \ - xml_expr.cpp \ - xml_goto_trace.cpp \ - # Empty last line - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = goto-programs$(LIBEXT) - -all: goto-programs$(LIBEXT) - -############################################################################### - -goto-programs$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile deleted file mode 100644 index d9670e644bd..00000000000 --- a/src/goto-symex/Makefile +++ /dev/null @@ -1,53 +0,0 @@ -SRC = auto_objects.cpp \ - build_goto_trace.cpp \ - expr_skeleton.cpp \ - field_sensitivity.cpp \ - goto_state.cpp \ - goto_symex.cpp \ - goto_symex_state.cpp \ - memory_model.cpp \ - memory_model_pso.cpp \ - memory_model_sc.cpp \ - memory_model_tso.cpp \ - partial_order_concurrency.cpp \ - path_storage.cpp \ - postcondition.cpp \ - precondition.cpp \ - renaming_level.cpp \ - show_program.cpp \ - show_vcc.cpp \ - slice.cpp \ - ssa_step.cpp \ - symex_assign.cpp \ - symex_atomic_section.cpp \ - symex_builtin_functions.cpp \ - symex_catch.cpp \ - symex_clean_expr.cpp \ - symex_dead.cpp \ - symex_decl.cpp \ - symex_dereference.cpp \ - symex_dereference_state.cpp \ - symex_function_call.cpp \ - symex_goto.cpp \ - symex_main.cpp \ - symex_other.cpp \ - symex_start_thread.cpp \ - symex_target.cpp \ - symex_target_equation.cpp \ - symex_throw.cpp \ - complexity_limiter.cpp \ - # Empty last line - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = goto-symex$(LIBEXT) - -all: goto-symex$(LIBEXT) - -############################################################################### - -goto-symex$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/jsil/Makefile b/src/jsil/Makefile deleted file mode 100644 index 3a1e01a6a1c..00000000000 --- a/src/jsil/Makefile +++ /dev/null @@ -1,42 +0,0 @@ -SRC = expr2jsil.cpp \ - jsil_convert.cpp \ - jsil_entry_point.cpp \ - jsil_internal_additions.cpp \ - jsil_language.cpp \ - jsil_lex.yy.cpp \ - jsil_parse_tree.cpp \ - jsil_parser.cpp \ - jsil_typecheck.cpp \ - jsil_types.cpp \ - jsil_y.tab.cpp \ - # Empty last line - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = jsil$(LIBEXT) \ - jsil_y.tab.h jsil_y.tab.cpp jsil_lex.yy.cpp \ - jsil_y.tab.cpp.output jsil_y.output - -all: jsil$(LIBEXT) - -############################################################################### - -jsil$(LIBEXT): $(OBJ) - $(LINKLIB) - -jsil_y.tab.cpp: parser.y - $(YACC) $(YFLAGS) $$flags -pyyjsil parser.y --defines=jsil_y.tab.h -o $@ - -jsil_y.tab.h: jsil_y.tab.cpp - -jsil_lex.yy.cpp: scanner.l - $(LEX) -Pyyjsil -o$@ scanner.l - -generated_files: jsil_lex.yy.cpp jsil_y.tab.cpp jsil_y.tab.h - -# extra dependencies -jsil_y.tab$(OBJEXT): jsil_y.tab.cpp jsil_y.tab.h -jsil_lex.yy$(OBJEXT): jsil_y.tab.cpp jsil_lex.yy.cpp jsil_y.tab.h diff --git a/src/json-symtab-language/Makefile b/src/json-symtab-language/Makefile deleted file mode 100644 index 3fb674732cf..00000000000 --- a/src/json-symtab-language/Makefile +++ /dev/null @@ -1,17 +0,0 @@ -SRC = json_symtab_language.cpp \ - json_symbol_table.cpp \ - json_symbol.cpp - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = json-symtab-language$(LIBEXT) - -all: json-symtab-language$(LIBEXT) - -############################################################################### - -json-symtab-language$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/json/Makefile b/src/json/Makefile deleted file mode 100644 index 8c5d345a25e..00000000000 --- a/src/json/Makefile +++ /dev/null @@ -1,33 +0,0 @@ -SRC = json_interface.cpp \ - json_lex.yy.cpp \ - json_parser.cpp \ - json_y.tab.cpp \ - # Empty last line -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES=json$(LIBEXT) json_y.tab.h json_y.tab.cpp json_lex.yy.cpp \ - json_y.tab.cpp.output json_y.output - -all: json$(LIBEXT) - -############################################################################### - -json$(LIBEXT): $(OBJ) - $(LINKLIB) - -json_y.tab.cpp: parser.y - $(YACC) $(YFLAGS) $$flags -pyyjson parser.y --defines=json_y.tab.h -o $@ - -json_y.tab.h: json_y.tab.cpp - -json_lex.yy.cpp: scanner.l - $(LEX) -Pyyjson -o$@ scanner.l - -generated_files: json_lex.yy.cpp json_y.tab.cpp json_y.tab.h - -# extra dependencies -json_y.tab$(OBJEXT): json_y.tab.cpp json_y.tab.h -json_lex.yy$(OBJEXT): json_y.tab.cpp json_lex.yy.cpp json_y.tab.h diff --git a/src/langapi/Makefile b/src/langapi/Makefile deleted file mode 100644 index 290d2023638..00000000000 --- a/src/langapi/Makefile +++ /dev/null @@ -1,18 +0,0 @@ -SRC = language_util.cpp \ - language_file.cpp \ - language.cpp \ - mode.cpp \ - # Empty last line -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = langapi$(LIBEXT) - -all: langapi$(LIBEXT) - -############################################################################### - -langapi$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/linking/Makefile b/src/linking/Makefile deleted file mode 100644 index f1a52517dae..00000000000 --- a/src/linking/Makefile +++ /dev/null @@ -1,18 +0,0 @@ -SRC = linking.cpp \ - remove_internal_symbols.cpp \ - static_lifetime_init.cpp \ - # Empty last line - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = linking$(LIBEXT) - -all: linking$(LIBEXT) - -############################################################################### - -linking$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/memory-analyzer/Makefile b/src/memory-analyzer/Makefile deleted file mode 100644 index 41bb6c4d414..00000000000 --- a/src/memory-analyzer/Makefile +++ /dev/null @@ -1,38 +0,0 @@ -SRC = \ - analyze_symbol.cpp \ - gdb_api.cpp \ - memory_analyzer_main.cpp \ - memory_analyzer_parse_options.cpp - # Empty last line - -INCLUDES= -I .. - -OBJ += \ - ../ansi-c/ansi-c$(LIBEXT) \ - ../goto-programs/goto-programs$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ - ../util/util$(LIBEXT) \ - ../big-int/big-int$(LIBEXT) \ - ../langapi/langapi$(LIBEXT) - -LIBS = - -CLEANFILES = memory-analyzer$(EXEEXT) - -include ../config.inc -include ../common - -all: memory-analyzer$(EXEEXT) - - - -############################################################################### - -memory-analyzer$(EXEEXT): $(OBJ) - $(LINKBIN) - - -.PHONY: memory-analyser-mac-signed - -memory-analyser-mac-signed: memory-analyzer$(EXEEXT) - codesign -v -s $(OSX_IDENTITY) memory-analyzer$(EXEEXT) diff --git a/src/pointer-analysis/Makefile b/src/pointer-analysis/Makefile deleted file mode 100644 index 61e59313ea3..00000000000 --- a/src/pointer-analysis/Makefile +++ /dev/null @@ -1,25 +0,0 @@ -SRC = add_failed_symbols.cpp \ - goto_program_dereference.cpp \ - rewrite_index.cpp \ - show_value_sets.cpp \ - value_set.cpp \ - value_set_analysis.cpp \ - value_set_analysis_fi.cpp \ - value_set_dereference.cpp \ - value_set_domain_fi.cpp \ - value_set_fi.cpp \ - # Empty last line - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = pointer-analysis$(LIBEXT) - -all: pointer-analysis$(LIBEXT) - -############################################################################### - -pointer-analysis$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/solvers/Makefile b/src/solvers/Makefile deleted file mode 100644 index ec9ddfceb18..00000000000 --- a/src/solvers/Makefile +++ /dev/null @@ -1,264 +0,0 @@ -include ../config.inc - -ifneq ($(CHAFF),) - CHAFF_SRC=sat/satcheck_zchaff.cpp sat/satcheck_zcore.cpp - CHAFF_INCLUDE=-I $(CHAFF) - CHAFF_LIB=$(CHAFF)/libsat$(LIBEXT) -endif - -ifneq ($(MINISAT),) - MINISAT_SRC=sat/satcheck_minisat.cpp - MINISAT_INCLUDE=-I $(MINISAT) - MINISAT_LIB=$(MINISAT)/Solver$(OBJEXT) $(MINISAT)/Proof$(OBJEXT) $(MINISAT)/File$(OBJEXT) - CP_CXXFLAGS += -DHAVE_MINISAT - CLEANFILES += $(MINISAT_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(MINISAT_LIB)) -endif - -ifneq ($(MINISAT2),) - MINISAT2_SRC=sat/satcheck_minisat2.cpp - MINISAT2_INCLUDE=-I $(MINISAT2) - MINISAT2_LIB=$(MINISAT2)/minisat/simp/SimpSolver$(OBJEXT) $(MINISAT2)/minisat/core/Solver$(OBJEXT) - CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS - CLEANFILES += $(MINISAT2_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(MINISAT2_LIB)) -endif - -ifneq ($(IPASIR),) - IPASIR_SRC=sat/satcheck_ipasir.cpp - IPASIR_INCLUDE=-I $(IPASIR) - CP_CXXFLAGS += -DHAVE_IPASIR -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS - override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS)) -endif - -ifneq ($(GLUCOSE),) - GLUCOSE_SRC=sat/satcheck_glucose.cpp - GLUCOSE_INCLUDE=-I $(GLUCOSE) - GLUCOSE_LIB=$(GLUCOSE)/simp/SimpSolver$(OBJEXT) $(GLUCOSE)/core/Solver$(OBJEXT) - CP_CXXFLAGS += -DHAVE_GLUCOSE -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS - CLEANFILES += $(GLUCOSE_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(GLUCOSE_LIB)) -endif - -ifneq ($(SQUOLEM2),) - SQUOLEM2_SRC=qbf/qbf_squolem.cpp qbf/qbf_squolem_core.cpp - SQUOLEM2_INCLUDE=-I $(SQUOLEM2) - SQUOLEM2_LIB=-L $(SQUOLEM2) -lsquolem2 -endif - -ifneq ($(CUDD),) - CUDD_LIB=$(CUDD)/cudd/.libs/libcudd$(LIBEXT) $(CUDD)/cplusplus/.libs/libobj$(LIBEXT) -endif - -ifneq ($(PICOSAT),) - PICOSAT_SRC=sat/satcheck_picosat.cpp - PICOSAT_INCLUDE=-I $(PICOSAT) - PICOSAT_LIB=$(PICOSAT)/libpicosat$(LIBEXT) - CP_CXXFLAGS += -DHAVE_PICOSAT -endif - -ifneq ($(LINGELING),) - LINGELING_SRC=sat/satcheck_lingeling.cpp - LINGELING_INCLUDE=-I $(LINGELING) - LINGELING_LIB=$(LINGELING)/liblgl$(LIBEXT) - CP_CXXFLAGS += -DHAVE_LINGELING -endif - -ifneq ($(CADICAL),) - CADICAL_SRC=sat/satcheck_cadical.cpp - CADICAL_INCLUDE=-I $(CADICAL)/src - CADICAL_LIB=$(CADICAL)/build/libcadical$(LIBEXT) - CP_CXXFLAGS += -DHAVE_CADICAL -endif - -SRC = $(BOOLEFORCE_SRC) \ - $(CHAFF_SRC) \ - $(CUDD_SRC) \ - $(GLUCOSE_SRC) \ - $(LINGELING_SRC) \ - $(MINISAT2_SRC) \ - $(IPASIR_SRC) \ - $(MINISAT_SRC) \ - $(PICOSAT_SRC) \ - $(SQUOLEM2_SRC) \ - $(CADICAL_SRC) \ - decision_procedure.cpp \ - solver_hardness.cpp \ - flattening/arrays.cpp \ - flattening/boolbv.cpp \ - flattening/boolbv_abs.cpp \ - flattening/boolbv_add_sub.cpp \ - flattening/boolbv_array.cpp \ - flattening/boolbv_array_of.cpp \ - flattening/boolbv_bitwise.cpp \ - flattening/boolbv_bswap.cpp \ - flattening/boolbv_bv_rel.cpp \ - flattening/boolbv_byte_extract.cpp \ - flattening/boolbv_byte_update.cpp \ - flattening/boolbv_case.cpp \ - flattening/boolbv_complex.cpp \ - flattening/boolbv_concatenation.cpp \ - flattening/boolbv_cond.cpp \ - flattening/boolbv_constant.cpp \ - flattening/boolbv_constraint_select_one.cpp \ - flattening/boolbv_div.cpp \ - flattening/boolbv_equality.cpp \ - flattening/boolbv_extractbit.cpp \ - flattening/boolbv_extractbits.cpp \ - flattening/boolbv_floatbv_op.cpp \ - flattening/boolbv_get.cpp \ - flattening/boolbv_ieee_float_rel.cpp \ - flattening/boolbv_if.cpp \ - flattening/boolbv_index.cpp \ - flattening/boolbv_let.cpp \ - flattening/boolbv_map.cpp \ - flattening/boolbv_member.cpp \ - flattening/boolbv_mod.cpp \ - flattening/boolbv_mult.cpp \ - flattening/boolbv_not.cpp \ - flattening/boolbv_onehot.cpp \ - flattening/boolbv_overflow.cpp \ - flattening/boolbv_power.cpp \ - flattening/boolbv_quantifier.cpp \ - flattening/boolbv_reduction.cpp \ - flattening/boolbv_replication.cpp \ - flattening/boolbv_shift.cpp \ - flattening/boolbv_struct.cpp \ - flattening/boolbv_type.cpp \ - flattening/boolbv_typecast.cpp \ - flattening/boolbv_unary_minus.cpp \ - flattening/boolbv_union.cpp \ - flattening/boolbv_update.cpp \ - flattening/boolbv_vector.cpp \ - flattening/boolbv_width.cpp \ - flattening/boolbv_with.cpp \ - flattening/bv_dimacs.cpp \ - flattening/bv_endianness_map.cpp \ - flattening/bv_minimize.cpp \ - flattening/bv_pointers.cpp \ - flattening/bv_utils.cpp \ - flattening/c_bit_field_replacement_type.cpp \ - flattening/equality.cpp \ - flattening/pointer_logic.cpp \ - floatbv/float_bv.cpp \ - floatbv/float_utils.cpp \ - floatbv/float_approximation.cpp \ - lowering/byte_operators.cpp \ - lowering/functions.cpp \ - lowering/popcount.cpp \ - bdd/miniBDD/miniBDD.cpp \ - prop/bdd_expr.cpp \ - prop/cover_goals.cpp \ - prop/literal.cpp \ - prop/prop_minimize.cpp \ - prop/prop.cpp \ - prop/prop_conv.cpp \ - prop/prop_conv_solver.cpp \ - qbf/qbf_quantor.cpp \ - qbf/qbf_qube.cpp \ - qbf/qbf_qube_core.cpp \ - qbf/qbf_skizzo.cpp \ - qbf/qdimacs_cnf.cpp \ - qbf/qdimacs_core.cpp \ - refinement/bv_refinement_loop.cpp \ - refinement/refine_arithmetic.cpp \ - refinement/refine_arrays.cpp \ - strings/array_pool.cpp \ - strings/equation_symbol_mapping.cpp \ - strings/format_specifier.cpp \ - strings/string_builtin_function.cpp \ - strings/string_dependencies.cpp \ - strings/string_concatenation_builtin_function.cpp \ - strings/string_format_builtin_function.cpp \ - strings/string_insertion_builtin_function.cpp \ - strings/string_refinement.cpp \ - strings/string_refinement_util.cpp \ - strings/string_constraint.cpp \ - strings/string_constraint_generator_code_points.cpp \ - strings/string_constraint_generator_comparison.cpp \ - strings/string_constraint_generator_constants.cpp \ - strings/string_constraint_generator_indexof.cpp \ - strings/string_constraint_generator_float.cpp \ - strings/string_constraint_generator_main.cpp \ - strings/string_constraint_generator_testing.cpp \ - strings/string_constraint_generator_transformation.cpp \ - strings/string_constraint_generator_valueof.cpp \ - strings/string_constraint_instantiation.cpp \ - sat/cnf.cpp \ - sat/cnf_clause_list.cpp \ - sat/dimacs_cnf.cpp \ - sat/external_sat.cpp \ - sat/pbs_dimacs_cnf.cpp \ - sat/resolution_proof.cpp \ - smt2/letify.cpp \ - smt2/smt2_conv.cpp \ - smt2/smt2_dec.cpp \ - smt2/smt2_format.cpp \ - smt2/smt2_parser.cpp \ - smt2/smt2_tokenizer.cpp \ - smt2/smt2irep.cpp \ - # Empty last line - -include ../common - -ifneq ($(MINISAT2),) -ifeq ($(BUILD_ENV_),MSVC) -sat/satcheck_minisat2$(OBJEXT): sat/satcheck_minisat2.cpp - $(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@ - -$(MINISAT2)/minisat/simp/SimpSolver$(OBJEXT): $(MINISAT2)/minisat/simp/SimpSolver.cc - $(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@ - -$(MINISAT2)/minisat/core/Solver$(OBJEXT): $(MINISAT2)/minisat/core/Solver.cc - $(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@ -endif -endif - -ifneq ($(GLUCOSE),) -ifeq ($(BUILD_ENV_),MSVC) -sat/satcheck_glucose$(OBJEXT): sat/satcheck_glucose.cpp - $(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@ - -$(GLUCOSE)/simp/SimpSolver$(OBJEXT): $(GLUCOSE)/simp/SimpSolver.cc - $(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@ - -$(GLUCOSE)/core/Solver$(OBJEXT): $(GLUCOSE)/core/Solver.cc - $(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@ -endif -endif - -INCLUDES += -I .. \ - $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \ - $(IPASIR_INCLUDE) \ - $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \ - $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE) $(CADICAL_INCLUDE) - -CLEANFILES += solvers$(LIBEXT) \ - smt2_solver$(EXEEXT) smt2/smt2_solver$(OBJEXT) smt2/smt2_solver$(DEPEXT) - -all: solvers$(LIBEXT) smt2_solver$(EXEEXT) - -ifneq ($(SQUOLEM2),) - CP_CXXFLAGS += -DHAVE_QBF_CORE -else -ifneq ($(CUDD),) - CP_CXXFLAGS += -DHAVE_QBF_CORE -endif -endif - -SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \ - $(MINISAT2_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \ - $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB) $(CADICAL_LIB) - -SOLVER_OBJS = $(filter %$(OBJEXT), $(SOLVER_LIB)) -ifneq ($(SOLVER_OBJS),) --include $(SOLVER_OBJS:$(OBJEXT)=$(DEPEXT)) -endif - -############################################################################### - -solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB) - $(LINKLIB) - --include smt2/smt2_solver$(DEPEXT) - -smt2_solver$(EXEEXT): $(OBJ) smt2/smt2_solver$(OBJEXT) \ - ../util/util$(LIBEXT) ../big-int/big-int$(LIBEXT) $(SOLVER_LIB) - $(LINKBIN) diff --git a/src/solvers/bdd/miniBDD/Makefile b/src/solvers/bdd/miniBDD/Makefile deleted file mode 100644 index 55b6a0ed86c..00000000000 --- a/src/solvers/bdd/miniBDD/Makefile +++ /dev/null @@ -1,23 +0,0 @@ - -CPLUSFLAGS = -g - -all: miniBDD.o test_miniBDD - -miniBDD.h: -miniBDD.cpp: - -miniBDD.o: miniBDD.cpp miniBDD.inc miniBDD.h - g++ $(CPLUSFLAGS) -c miniBDD.cpp -o miniBDD.o - -test_miniBDD.o: miniBDD.inc miniBDD.h test_miniBDD.cpp - g++ $(CPLUSFLAGS) -c test_miniBDD.cpp -o test_miniBDD.o - -test_miniBDD: miniBDD.o test_miniBDD.o - g++ $(CPLUSFLAGS) miniBDD.o test_miniBDD.o -o test_miniBDD - -clean: - $(RM) miniBDD.o test_miniBDD.o test_miniBDD - -miniBDD.tgz: miniBDD.cpp miniBDD.inc miniBDD.h test_miniBDD.cpp Makefile - tar cvfz miniBDD.tgz miniBDD.cpp miniBDD.inc \ - miniBDD.h test_miniBDD.cpp Makefile diff --git a/src/statement-list/Makefile b/src/statement-list/Makefile deleted file mode 100644 index 3b42f0c3030..00000000000 --- a/src/statement-list/Makefile +++ /dev/null @@ -1,55 +0,0 @@ -SRC = converters/convert_bool_literal.cpp \ - converters/convert_dint_literal.cpp \ - converters/convert_int_literal.cpp \ - converters/convert_real_literal.cpp \ - converters/convert_string_value.cpp \ - converters/expr2statement_list.cpp \ - converters/statement_list_types.cpp \ - statement_list_entry_point.cpp \ - statement_list_language.cpp \ - statement_list_lex.yy.cpp \ - statement_list_parse_tree.cpp \ - statement_list_parse_tree_io.cpp \ - statement_list_parser.cpp \ - statement_list_typecheck.cpp \ - statement_list_y.tab.cpp \ - # Empty last line - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = statement-list$(LIBEXT) \ - statement_list_y.tab.h statement_list_y.tab.cpp \ - statement_list_lex.yy.cpp statement_list_y.tab.cpp.output \ - statement_list_y.output - -all: statement-list$(LIBEXT) - -############################################################################### - -statement_list_y.tab.cpp: parser.y - $(YACC) $(YFLAGS) $$flags -pyystatement_list parser.y --defines=statement_list_y.tab.h -o $@ - -statement_list_y.tab.h: statement_list_y.tab.cpp - -statement_list_lex.yy.cpp: scanner.l - $(LEX) -Pyystatement_list -o$@ scanner.l - -# extra dependencies -statement_list_y.tab$(OBJEXT): statement_list_y.tab.cpp \ - statement_list_y.tab.h -statement_list_lex.yy$(OBJEXT): statement_list_y.tab.cpp \ - statement_list_lex.yy.cpp statement_list_y.tab.h - -############################################################################### - -generated_files: statement_list_y.tab.cpp statement_list_lex.yy.cpp \ - statement_list_y.tab.h - -############################################################################### - -statement-list$(LIBEXT): $(OBJ) - $(LINKLIB) - diff --git a/src/symtab2gb/Makefile b/src/symtab2gb/Makefile deleted file mode 100644 index dd18aaa51c0..00000000000 --- a/src/symtab2gb/Makefile +++ /dev/null @@ -1,35 +0,0 @@ -SRC = \ - symtab2gb_main.cpp \ - symtab2gb_parse_options.cpp \ - # Empty last line - -OBJ += \ - ../util/util$(LIBEXT) \ - ../goto-programs/goto-programs$(LIBEXT) \ - ../big-int/big-int$(LIBEXT) \ - ../langapi/langapi$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ - ../json/json$(LIBEXT) \ - ../json-symtab-language/json-symtab-language$(LIBEXT) \ - # Empty last line - -INCLUDES= -I .. - -LIBS = - -CLEANFILES = symtab2gb$(EXEEXT) - -include ../config.inc -include ../common - -all: symtab2gb$(EXEEXT) - -############################################################################### - -symtab2gb$(EXEEXT): $(OBJ) - $(LINKBIN) - -.PHONY: symtab2gb-mac-signed - -symtab2gb-mac-signed: symtab2gb$(EXEEXT) - codesign -v -s $(OSX_IDENTITY) symtab2gb2$(EXEEXT) diff --git a/src/util/Makefile b/src/util/Makefile deleted file mode 100644 index 8e800b92ded..00000000000 --- a/src/util/Makefile +++ /dev/null @@ -1,141 +0,0 @@ -SRC = allocate_objects.cpp \ - arith_tools.cpp \ - array_element_from_pointer.cpp \ - array_name.cpp \ - base_type.cpp \ - bv_arithmetic.cpp \ - byte_operators.cpp \ - c_types.cpp \ - cmdline.cpp \ - config.cpp \ - cout_message.cpp \ - dstring.cpp \ - endianness_map.cpp \ - edit_distance.cpp \ - expr.cpp \ - expr_initializer.cpp \ - expr_util.cpp \ - exception_utils.cpp \ - file_util.cpp \ - find_macros.cpp \ - find_symbols.cpp \ - fixedbv.cpp \ - format_constant.cpp \ - format_expr.cpp \ - format_number_range.cpp \ - format_type.cpp \ - fresh_symbol.cpp \ - get_base_name.cpp \ - get_module.cpp \ - identifier.cpp \ - ieee_float.cpp \ - interval_union.cpp \ - invariant.cpp \ - irep.cpp \ - irep_hash.cpp \ - irep_hash_container.cpp \ - irep_ids.cpp \ - irep_serialization.cpp \ - interval_constraint.cpp \ - invariant_utils.cpp \ - json.cpp \ - json_irep.cpp \ - json_stream.cpp \ - lispexpr.cpp \ - lispirep.cpp \ - mathematical_expr.cpp \ - mathematical_types.cpp \ - memory_info.cpp \ - merge_irep.cpp \ - message.cpp \ - mp_arith.cpp \ - namespace.cpp \ - nondet.cpp \ - object_factory_parameters.cpp \ - options.cpp \ - parse_options.cpp \ - parser.cpp \ - pointer_offset_size.cpp \ - pointer_offset_sum.cpp \ - pointer_predicates.cpp \ - prefix_filter.cpp \ - rational.cpp \ - rational_tools.cpp \ - ref_expr_set.cpp \ - refined_string_type.cpp \ - rename.cpp \ - rename_symbol.cpp \ - replace_expr.cpp \ - replace_symbol.cpp \ - run.cpp \ - signal_catcher.cpp \ - simplify_expr.cpp \ - simplify_expr_array.cpp \ - simplify_expr_boolean.cpp \ - simplify_expr_floatbv.cpp \ - simplify_expr_if.cpp \ - simplify_expr_int.cpp \ - simplify_expr_pointer.cpp \ - simplify_expr_struct.cpp \ - simplify_utils.cpp \ - source_location.cpp \ - ssa_expr.cpp \ - std_code.cpp \ - std_expr.cpp \ - std_types.cpp \ - string2int.cpp \ - string_constant.cpp \ - string_container.cpp \ - string_hash.cpp \ - string_utils.cpp \ - structured_data.cpp \ - symbol.cpp \ - symbol_table_base.cpp \ - symbol_table.cpp \ - tempdir.cpp \ - tempfile.cpp \ - threeval.cpp \ - timestamper.cpp \ - type.cpp \ - typecheck.cpp \ - ui_message.cpp \ - unicode.cpp \ - union_find.cpp \ - union_find_replace.cpp \ - validate_code.cpp \ - validate_expressions.cpp \ - validate_types.cpp \ - version.cpp \ - xml.cpp \ - xml_irep.cpp \ - interval.cpp \ - # Empty last line - -INCLUDES= -I .. - -include ../config.inc -include ../common - -# get version from git -GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a") -RELEASE_INFO = const char *CBMC_VERSION="$(CBMC_VERSION) ($(GIT_INFO))"; -GIT_INFO_FILE = version.cpp - -$(GIT_INFO_FILE): - echo '$(RELEASE_INFO)' > $@ - -generated_files: $(GIT_INFO_FILE) - -# mark the actually generated file as a phony target to enforce a rebuild - but -# only if the version information has changed! -KNOWN_RELEASE_INFO = $(shell cat $(GIT_INFO_FILE) 2>/dev/null) -ifneq ($(RELEASE_INFO), $(KNOWN_RELEASE_INFO)) -.PHONY: $(GIT_INFO_FILE) -endif - -CLEANFILES = $(GIT_INFO_FILE) util$(LIBEXT) - -all: util$(LIBEXT) $(GIT_INFO_FILE) - -util$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/xmllang/Makefile b/src/xmllang/Makefile deleted file mode 100644 index ecd4eca6103..00000000000 --- a/src/xmllang/Makefile +++ /dev/null @@ -1,35 +0,0 @@ -SRC = graphml.cpp \ - xml_interface.cpp \ - xml_lex.yy.cpp \ - xml_parse_tree.cpp \ - xml_parser.cpp \ - xml_y.tab.cpp \ - # Empty last line -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES=xmllang$(LIBEXT) xml_y.tab.h xml_y.tab.cpp xml_lex.yy.cpp \ - xml_y.tab.cpp.output xml_y.output - -all: xmllang$(LIBEXT) - -############################################################################### - -xmllang$(LIBEXT): $(OBJ) - $(LINKLIB) - -xml_y.tab.cpp: parser.y - $(YACC) $(YFLAGS) $$flags -pyyxml parser.y --defines=xml_y.tab.h -o $@ - -xml_y.tab.h: xml_y.tab.cpp - -xml_lex.yy.cpp: scanner.l - $(LEX) -Pyyxml -o$@ scanner.l - -generated_files: xml_lex.yy.cpp xml_y.tab.cpp xml_y.tab.h - -# extra dependencies -xml_y.tab$(OBJEXT): xml_y.tab.cpp xml_y.tab.h -xml_lex.yy$(OBJEXT): xml_y.tab.cpp xml_lex.yy.cpp xml_y.tab.h diff --git a/unit/Makefile b/unit/Makefile deleted file mode 100644 index 75fb0e52368..00000000000 --- a/unit/Makefile +++ /dev/null @@ -1,243 +0,0 @@ -.PHONY: all cprover.dir test testing-utils-clean - -# Source files for test utilities -SRC = unit_tests.cpp \ - # Empty last line - -# Test source files -SRC += analyses/ai/ai.cpp \ - analyses/ai/ai_simplify_lhs.cpp \ - analyses/call_graph.cpp \ - analyses/constant_propagator.cpp \ - analyses/dependence_graph.cpp \ - analyses/disconnect_unreachable_nodes_in_graph.cpp \ - analyses/does_remove_const/does_expr_lose_const.cpp \ - analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ - analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ - ansi-c/max_malloc_size.cpp \ - ansi-c/type2name.cpp \ - big-int/big-int.cpp \ - compound_block_locations.cpp \ - get_goto_model_from_c_test.cpp \ - goto-cc/armcc_cmdline.cpp \ - goto-checker/report_util/is_property_less_than.cpp \ - goto-instrument/cover_instrument.cpp \ - goto-instrument/cover/cover_only.cpp \ - goto-programs/goto_model_function_type_consistency.cpp \ - goto-programs/goto_program_assume.cpp \ - goto-programs/goto_program_dead.cpp \ - goto-programs/goto_program_declaration.cpp \ - goto-programs/goto_program_function_call.cpp \ - goto-programs/goto_program_goto_target.cpp \ - goto-programs/goto_program_symbol_type_table_consistency.cpp \ - goto-programs/goto_program_table_consistency.cpp \ - goto-programs/goto_program_validate.cpp \ - goto-programs/goto_trace_output.cpp \ - goto-programs/is_goto_binary.cpp \ - goto-programs/label_function_pointer_call_sites.cpp \ - goto-programs/osx_fat_reader.cpp \ - goto-programs/restrict_function_pointers.cpp \ - goto-programs/structured_trace_util.cpp \ - goto-programs/remove_returns.cpp \ - goto-programs/xml_expr.cpp \ - goto-symex/apply_condition.cpp \ - goto-symex/expr_skeleton.cpp \ - goto-symex/goto_symex_state.cpp \ - goto-symex/ssa_equation.cpp \ - goto-symex/is_constant.cpp \ - goto-symex/symex_assign.cpp \ - goto-symex/symex_level0.cpp \ - goto-symex/symex_level1.cpp \ - goto-symex/try_evaluate_pointer_comparisons.cpp \ - interpreter/interpreter.cpp \ - json/json_parser.cpp \ - json_symbol_table.cpp \ - path_strategies.cpp \ - pointer-analysis/value_set.cpp \ - solvers/bdd/miniBDD/miniBDD.cpp \ - solvers/floatbv/float_utils.cpp \ - solvers/lowering/byte_operators.cpp \ - solvers/prop/bdd_expr.cpp \ - solvers/sat/external_sat.cpp \ - solvers/sat/satcheck_minisat2.cpp \ - solvers/strings/array_pool/array_pool.cpp \ - solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \ - solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \ - solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp \ - solvers/strings/string_format_builtin_function/length_for_format_specifier.cpp \ - solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp \ - solvers/strings/string_refinement/concretize_array.cpp \ - solvers/strings/string_refinement/sparse_array.cpp \ - solvers/strings/string_refinement/string_refinement.cpp \ - solvers/strings/string_refinement/substitute_array_list.cpp \ - solvers/strings/string_refinement/union_find_replace.cpp \ - util/allocate_objects.cpp \ - util/cmdline.cpp \ - util/dense_integer_map.cpp \ - util/edit_distance.cpp \ - util/expr_cast/expr_cast.cpp \ - util/expr.cpp \ - util/expr_iterator.cpp \ - util/file_util.cpp \ - util/format_number_range.cpp \ - util/get_base_name.cpp \ - util/graph.cpp \ - util/interval/add.cpp \ - util/interval/bitwise.cpp \ - util/interval/comparisons.cpp \ - util/interval/divide.cpp \ - util/interval/eval.cpp \ - util/interval/get_extreme.cpp \ - util/interval/modulo.cpp \ - util/interval/multiply.cpp \ - util/interval/shift.cpp \ - util/interval/subtract.cpp \ - util/interval/to_string.cpp \ - util/interval_constraint.cpp \ - util/interval_union.cpp \ - util/irep.cpp \ - util/irep_sharing.cpp \ - util/json_array.cpp \ - util/json_object.cpp \ - util/lazy.cpp \ - util/memory_info.cpp \ - util/message.cpp \ - util/optional.cpp \ - util/optional_utils.cpp \ - util/parse_options.cpp \ - util/pointer_offset_size.cpp \ - util/prefix_filter.cpp \ - util/range.cpp \ - util/replace_symbol.cpp \ - util/sharing_map.cpp \ - util/sharing_node.cpp \ - util/simplify_expr.cpp \ - util/small_map.cpp \ - util/small_shared_n_way_ptr.cpp \ - util/ssa_expr.cpp \ - util/std_expr.cpp \ - util/string2int.cpp \ - util/structured_data.cpp \ - util/string_utils/capitalize.cpp \ - util/string_utils/escape_non_alnum.cpp \ - util/string_utils/join_string.cpp \ - util/string_utils/split_string.cpp \ - util/string_utils/strip_string.cpp \ - util/string_utils/wrap_line.cpp \ - util/symbol_table.cpp \ - util/symbol.cpp \ - util/unicode.cpp \ - util/xml.cpp \ - # Empty last line - -ifeq ($(OS),Windows_NT) - detected_OS := Windows -else - detected_OS := $(shell sh -c 'uname 2>/dev/null || echo Unknown') -endif - -ifeq ($(detected_OS),Linux) - ifneq ($(WITH_MEMORY_ANALYZER),0) - # only set if it wasn't explicitly unset - WITH_MEMORY_ANALYZER=1 - endif -endif - -ifeq ($(WITH_MEMORY_ANALYZER),1) - SRC += memory-analyzer/gdb_api.cpp -endif - -INCLUDES= -I ../src/ -I. - -CPROVER_DIR = . -include ../src/config.inc -include ../src/common - -cprover.dir: - $(MAKE) $(MAKEARGS) -C ../src - -testing-utils/testing-utils$(LIBEXT): cprover.dir - $(MAKE) $(MAKEARGS) -C testing-utils - -testing-utils-clean: - $(MAKE) $(MAKEARGS) -C testing-utils clean - -# We need to link bmc.o to the unit test, so here's everything it depends on... -BMC_DEPS =../src/cbmc/c_test_input_generator$(OBJEXT) \ - ../src/cbmc/cbmc_languages$(OBJEXT) \ - ../src/cbmc/cbmc_parse_options$(OBJEXT) \ - ../src/goto-cc/armcc_cmdline$(OBJEXT) \ - ../src/goto-cc/goto_cc_cmdline$(OBJEXT) \ - ../src/goto-instrument/source_lines$(OBJEXT) \ - ../src/goto-instrument/cover$(OBJEXT) \ - ../src/goto-instrument/cover_basic_blocks$(OBJEXT) \ - ../src/goto-instrument/cover_filter$(OBJEXT) \ - ../src/goto-instrument/cover_instrument_branch$(OBJEXT) \ - ../src/goto-instrument/cover_instrument_condition$(OBJEXT) \ - ../src/goto-instrument/cover_instrument_decision$(OBJEXT) \ - ../src/goto-instrument/cover_instrument_location$(OBJEXT) \ - ../src/goto-instrument/cover_instrument_mcdc$(OBJEXT) \ - ../src/goto-instrument/cover_instrument_other$(OBJEXT) \ - ../src/goto-instrument/cover_util$(OBJEXT) \ - ../src/goto-instrument/goto_program2code$(OBJEXT) \ - ../src/goto-instrument/reachability_slicer$(OBJEXT) \ - ../src/goto-instrument/nondet_static$(OBJEXT) \ - ../src/goto-instrument/full_slicer$(OBJEXT) \ - ../src/goto-instrument/unwindset$(OBJEXT) \ - ../src/xmllang/xmllang$(LIBEXT) \ - ../src/goto-symex/goto-symex$(LIBEXT) \ - ../src/jsil/jsil$(LIBEXT) \ - # Empty last line -# -CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \ - ../src/cpp/cpp$(LIBEXT) \ - ../src/json/json$(LIBEXT) \ - ../src/json-symtab-language/json-symtab-language$(LIBEXT) \ - ../src/linking/linking$(LIBEXT) \ - ../src/util/util$(LIBEXT) \ - ../src/big-int/big-int$(LIBEXT) \ - ../src/goto-checker/goto-checker$(LIBEXT) \ - ../src/goto-programs/goto-programs$(LIBEXT) \ - ../src/pointer-analysis/pointer-analysis$(LIBEXT) \ - ../src/langapi/langapi$(LIBEXT) \ - ../src/assembler/assembler$(LIBEXT) \ - ../src/analyses/analyses$(LIBEXT) \ - ../src/solvers/solvers$(LIBEXT) \ - ../src/statement-list/statement-list$(LIBEXT) \ - $(BMC_DEPS) - # Empty last line - -OBJ += $(CPROVER_LIBS) testing-utils/testing-utils$(LIBEXT) - -CATCH_TEST = unit_tests$(EXEEXT) -EXCLUDED_TESTS=expr_undefined_casts.cpp -ifneq ($(WITH_MEMORY_ANALYZER),1) -EXCLUDED_TESTS += gdb_api.cpp -endif - -N_CATCH_TESTS = $(shell \ - cat $$(find . -name "*.cpp" \ - $$(printf ' -not -name %s ' $(EXCLUDED_TESTS))) | \ - grep -E "(SCENARIO|TEST_CASE)" | grep -c -v '\[\.\]') - -CLEANFILES = $(CATCH_TEST) testing-utils/testing-utils$(LIBEXT) - -# only add a dependency for libraries to avoid triggering implicit rules, which -# would cause unnecessary rebuilds -$(filter %$(LIBEXT), $(CPROVER_LIBS)): cprover.dir - -all: $(CATCH_TEST) - -clean: testing-utils-clean - -test: $(CATCH_TEST) - # Include hidden tests by specifying "*,[.]" for tests to count - if ! ./$(CATCH_TEST) "*,[.]" -l | grep -q "^$(N_CATCH_TESTS) matching test cases" ; then \ - ./$(CATCH_TEST) "*,[.]" -l ; fi - ./$(CATCH_TEST) ${TAGS} - - -############################################################################### - -unit_tests$(EXEEXT): $(OBJ) - $(LINKBIN) diff --git a/unit/testing-utils/Makefile b/unit/testing-utils/Makefile deleted file mode 100644 index df3ef1b5cca..00000000000 --- a/unit/testing-utils/Makefile +++ /dev/null @@ -1,23 +0,0 @@ -SRC = \ - call_graph_test_utils.cpp \ - free_form_cmdline.cpp \ - get_goto_model_from_c.cpp \ - invariant.cpp \ - message.cpp \ - require_expr.cpp \ - require_symbol.cpp \ - run_test_with_compilers.cpp \ - # Empty last line (please keep above list sorted!) - -INCLUDES = -I .. -I . -I ../../src - -include ../../src/config.inc -include ../../src/common - -CLEANFILES = testing-utils$(LIBEXT) - -.PHONY: all -all: testing-utils$(LIBEXT) - -testing-utils$(LIBEXT): $(OBJ) - $(LINKLIB) From a63d64794ee95da45e940e2cfaae1f9c69e54e75 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 11 Nov 2020 12:16:18 +0000 Subject: [PATCH 3/4] Remove linux gcc make job --- buildspec-linux-make-gcc-cov.yml | 47 -------------------------------- 1 file changed, 47 deletions(-) delete mode 100644 buildspec-linux-make-gcc-cov.yml diff --git a/buildspec-linux-make-gcc-cov.yml b/buildspec-linux-make-gcc-cov.yml deleted file mode 100644 index 269b5778d45..00000000000 --- a/buildspec-linux-make-gcc-cov.yml +++ /dev/null @@ -1,47 +0,0 @@ -version: 0.2 - -env: - variables: - # CodeBuild console doesn't display color codes correctly - TESTPL_COLOR_OUTPUT: 0 - -phases: - install: - runtime-versions: - java: openjdk8 - commands: - - sed -i 's#/archive.ubuntu.com#/us-east-1.ec2.archive.ubuntu.com#g' /etc/apt/sources.list - - apt-get update -y - - apt-get install -y flex bison make git libwww-perl patch ccache libc6-dev-i386 jq gdb lcov curl - build: - commands: - - echo Build started on `date` - - make -C src minisat2-download - - make -C jbmc/src setup-submodules - - make -C src CXX="ccache g++" -j2 CPROVER_WITH_PROFILING=1 - - make -C unit CXX="ccache g++" -j2 CPROVER_WITH_PROFILING=1 - - make -C jbmc/src CXX="ccache g++" -j2 CPROVER_WITH_PROFILING=1 - - make -C jbmc/unit CXX="ccache g++" -j2 CPROVER_WITH_PROFILING=1 - - echo Build completed on `date` - post_build: - commands: - # codecov script creation - # If $CODEBUILD_SOURCE_VERSION starts with 'pr/', filter out pr number, if not, return empty - - VCS_PULL_REQUEST=$(echo $CODEBUILD_SOURCE_VERSION | sed '/^pr\//!d;s/^pr\///') - # If $CODEBUILD_SOURCE_VERSION is commit id, set $VCS_COMMIT_ID - - VCS_COMMIT_ID=$(echo $CODEBUILD_SOURCE_VERSION | sed -r '/^[a-z0-9]{40}$/!d') - - COV_SCRIPT=/root/.cache/codecov.sh - - if [ ! -f "$COV_SCRIPT" ]; then curl -s https://codecov.io/bash > "$COV_SCRIPT"; fi - # Run unit test - - scripts/run_test_upload_cov_report.sh unit - # Run regression tests - - scripts/run_test_upload_cov_report.sh regression - # Run regression/cbmc tests with test-cprover-smt2 - - scripts/run_test_upload_cov_report.sh cproversmt2 - -cache: - paths: - - '/var/cache/apt/**/*' - - '/var/lib/apt/lists/**/*' - - '/root/.ccache/**/*' - - '/root/.cache/codecov.sh' From a246df2f2313222f8620f77dbaab7ceabc95fe0b Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 11 Nov 2020 12:27:03 +0000 Subject: [PATCH 4/4] Use `cmake` instead of `make` for Linux + `clang` CI jobs So we can remove `make`. --- .github/workflows/pull-request-checks.yaml | 62 ++++++++++++++++++++++ buildspec-linux-clang-3.8.yml | 28 ---------- buildspec-linux-clang.yml | 44 --------------- 3 files changed, 62 insertions(+), 72 deletions(-) delete mode 100644 buildspec-linux-clang-3.8.yml delete mode 100644 buildspec-linux-clang.yml diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index c629833f8f7..9eadc962a06 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -35,6 +35,68 @@ jobs: env: TESTPL_JOBS: 2 + check-ubuntu-20_04-cmake-clang-8: + runs-on: ubuntu-20.04 + steps: + - uses: actions/checkout@v2 + with: + submodules: true + - name: Fetch dependencies + env: + # This is needed in addition to -yq to prevent apt-get from asking for + # user input + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get install -yq cmake ninja-build clang-8 clang++-8 maven flex bison libxml2-utils cpanminus dpkg-dev + cpanm Thread::Pool::Simple + - name: Configure using CMake + run: | + mkdir build + cd build + cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang-8 -DCMAKE_CXX_COMPILER=/usr/bin/clang++-8 + - name: Build with Ninja + run: cd build; ninja + - name: Check if package building works + run: | + cd build + ninja package + ls *.deb + - name: Run tests + run: cd build; ctest . -V -L CORE + env: + TESTPL_JOBS: 2 + + check-ubuntu-20_04-cmake-clang-3_8: + runs-on: ubuntu-20.04 + steps: + - uses: actions/checkout@v2 + with: + submodules: true + - name: Fetch dependencies + env: + # This is needed in addition to -yq to prevent apt-get from asking for + # user input + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get install -yq cmake ninja-build clang-3.8 clang++-3.8 maven flex bison libxml2-utils cpanminus dpkg-dev + cpanm Thread::Pool::Simple + - name: Configure using CMake + run: | + mkdir build + cd build + cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang-3.8 -DCMAKE_CXX_COMPILER=/usr/bin/clang++-3.8 + - name: Build with Ninja + run: cd build; ninja + - name: Check if package building works + run: | + cd build + ninja package + ls *.deb + - name: Run tests + run: cd build; ctest . -V -L CORE + env: + TESTPL_JOBS: 2 + check-macos-10_15-cmake-clang: runs-on: macos-10.15 steps: diff --git a/buildspec-linux-clang-3.8.yml b/buildspec-linux-clang-3.8.yml deleted file mode 100644 index e7d8fe0312f..00000000000 --- a/buildspec-linux-clang-3.8.yml +++ /dev/null @@ -1,28 +0,0 @@ -version: 0.2 - -env: - variables: - # CodeBuild console doesn't display color codes correctly - TESTPL_COLOR_OUTPUT: 0 - -phases: - install: - commands: - - sed -i 's#/archive.ubuntu.com#/us-east-1.ec2.archive.ubuntu.com#g' /etc/apt/sources.list - - apt-get update -y - - apt-get install -y clang-3.8 flex bison make git libwww-perl patch ccache libc6-dev-i386 jq openjdk-8-jdk maven - build: - commands: - - echo Build started on `date` - - make -C src minisat2-download - - make -C jbmc/src setup-submodules - - make -C src CXX='ccache /usr/bin/clang++-3.8' CXX_FLAGS='-Qunused-arguments -DDEBUG' - - make -C jbmc/src CXX='ccache /usr/bin/clang++-3.8' CXX_FLAGS='-Qunused-arguments -DDEBUG' - post_build: - commands: - - echo Build completed on `date` -cache: - paths: - - '/var/cache/apt/**/*' - - '/var/lib/apt/lists/**/*' - - '/root/.ccache/**/*' diff --git a/buildspec-linux-clang.yml b/buildspec-linux-clang.yml deleted file mode 100644 index ec78098a47f..00000000000 --- a/buildspec-linux-clang.yml +++ /dev/null @@ -1,44 +0,0 @@ -version: 0.2 - -env: - variables: - # CodeBuild console doesn't display color codes correctly - TESTPL_COLOR_OUTPUT: 0 - -phases: - install: - runtime-versions: - java: openjdk8 - commands: - - sed -i 's#/archive.ubuntu.com#/us-east-1.ec2.archive.ubuntu.com#g' /etc/apt/sources.list - - wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - - - add-apt-repository 'deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-8 main' - - apt-get update -y - - apt-get install -y clang-8 flex bison make git libwww-perl patch ccache libc6-dev-i386 jq gdb - build: - commands: - - echo Build started on `date` - - make -C src minisat2-download - - make -C jbmc/src setup-submodules - - make -C src CXX='ccache /usr/bin/clang++-8' CXX_FLAGS='-Qunused-arguments' -j2 - - make -C unit CXX='ccache /usr/bin/clang++-8' CXX_FLAGS='-Qunused-arguments' -j2 - - make -C jbmc/src CXX='ccache /usr/bin/clang++-8' CXX_FLAGS='-Qunused-arguments' -j2 - - make -C jbmc/unit CXX='ccache /usr/bin/clang++-8' CXX_FLAGS='-Qunused-arguments' -j2 - post_build: - commands: - - make -C unit test - - echo "Running expected failure tests" - - make TAGS="[!shouldfail]" -C unit test - - make -C regression test CXX='ccache /usr/bin/clang++-8' CXX_FLAGS='-Qunused-arguments' - - make -C regression/cbmc test-paths-lifo - - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 - - make -C jbmc/unit test - - echo "Running expected failure tests" - - make TAGS="[!shouldfail]" -C jbmc/unit test - - make -C jbmc/regression test - - echo Build completed on `date` -cache: - paths: - - '/var/cache/apt/**/*' - - '/var/lib/apt/lists/**/*' - - '/root/.ccache/**/*'