diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 4451ee1820b..9eadc962a06 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -4,7 +4,7 @@ on: branches: [ develop ] jobs: - check-ubuntu-20_04-make-gcc: + check-ubuntu-20_04-cmake-gcc: runs-on: ubuntu-20.04 steps: - uses: actions/checkout@v2 @@ -15,32 +15,27 @@ jobs: # 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 + sudo apt-get install -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils cpanminus dpkg-dev 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 + - name: Configure using CMake + run: | + mkdir build + cd build + cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ + - 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-gcc: + check-ubuntu-20_04-cmake-clang-8: runs-on: ubuntu-20.04 steps: - uses: actions/checkout@v2 @@ -52,13 +47,13 @@ jobs: # user input DEBIAN_FRONTEND: noninteractive run: | - sudo apt-get install -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils cpanminus dpkg-dev + 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/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ + 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 @@ -71,29 +66,36 @@ jobs: env: TESTPL_JOBS: 2 - check-macos-10_15-make-clang: - runs-on: macos-10.15 + check-ubuntu-20_04-cmake-clang-3_8: + runs-on: ubuntu-20.04 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 + 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 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/**/*' 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' 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\**\*' 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)