Merge branch 'release-1.9.1'

.travis.yml

@@ -3,27 +3,50 @@ dist: trusty
 sudo: required
 compiler: clang
 
+addons:
+  apt:
+    packages:
+      - git
+      - cmake
+      - python-yaml
+      - python-psutil
+      - unzip
+      - libz-dev
+      - libedit-dev
+
+cache:
+  directories:
+    - $HOME/build/smackers/boogie
+    - $HOME/build/smackers/corral
+    - $HOME/build/smackers/symbooglix
+    - $HOME/build/smackers/lockpwn
+
 env:
   global:
     - COMPILER_NAME=clang COMPILER=clang++ CXX=clang++ CC=clang
   matrix:
     - TRAVIS_ENV="--exhaustive --folder=basic"
+    - TRAVIS_ENV="--exhaustive --folder=data"
     - TRAVIS_ENV="--exhaustive --folder=ntdrivers-simplified"
     - TRAVIS_ENV="--exhaustive --folder=bits"
     - TRAVIS_ENV="--exhaustive --folder=float"
     - TRAVIS_ENV="--exhaustive --folder=locks"
     - TRAVIS_ENV="--exhaustive --folder=contracts"
+    - TRAVIS_ENV="--exhaustive --folder=simd"
     - TRAVIS_ENV="--exhaustive --folder=memory-safety"
     - TRAVIS_ENV="--exhaustive --folder=pthread"
+    - TRAVIS_ENV="--exhaustive --folder=strings"
 
 before_install:
   - sudo rm -rf /usr/local/clang-3.5.0
   - sudo add-apt-repository "deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.9 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
+  - echo "deb http://download.mono-project.com/repo/ubuntu trusty main" | sudo tee /etc/apt/sources.list.d/mono-official.list
   - sudo apt-get update
 
 install:
-  - sudo apt-get install -y clang-3.9 llvm-3.9
+  - sudo apt-get install -y clang-3.9 llvm-3.9 mono-complete
   - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-3.9 20
   - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.9 20
   - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-3.9 20
@@ -38,4 +61,3 @@ script:
   - clang --version
   - clang++ --version
   - ./bin/build.sh
-

CMakeLists.txt

@@ -21,6 +21,8 @@ if (NOT WIN32 OR MSYS OR CYGWIN)
   string(REPLACE "-DNDEBUG" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
   string(REPLACE "-Wno-maybe-uninitialized" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
   string(REPLACE "-fuse-ld=gold" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
+  string(REPLACE "--no-keep-files-mapped" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
+  string(REPLACE "--no-map-whole-files" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
   string(REPLACE "-Wl," "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
   string(REPLACE "-gsplit-dwarf" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
   string(REGEX REPLACE "-O[0-9]" "" CMAKE_CXX_FLAGS "${LLVM_CXXFLAGS}")
@@ -172,9 +174,11 @@ add_library(smackTranslator STATIC
   include/smack/VerifierCodeMetadata.h
   include/smack/SimplifyLibCalls.h
   include/smack/SmackRep.h
+  include/smack/VectorOperations.h
   include/smack/MemorySafetyChecker.h
-  include/smack/SignedIntegerOverflowChecker.h
-  include/smack/SplitAggregateLoadStore.h
+  include/smack/IntegerOverflowChecker.h
+  include/smack/NormalizeLoops.h
+  include/smack/SplitAggregateValue.h
   lib/smack/AddTiming.cpp
   lib/smack/BoogieAst.cpp
   lib/smack/BplFilePrinter.cpp
@@ -192,9 +196,11 @@ add_library(smackTranslator STATIC
   lib/smack/VerifierCodeMetadata.cpp
   lib/smack/SimplifyLibCalls.cpp
   lib/smack/SmackRep.cpp
+  lib/smack/VectorOperations.cpp
   lib/smack/MemorySafetyChecker.cpp
-  lib/smack/SignedIntegerOverflowChecker.cpp
-  lib/smack/SplitAggregateLoadStore.cpp
+  lib/smack/IntegerOverflowChecker.cpp
+  lib/smack/NormalizeLoops.cpp
+  lib/smack/SplitAggregateValue.cpp
 )
 
 add_executable(llvm2bpl
@@ -211,6 +217,7 @@ INSTALL(TARGETS llvm2bpl
 INSTALL(FILES
   ${CMAKE_CURRENT_SOURCE_DIR}/bin/boogie
   ${CMAKE_CURRENT_SOURCE_DIR}/bin/corral
+  ${CMAKE_CURRENT_SOURCE_DIR}/bin/symbooglix
   ${CMAKE_CURRENT_SOURCE_DIR}/bin/lockpwn
   ${CMAKE_CURRENT_SOURCE_DIR}/bin/smack
   ${CMAKE_CURRENT_SOURCE_DIR}/bin/smack-doctor
@@ -223,5 +230,5 @@ INSTALL(FILES
 INSTALL(DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/share/smack
   DESTINATION share
   USE_SOURCE_PERMISSIONS
-  FILES_MATCHING PATTERN "*.py" PATTERN "*.h" PATTERN "*.c" PATTERN "Makefile"
+  FILES_MATCHING PATTERN "*.py" PATTERN "*.h" PATTERN "*.c" PATTERN "Makefile" PATTERN "*.rs" PATTERN "*.f90" PATTERN "*.di"
 )

Doxyfile

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

LICENSE

@@ -1,8 +1,8 @@
 The MIT License
 
-Copyright (c) 2008-2017 Zvonimir Rakamaric ([email protected]),
+Copyright (c) 2008-2018 Zvonimir Rakamaric ([email protected]),
                         Michael Emmi ([email protected])
-Modified work Copyright (c) 2013-2017 Montgomery Carter,
+Modified work Copyright (c) 2013-2018 Montgomery Carter,
                                       Pantazis Deligiannis,
                                       Dietrich Geisler,
                                       Arvind Haran,
@@ -51,6 +51,6 @@ tools and packages, which come with their own licenses:
 - LLVM, clang, LLVM runtime (http://llvm.org/)
 - mono (http://www.mono-project.com/)
 - Boogie (https://github.com/boogie-org/boogie/)
-- Corral (http://corral.codeplex.com/)
+- Corral (https://github.com/boogie-org/corral/)
 - Z3 (https://github.com/Z3Prover/z3/)
 

README.md

@@ -13,14 +13,14 @@ bitwise operations.
 
 Under the hood, SMACK is a translator from the [LLVM](http://www.llvm.org)
 compiler's popular intermediate representation (IR) into the
-[Boogie](http://boogie.codeplex.com) intermediate verification language (IVL).
+[Boogie](https://github.com/boogie-org/boogie) intermediate verification language (IVL).
 Sourcing LLVM IR exploits an increasing number of compiler front-ends,
 optimizations, and analyses. Currently SMACK only supports the C language via
 the [Clang](http://clang.llvm.org) compiler, though we are working on providing
 support for additional languages. Targeting Boogie exploits a canonical
 platform which simplifies the implementation of algorithms for verification,
 model checking, and abstract interpretation. Currently, SMACK leverages the
-[Boogie](http://boogie.codeplex.com) and [Corral](http://corral.codeplex.com)
+[Boogie](https://github.com/boogie-org/boogie) and [Corral](https://github.com/boogie-org/corral)
 verifiers.
 
 See below for system requirements, installation, usage, and everything else.

bin/boogie

@@ -1,2 +1,6 @@
 #!/bin/bash
+if [ -z "$BOOGIE" ] ; then
+  echo "The required BOOGIE environment variable is not set. See SMACK documentation for details."
+  exit 1
+fi
 $BOOGIE "$@"