Merge branch 'release-2.2.0'

smackers · Jul 28, 2019 · eff7f3b · eff7f3b
2 parents 174ed53 + a981734
commit eff7f3b
Show file tree

Hide file tree

Showing 20 changed files with 1,490 additions and 654 deletions.
diff --git a/.travis.yml b/.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-5.0 main"
+  - sudo add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial-6.0 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-5.0 clang-format-5.0 llvm-5.0-dev mono-complete ninja-build
-  - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-5.0 20
-  - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-5.0 20
-  - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-5.0 20
-  - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-5.0 20
-  - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-5.0 20
-  - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-5.0 20
+  - sudo apt-get install -y clang-6.0 clang-format-6.0 llvm-6.0-dev mono-complete ninja-build
+  - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-6.0 20
+  - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-6.0 20
+  - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-6.0 20
+  - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-6.0 20
+  - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-6.0 20
+  - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-6.0 20
   - sudo pip install pyyaml psutil
 
 script:

diff --git a/CMakeLists.txt b/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-5.0 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
+  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-6.0 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!")

diff --git a/Doxyfile b/Doxyfile
@@ -5,7 +5,7 @@
 #---------------------------------------------------------------------------
 DOXYFILE_ENCODING      = UTF-8
 PROJECT_NAME           = smack
-PROJECT_NUMBER         = 2.1.0
+PROJECT_NUMBER         = 2.2.0
 PROJECT_BRIEF          = "A bounded software verifier."
 PROJECT_LOGO           =
 OUTPUT_DIRECTORY       = docs

diff --git a/bin/versions b/bin/versions
@@ -5,6 +5,6 @@ BOOGIE_COMMIT=5c829b6340
 CORRAL_COMMIT=c446f5e827
 SYMBOOGLIX_COMMIT=7210e5d09b
 LOCKPWN_COMMIT=73eddf97bd
-LLVM_SHORT_VERSION=5.0
-LLVM_FULL_VERSION=5.0.2
+LLVM_SHORT_VERSION=6.0
+LLVM_FULL_VERSION=6.0.1
 RUST_VERSION=2016-12-16
diff --git a/docs/installation.md b/docs/installation.md
@@ -80,8 +80,8 @@ to Docker's official documentation.
 
 SMACK depends on the following projects:
 
-* [LLVM][] version [5.0.2][LLVM-5.0.2]
-* [Clang][] version [5.0.2][Clang-5.0.2]
+* [LLVM][] version [6.0.1][LLVM-6.0.1]
+* [Clang][] version [6.0.1][Clang-6.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-5.0.2]: http://llvm.org/releases/download.html#5.0.2
+[LLVM-6.0.1]: http://llvm.org/releases/download.html#6.0.1
 [Clang]: http://clang.llvm.org
-[Clang-5.0.2]: http://llvm.org/releases/download.html#5.0.2
+[Clang-6.0.1]: http://llvm.org/releases/download.html#6.0.1
 [Boogie]: https://github.com/boogie-org/boogie
 [Corral]: https://github.com/boogie-org/corral
 [Z3]: https://github.com/Z3Prover/z3/

diff --git a/include/smack/Debug.h b/include/smack/Debug.h
@@ -36,6 +36,6 @@ extern bool DebugFlag;
 llvm::raw_ostream &dbgs();
 
 #define SDEBUG(X) SMACK_DEBUG_WITH_TYPE(DEBUG_TYPE, X)
-}
+} // namespace smack
 
 #endif
diff --git a/lib/smack/SimplifyLibCalls.cpp b/lib/smack/SimplifyLibCalls.cpp
@@ -8,6 +8,7 @@
 #include "smack/Debug.h"
 #include "smack/Naming.h"
 #include "smack/SmackOptions.h"
+#include "llvm/Analysis/OptimizationRemarkEmitter.h"
 #include "llvm/Analysis/TargetLibraryInfo.h"
 #include "llvm/Transforms/Utils/BasicBlockUtils.h"
 
@@ -28,7 +29,8 @@ void SimplifyLibCalls::getAnalysisUsage(AnalysisUsage &AU) const {
 bool SimplifyLibCalls::runOnModule(Module &M) {
   modified = false;
   simplifier = new LibCallSimplifier(
-      M.getDataLayout(), &getAnalysis<TargetLibraryInfoWrapperPass>().getTLI());
+      M.getDataLayout(), &getAnalysis<TargetLibraryInfoWrapperPass>().getTLI(),
+      getAnalysis<OptimizationRemarkEmitterWrapperPass>().getORE());
   if (simplifier)
     visit(M);
   return modified;

diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp
@@ -647,7 +647,10 @@ const Expr *SmackRep::lit(const llvm::Value *v, bool isUnsigned) {
       const APFloat APF = CFP->getValueAPF();
       const Type *type = CFP->getType();
       unsigned expSize, sigSize;
-      if (type->isFloatTy()) {
+      if (type->isHalfTy()) {
+        expSize = 5;
+        sigSize = 11;
+      } else if (type->isFloatTy()) {
         expSize = 8;
         sigSize = 24;
       } else if (type->isDoubleTy()) {

diff --git a/share/smack/reach.py b/share/smack/reach.py
@@ -11,7 +11,7 @@
 from smackgen import *
 from smackverify import *
 
-VERSION = '2.1.0'
+VERSION = '2.2.0'
 
 def reachParser():
     parser = argparse.ArgumentParser(add_help=False, parents=[verifyParser()])

diff --git a/share/smack/top.py b/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.1.0'
+VERSION = '2.2.0'
 
 def results(args):
   """A dictionary of the result output messages."""

diff --git a/test/ntdrivers-simplified/cdaudio_simpl1_false.cil.c b/test/ntdrivers-simplified/cdaudio_simpl1_false.cil.c
@@ -2768,7 +2768,9 @@ int main(void) {
                 }
               } else {
                 if (status != 259) {
-                  { errorFn(); }
+                  {
+                    errorFn();
+                  }
                 } else {
                 }
               }