Merge branch 'release-1.7.0'

Author: zvonimir

Doxyfile

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

README.md

@@ -1,5 +1,7 @@
 [![Build Status](http://kornat.cs.utah.edu:8080/job/smack/badge/icon)](http://kornat.cs.utah.edu:8080/job/smack/)
 
+<img src="docs/smack-logo.png" width=400 alt="SMACK Logo" align="right">
+
 SMACK is both a *modular software verification toolchain* and a
 *self-contained software verifier*. It can be used to verify the assertions
 in its input programs. In its default mode, assertions are verified up to a

bin/build.sh

@@ -162,7 +162,7 @@ linux-opensuse*)
 
 linux-ubuntu-14*)
   Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/z3-4.4.1-x64-ubuntu-14.04.zip"
-  DEPENDENCIES+=" clang-3.6 llvm-3.6 mono-complete libz-dev libedit-dev"
+  DEPENDENCIES+=" clang-3.7 llvm-3.7 mono-complete libz-dev libedit-dev"
   ;;
 
 linux-ubuntu-12*)
@@ -223,19 +223,19 @@ then
 
   linux-ubuntu-14*)
     # Adding LLVM repository
-    sudo add-apt-repository "deb http://llvm-apt.ecranbleu.org/apt/trusty/ llvm-toolchain-trusty-3.6 main"
+    sudo add-apt-repository "deb http://llvm-apt.ecranbleu.org/apt/trusty/ llvm-toolchain-trusty-3.7 main"
     ${WGET} -O - http://llvm-apt.ecranbleu.org/apt/llvm-snapshot.gpg.key | sudo apt-key add -
     # Adding MONO repository
     sudo add-apt-repository "deb http://download.mono-project.com/repo/debian wheezy main"
     sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF
 #    echo "deb http://download.mono-project.com/repo/debian wheezy main" | sudo tee /etc/apt/sources.list.d/mono-xamarin.list
     sudo apt-get update
     sudo apt-get install -y ${DEPENDENCIES}
-    sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-3.6 20
-    sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.6 20
-    sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-3.6 20
-    sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-3.6 20
-    sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-3.6 20
+    sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-3.7 20
+    sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.7 20
+    sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-3.7 20
+    sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-3.7 20
+    sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-3.7 20
     ;;
 
   linux-ubuntu-12*)
@@ -299,13 +299,13 @@ then
   mkdir -p ${LLVM_DIR}/src/{tools/clang,projects/compiler-rt}
   mkdir -p ${LLVM_DIR}/build
 
-  ${WGET} http://llvm.org/releases/3.6.2/llvm-3.6.2.src.tar.xz
-  ${WGET} http://llvm.org/releases/3.6.2/cfe-3.6.2.src.tar.xz
-  ${WGET} http://llvm.org/releases/3.6.2/compiler-rt-3.6.2.src.tar.xz
+  ${WGET} http://llvm.org/releases/3.7.1/llvm-3.7.1.src.tar.xz
+  ${WGET} http://llvm.org/releases/3.7.1/cfe-3.7.1.src.tar.xz
+  ${WGET} http://llvm.org/releases/3.7.1/compiler-rt-3.7.1.src.tar.xz
 
-  tar -C ${LLVM_DIR}/src -xvf llvm-3.6.2.src.tar.xz --strip 1
-  tar -C ${LLVM_DIR}/src/tools/clang -xvf cfe-3.6.2.src.tar.xz --strip 1
-  tar -C ${LLVM_DIR}/src/projects/compiler-rt -xvf compiler-rt-3.6.2.src.tar.xz --strip 1
+  tar -C ${LLVM_DIR}/src -xvf llvm-3.7.1.src.tar.xz --strip 1
+  tar -C ${LLVM_DIR}/src/tools/clang -xvf cfe-3.7.1.src.tar.xz --strip 1
+  tar -C ${LLVM_DIR}/src/projects/compiler-rt -xvf compiler-rt-3.7.1.src.tar.xz --strip 1
 
   cd ${LLVM_DIR}/build/
   cmake ${CMAKE_INSTALL_PREFIX} -DCMAKE_BUILD_TYPE=Release ../src

bin/package-smack.sh

@@ -6,7 +6,7 @@
 # Note: this script requires CDE to be downloaded from
 # http://www.pgbovine.net/cde.html
 
-VERSION=1.6.0
+VERSION=1.7.0
 PACKAGE=smack-$VERSION-64
 
 # Create folder to export

bin/versions

@@ -1,3 +1,3 @@
 MONO_VERSION=3.8.0
-BOOGIE_COMMIT=ba4f9fa1fb
+BOOGIE_COMMIT=4e4c3a5252
 CORRAL_COMMIT=874a078e39

docs/code-of-conduct.md

