Merge branch 'release-2.4.0'

.travis.yml

@@ -39,21 +39,21 @@ env:
 
 before_install:
   - sudo rm -rf /usr/local/clang-7.0.0
-  - sudo add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial-7 main"
+  - sudo add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial-8 main"
   - wget -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
   - sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF
   - sudo apt-get install -y apt-transport-https
   - echo "deb https://download.mono-project.com/repo/ubuntu stable-xenial main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
   - sudo apt-get update
 
 install:
-  - sudo apt-get install -y clang-7 clang-format-7 llvm-7-dev mono-complete ninja-build
-  - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-7 20
-  - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-7 20
-  - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-7 20
-  - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-7 20
-  - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-7 20
-  - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-7 20
+  - sudo apt-get install -y clang-8 clang-format-8 llvm-8-dev mono-complete ninja-build
+  - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-8 20
+  - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-8 20
+  - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-8 20
+  - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-8 20
+  - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-8 20
+  - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-8 20
   - sudo pip install pyyaml psutil
 
 script:

CMakeLists.txt

@@ -6,7 +6,7 @@ cmake_minimum_required(VERSION 2.8)
 project(smack)
 
 if (NOT WIN32 OR MSYS OR CYGWIN)
-  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-7.1 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
+  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-8 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
 
   if (LLVM_CONFIG_EXECUTABLE STREQUAL "LLVM_CONFIG_EXECUTABLE-NOTFOUND")
     message(FATAL_ERROR "llvm-config could not be found!")

Dockerfile

@@ -1,4 +1,4 @@
-FROM ubuntu:16.04
+FROM ubuntu:18.04
 MAINTAINER Shaobo He <[email protected]>
 
 ENV SMACKDIR /home/user/smack

Doxyfile

@@ -5,7 +5,7 @@
 #---------------------------------------------------------------------------
 DOXYFILE_ENCODING      = UTF-8
 PROJECT_NAME           = smack
-PROJECT_NUMBER         = 2.3.0
+PROJECT_NUMBER         = 2.4.0
 PROJECT_BRIEF          = "A bounded software verifier."
 PROJECT_LOGO           =
 OUTPUT_DIRECTORY       = docs

Vagrantfile

@@ -10,7 +10,7 @@ Vagrant.configure(2) do |config|
   config.vm.synced_folder ".", "/home/vagrant/#{project_name}"
 
   config.vm.define :ubuntu do |ubuntu_config|
-    ubuntu_config.vm.box = "bento/ubuntu-16.04"
+    ubuntu_config.vm.box = "bento/ubuntu-18.04"
   end
 
   # This provision, 'fix-no-tty', gets rid of an error during build

bin/build.sh

@@ -279,8 +279,8 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then
     fi
 
     # Adding LLVM repository
-    sudo add-apt-repository "deb http://apt.llvm.org/${UBUNTU_CODENAME}/ llvm-toolchain-${UBUNTU_CODENAME}-${LLVM_SHORT_VERSION} main"
     ${WGET} -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
+    sudo add-apt-repository "deb http://apt.llvm.org/${UBUNTU_CODENAME}/ llvm-toolchain-${UBUNTU_CODENAME}-${LLVM_SHORT_VERSION} main"
     # Adding MONO repository
     sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF
     sudo apt-get install -y apt-transport-https

bin/versions

@@ -5,6 +5,6 @@ BOOGIE_COMMIT=5c829b6340
 CORRAL_COMMIT=c446f5e827
 SYMBOOGLIX_COMMIT=7210e5d09b
 LOCKPWN_COMMIT=73eddf97bd
-LLVM_SHORT_VERSION=7
-LLVM_FULL_VERSION=7.1.0
+LLVM_SHORT_VERSION=8
+LLVM_FULL_VERSION=8.0.1
 RUST_VERSION=2016-12-16

docs/installation.md

@@ -80,8 +80,8 @@ to Docker's official documentation.
 
 SMACK depends on the following projects:
 
-* [LLVM][] version [7.1.0][LLVM-7.1.0]
-* [Clang][] version [7.1.0][Clang-7.1.0]
+* [LLVM][] version [8.0.1][LLVM-8.0.1]
+* [Clang][] version [8.0.1][Clang-8.0.1]
 * [Python][] version 2.7 or greater
 * [Ninja][] version 1.5.1 or greater
 * [Mono][] version 5.0.0 or greater (except on Windows)
@@ -203,9 +203,9 @@ shell in the `test` directory by executing
 [CMake]: http://www.cmake.org
 [Python]: http://www.python.org
 [LLVM]: http://llvm.org
-[LLVM-7.1.0]: http://llvm.org/releases/download.html#7.1.0
+[LLVM-8.0.1]: http://llvm.org/releases/download.html#8.0.1
 [Clang]: http://clang.llvm.org
-[Clang-7.1.0]: http://llvm.org/releases/download.html#7.1.0
+[Clang-8.0.1]: http://llvm.org/releases/download.html#8.0.1
 [Boogie]: https://github.com/boogie-org/boogie
 [Corral]: https://github.com/boogie-org/corral
 [Z3]: https://github.com/Z3Prover/z3/

include/smack/SmackInstGenerator.h

@@ -36,7 +36,7 @@ class SmackInstGenerator : public llvm::InstVisitor<SmackInstGenerator> {
   Block *createBlock();
   Block *getBlock(llvm::BasicBlock *bb);
 
-  void generatePhiAssigns(llvm::TerminatorInst &i);
+  void generatePhiAssigns(llvm::Instruction &i);
   void generateGotoStmts(
       llvm::Instruction &i,
       std::vector<std::pair<const Expr *, llvm::BasicBlock *>> target);

lib/DSA/Basic.cpp

@@ -21,7 +21,6 @@
 #include "llvm/IR/Instructions.h"
 #include "llvm/IR/Intrinsics.h"
 #include "llvm/IR/Module.h"
-#include "llvm/IR/TypeBuilder.h"
 #include "llvm/IR/InstIterator.h"
 #include "llvm/IR/GetElementPtrTypeIterator.h"
 

lib/smack/NormalizeLoops.cpp

@@ -46,7 +46,7 @@ BasicBlock *makeForwardingBlock(BasicBlock *target) {
  * Returns a vector of each successor index in \param ti which equals \param
  * headerBlock.
  */
-std::vector<unsigned> getSuccessorIndices(TerminatorInst *ti,
+std::vector<unsigned> getSuccessorIndices(Instruction *ti,
                                           BasicBlock *headerBlock) {
   std::vector<unsigned> result;
   unsigned numSuccs = ti->getNumSuccessors();
@@ -71,7 +71,7 @@ std::vector<unsigned> getSuccessorIndices(TerminatorInst *ti,
  */
 void splitBlock(BasicBlock *BB, BasicBlock *headerBlock,
                 std::map<BasicBlock *, BasicBlock *> &blockMap) {
-  TerminatorInst *ti = BB->getTerminator();
+  Instruction *ti = BB->getTerminator();
 
   // Get a list of all successor indices which point to headerBlock.
   std::vector<unsigned> succIndices = getSuccessorIndices(ti, headerBlock);

lib/smack/SmackInstGenerator.cpp

@@ -177,7 +177,7 @@ void SmackInstGenerator::visitInstruction(llvm::Instruction &inst) {
   llvm_unreachable("Instruction not handled.");
 }
 
-void SmackInstGenerator::generatePhiAssigns(llvm::TerminatorInst &ti) {
+void SmackInstGenerator::generatePhiAssigns(llvm::Instruction &ti) {
   llvm::BasicBlock *block = ti.getParent();
   std::list<const Expr *> lhs;
   std::list<const Expr *> rhs;

share/smack/reach.py

@@ -11,7 +11,7 @@
 from smackgen import *
 from smackverify import *
 
-VERSION = '2.3.0'
+VERSION = '2.4.0'
 
 def reachParser():
     parser = argparse.ArgumentParser(add_help=False, parents=[verifyParser()])

share/smack/top.py

@@ -15,7 +15,7 @@
 from replay import replay_error_trace
 from frontend import link_bc_files, frontends, languages, extra_libs 
 
-VERSION = '2.3.0'
+VERSION = '2.4.0'
 
 def results(args):
   """A dictionary of the result output messages."""