@@ -0,0 +1,75 @@
+## Contributor Covenant Code of Conduct
+
+### Our Pledge
+
+In the interest of fostering an open and welcoming environment, we as
+contributors and maintainers pledge to making participation in our project and
+our community a harassment-free experience for everyone, regardless of age, body
+size, disability, ethnicity, gender identity and expression, level of experience,
+nationality, personal appearance, race, religion, or sexual identity and
+orientation.
+
+### Our Standards
+
+Examples of behavior that contributes to creating a positive environment
+include:
+
+* Using welcoming and inclusive language
+* Being respectful of differing viewpoints and experiences
+* Gracefully accepting constructive criticism
+* Focusing on what is best for the community
+* Showing empathy towards other community members
+
+Examples of unacceptable behavior by participants include:
+
+* The use of sexualized language or imagery and unwelcome sexual attention or
+advances
+* Trolling, insulting/derogatory comments, and personal or political attacks
+* Public or private harassment
+* Publishing others' private information, such as a physical or electronic
+  address, without explicit permission
+* Other conduct which could reasonably be considered inappropriate in a
+  professional setting
+
+### Our Responsibilities
+
+Project maintainers are responsible for clarifying the standards of acceptable
+behavior and are expected to take appropriate and fair corrective action in
+response to any instances of unacceptable behavior.
+
+Project maintainers have the right and responsibility to remove, edit, or
+reject comments, commits, code, wiki edits, issues, and other contributions
+that are not aligned to this Code of Conduct, or to ban temporarily or
+permanently any contributor for other behaviors that they deem inappropriate,
+threatening, offensive, or harmful.
+
+### Scope
+
+This Code of Conduct applies both within project spaces and in public spaces
+when an individual is representing the project or its community. Examples of
+representing a project or community include using an official project e-mail
+address, posting via an official social media account, or acting as an appointed
+representative at an online or offline event. Representation of a project may be
+further defined and clarified by project maintainers.
+
+### Enforcement
+
+Instances of abusive, harassing, or otherwise unacceptable behavior may be
+reported by contacting the project team at
+[zvonimir@cs.utah.edu](mailto:zvonimir@cs.utah.edu). All complaints will be
+reviewed and investigated and will result in a response that is deemed
+necessary and appropriate to the circumstances. The project team is obligated
+to maintain confidentiality with regard to the reporter of an incident.
+Further details of specific enforcement policies may be posted separately.
+
+Project maintainers who do not follow or enforce the Code of Conduct in good
+faith may face temporary or permanent repercussions as determined by other
+members of the project's leadership.
+
+### Attribution
+
+This Code of Conduct is adapted from the [Contributor Covenant][homepage], version 1.4,
+available at [http://contributor-covenant.org/version/1/4][version]
+
+[homepage]: http://contributor-covenant.org
+[version]: http://contributor-covenant.org/version/1/4/

docs/contributions.md

@@ -4,8 +4,7 @@
 The information provided here is a must read for anyone who would like to
 contribute to SMACK. Hence, please make sure to study thoroughly the following
 items before you start contributing:
-* We adhere to the [Open Code of
-  Conduct](http://todogroup.org/opencodeofconduct/#SMACK/zvonimir@cs.utah.edu).
+* We adhere to the [Contributor Covenant Code of Conduct](code-of-conduct.md).
   By participating, you are expected to honor this code.
 * We use this [git branching
   model](http://nvie.com/posts/a-successful-git-branching-model/). Please avoid

docs/installation.md

@@ -59,8 +59,8 @@ vagrant destroy
 
 SMACK depends on the following projects:
 
-* [LLVM][] version [3.5.0][LLVM-3.5.0]
-* [Clang][] version [3.5.0][Clang-3.5.0]
+* [LLVM][] version [3.7.1][LLVM-3.7.1]
+* [Clang][] version [3.7.1][Clang-3.7.1]
 * [Python][] version 2.7 or greater
 * [Mono][] version 3.8.0 or greater (except on Windows)
 * [Z3][] or compatible SMT-format theorem prover
@@ -168,12 +168,12 @@ shell in the `test` directory by executing
 [CMake]: http://www.cmake.org
 [Python]: http://www.python.org
 [LLVM]: http://llvm.org
-[LLVM-3.5.0]: http://llvm.org/releases/download.html#3.5.0
+[LLVM-3.7.1]: http://llvm.org/releases/download.html#3.7.1
 [Clang]: http://clang.llvm.org
-[Clang-3.5.0]: http://llvm.org/releases/download.html#3.5.0
+[Clang-3.7.1]: http://llvm.org/releases/download.html#3.7.1
 [Boogie]: https://github.com/boogie-org/boogie
 [Corral]: https://corral.codeplex.com/
-[Z3]: http://z3.codeplex.com/
+[Z3]: https://github.com/Z3Prover/z3/
 [Mono]: http://www.mono-project.com/
 [Cygwin]: https://www.cygwin.com
 [.NET]: https://msdn.microsoft.com/en-us/vstudio/aa496123.aspx

docs/people.md

@@ -10,9 +10,9 @@
 ### Contributors
 
 * [Montgomery Carter](http://www.linkedin.com/pub/montgomery-carter/12/a89/512) ([SOAR Lab](http://soarlab.org/), University of Utah)
-* [Pantazis Deligiannis](http://www.doc.ic.ac.uk/~pd1113/index.html) (Imperial College London)
+* [Pantazis Deligiannis](http://pdeligia.github.io/) (Microsoft Research)
 * [Arvind Haran](http://www.cs.utah.edu/~haran) ([SOAR Lab](http://soarlab.org/), University of Utah)
-* Shaobo He ([SOAR Lab](http://soarlab.org/), University of Utah)
-* Jiten Thakkar ([SOAR Lab](http://soarlab.org/), University of Utah)
+* [Shaobo He](http://www.cs.utah.edu/~shaobo) ([SOAR Lab](http://soarlab.org/), University of Utah)
+* [Jiten Thakkar](http://jiten-thakkar.com) ([SOAR Lab](http://soarlab.org/), University of Utah)
 * [Jonathan Whitaker](https://www.linkedin.com/in/jonathan-whitaker-5a8b2484) ([SOAR Lab](http://soarlab.org/), University of Utah)