Merge branch 'release-1.4.1'

CMakeLists.txt

@@ -179,9 +179,9 @@ INSTALL(FILES ${CMAKE_CURRENT_SOURCE_DIR}/bin/boogie
 	${CMAKE_CURRENT_SOURCE_DIR}/bin/corral
 	${CMAKE_CURRENT_SOURCE_DIR}/bin/llvm2bpl.py
 	${CMAKE_CURRENT_SOURCE_DIR}/bin/smackgen.py
-	${CMAKE_CURRENT_SOURCE_DIR}/bin/smack-verify.py
+	${CMAKE_CURRENT_SOURCE_DIR}/bin/smackverify.py
 	PERMISSIONS OWNER_EXECUTE OWNER_WRITE OWNER_READ
 	GROUP_EXECUTE GROUP_READ WORLD_EXECUTE WORLD_READ
   DESTINATION bin
 )
-
+

LICENSE

@@ -1,6 +1,6 @@
 The MIT License
 
-Copyright (c) 2008-2013 Zvonimir Rakamaric (zvonimir@cs.utah.edu),
+Copyright (c) 2008-2014 Zvonimir Rakamaric (zvonimir@cs.utah.edu),
                         Michael Emmi (michael.emmi@gmail.com)
 
 Permission is hereby granted, free of charge, to any person obtaining a copy

Makefile.common.in

@@ -1,6 +1,6 @@
 # Set the name of the project here
 PROJECT_NAME := smack
-PROJ_VERSION := 1.4.0
+PROJ_VERSION := 1.4.1
 
 # Set this variable to the top of the LLVM source tree.
 LLVM_SRC_ROOT = @LLVM_SRC@

Makefile.llvm.config.in

@@ -59,7 +59,7 @@ PROJ_SRC_DIR := $(call realpath, $(PROJ_SRC_ROOT)/$(patsubst $(PROJ_OBJ_ROOT)%,%
 prefix          := $(PROJ_INSTALL_ROOT)
 PROJ_prefix     := $(prefix)
 ifndef PROJ_VERSION
-PROJ_VERSION := 1.4.0
+PROJ_VERSION := 1.4.1
 endif
 
 PROJ_bindir     := $(PROJ_prefix)/bin

README.md

@@ -11,6 +11,9 @@ experience verifying C language programs is encouraging: SMACK is competitive
 in SV-COMP benchmarks, is able to translate large programs (100 KLOC), and is
 used in several verification research prototypes.
 
+*Please drop us a note if using SMACK in your research or teaching. We would
+love to learn more about your experience.*
+
 ## A Quick Demo
 
 SMACK can verify C programs, such as the following:
@@ -49,7 +52,7 @@ concluding that the original program `simple.c` is verified to be correct.
 While SMACK is designed to be a *modular* verifier, for our convenience, this
 whole process has also been wrapped into a single command in SMACK:
 
-    smack-verify.py simple.c -o simple.bpl
+    smackverify.py simple.c -o simple.bpl
 
 which equally reports that the program `simple.c` is verified.
 

autoconf/configure.ac

@@ -1,7 +1,7 @@
 dnl **************************************************************************
 dnl * Initialize
 dnl **************************************************************************
-AC_INIT([[SMACK]],[[1.4.0]],[smack-dev@googlegroups.com],[smack],[http://github.com/smackers/smack])
+AC_INIT([[SMACK]],[[1.4.1]],[smack-dev@googlegroups.com],[smack],[http://github.com/smackers/smack])
 
 dnl Identify where LLVM source tree is
 LLVM_SRC_ROOT="../.."

bin/build-linux-cmake.sh

@@ -55,6 +55,7 @@ sudo apt-get install -y git
 sudo apt-get install -y mercurial
 sudo apt-get install -y autoconf
 sudo apt-get install -y wget
+sudo apt-get install -y unzip
 
 fi
 
@@ -96,7 +97,7 @@ sudo make install
 
 # Install libgdiplus
 sudo apt-get install -y libglib2.0-dev libfontconfig1-dev libfreetype6-dev libxrender-dev 
-sudo apt-get install -y libtiff-dev libjpeg-dev libgif-dev libpng-dev
+sudo apt-get install -y libtiff-dev libjpeg-dev libgif-dev libpng-dev libcairo2-dev
 cd ${MONO_DIR}
 git clone git://github.com/mono/libgdiplus.git
 cd libgdiplus
@@ -145,7 +146,7 @@ if [ ${INSTALL_BOOGIE} -eq 1 ]; then
 mkdir -p ${BOOGIE_DIR}
 
 # Get Boogie
-hg clone -r f59ad49fc3a4 https://hg.codeplex.com/boogie ${BOOGIE_DIR}
+hg clone -r 661c32e8d5ca https://hg.codeplex.com/boogie ${BOOGIE_DIR}
 
 # Build Boogie
 cd ${BOOGIE_DIR}/Source
@@ -167,7 +168,7 @@ mkdir -p ${CORRAL_DIR}
 # Get Corral
 git clone https://git01.codeplex.com/corral ${CORRAL_DIR}
 cd ${CORRAL_DIR}
-git checkout 9311d7273384
+git checkout df4d2e2ace82
 
 # Build Corral
 cd ${CORRAL_DIR}/references

bin/build-linux-ubuntu_1404.sh

@@ -0,0 +1,225 @@
+#!/bin/bash
+
+################################################################################
+#
+# Builds and installs SMACK in BASE_DIR (see shell var below in settings).
+#
+# Requirements (see "Install required packages" below):
+# - git
+# - mercurial
+# - python
+# - gcc
+# - g++
+# - make
+# - autoconf
+# - mono
+#
+################################################################################
+
+# Exit on error
+set -e
+
+################################################################################
+
+# Settings
+
+# Change this to the desired path (default uses working-dir/smack-project)
+BASE_DIR=`pwd`/smack-project
+
+# Set these flags to control various installation options
+INSTALL_PACKAGES=1
+INSTALL_Z3=1
+INSTALL_BOOGIE=1
+INSTALL_CORRAL=1
+INSTALL_LLVM=1
+INSTALL_SMACK=1
+
+# Other dirs
+Z3_DIR="${BASE_DIR}/z3"
+BOOGIE_DIR="${BASE_DIR}/boogie"
+CORRAL_DIR="${BASE_DIR}/corral"
+LLVM_DIR="${BASE_DIR}/llvm"
+SMACK_DIR="${BASE_DIR}/smack"
+
+################################################################################
+
+# Install required packages
+
+if [ ${INSTALL_PACKAGES} -eq 1 ]; then
+
+sudo apt-get install -y g++
+sudo apt-get install -y git
+sudo apt-get install -y mercurial
+sudo apt-get install -y autoconf
+sudo apt-get install -y wget
+sudo apt-get install -y unzip
+sudo apt-get install -y monodevelop
+
+fi
+
+################################################################################
+
+# Set up base directory for everything
+mkdir -p ${BASE_DIR}
+cd ${BASE_DIR}
+
+################################################################################
+
+# Z3
+
+if [ ${INSTALL_Z3} -eq 1 ]; then
+
+mkdir -p ${Z3_DIR}/src
+mkdir -p ${Z3_DIR}/install
+
+# Get Z3
+cd ${Z3_DIR}/src/
+wget "http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx?ProjectName=z3&changeSetId=89c1785b73225a1b363c0e485f854613121b70a7"
+unzip -o SourceControlFileDownload*
+rm -f SourceControlFileDownload*
+
+# Configure Z3 and build
+cd ${Z3_DIR}/src/
+autoconf
+./configure --prefix=${Z3_DIR}/install
+python scripts/mk_make.py
+cd build
+make
+sudo make install
+
+cd ${BASE_DIR}
+
+fi
+
+################################################################################
+
+# Boogie
+
+if [ ${INSTALL_BOOGIE} -eq 1 ]; then
+
+mkdir -p ${BOOGIE_DIR}
+
+# Get Boogie
+hg clone -r 661c32e8d5ca https://hg.codeplex.com/boogie ${BOOGIE_DIR}
+
+# Build Boogie
+cd ${BOOGIE_DIR}/Source
+xbuild Boogie.sln
+ln -s ${Z3_DIR}/install/bin/z3 ${BOOGIE_DIR}/Binaries/z3.exe
+
+cd ${BASE_DIR}
+
+fi
+
+################################################################################
+
+# Corral
+
+if [ ${INSTALL_CORRAL} -eq 1 ]; then
+
+mkdir -p ${CORRAL_DIR}
+
+# Get Corral
+git clone https://git01.codeplex.com/corral ${CORRAL_DIR}
+cd ${CORRAL_DIR}
+git checkout df4d2e2ace82
+
+# Build Corral
+cd ${CORRAL_DIR}/references
+
+cp ${BOOGIE_DIR}/Binaries/AbsInt.dll .
+cp ${BOOGIE_DIR}/Binaries/Basetypes.dll .
+cp ${BOOGIE_DIR}/Binaries/CodeContractsExtender.dll .
+cp ${BOOGIE_DIR}/Binaries/Concurrency.dll .
+cp ${BOOGIE_DIR}/Binaries/Core.dll .
+cp ${BOOGIE_DIR}/Binaries/ExecutionEngine.dll .
+cp ${BOOGIE_DIR}/Binaries/Graph.dll .
+cp ${BOOGIE_DIR}/Binaries/Houdini.dll .
+cp ${BOOGIE_DIR}/Binaries/Model.dll .
+cp ${BOOGIE_DIR}/Binaries/ParserHelper.dll .
+cp ${BOOGIE_DIR}/Binaries/Provers.SMTLib.dll .
+cp ${BOOGIE_DIR}/Binaries/VCExpr.dll .
+cp ${BOOGIE_DIR}/Binaries/VCGeneration.dll .
+cp ${BOOGIE_DIR}/Binaries/Boogie.exe .
+cp ${BOOGIE_DIR}/Binaries/BVD.exe .
+cp ${BOOGIE_DIR}/Binaries/Doomed.dll .
+cp ${BOOGIE_DIR}/Binaries/Predication.dll .
+
+cd ${CORRAL_DIR}
+xbuild cba.sln
+ln -s ${Z3_DIR}/install/bin/z3 ${CORRAL_DIR}/bin/Debug/z3.exe
+
+cd ${BASE_DIR}
+
+fi
+
+################################################################################
+
+# LLVM
+
+if [ ${INSTALL_LLVM} -eq 1 ]; then
+
+mkdir -p ${LLVM_DIR}/src
+mkdir -p ${LLVM_DIR}/build
+mkdir -p ${LLVM_DIR}/install
+
+# Get llvm and extract
+wget http://llvm.org/releases/3.4/llvm-3.4.src.tar.gz
+wget http://llvm.org/releases/3.4/clang-3.4.src.tar.gz
+wget http://llvm.org/releases/3.4/compiler-rt-3.4.src.tar.gz
+
+tar -C ${LLVM_DIR}/src -xzvf llvm-3.4.src.tar.gz --strip 1
+mkdir -p ${LLVM_DIR}/src/tools/clang
+tar -C ${LLVM_DIR}/src/tools/clang -xzvf clang-3.4.src.tar.gz --strip 1
+mkdir -p ${LLVM_DIR}/src/projects/compiler-rt
+tar -C ${LLVM_DIR}/src/projects/compiler-rt -xzvf compiler-rt-3.4.src.tar.gz --strip 1
+
+# Configure llvm and build
+cd ${LLVM_DIR}/build/
+${LLVM_DIR}/src/configure --prefix=${LLVM_DIR}/install --enable-optimized
+make
+make install
+
+cd ${BASE_DIR}
+
+fi
+
+################################################################################
+
+# SMACK
+
+if [ ${INSTALL_SMACK} -eq 1 ]; then
+
+mkdir -p ${SMACK_DIR}/src
+mkdir -p ${SMACK_DIR}/build
+mkdir -p ${SMACK_DIR}/install
+
+# Get SMACK
+git clone git://github.com/smackers/smack.git ${SMACK_DIR}/src/
+
+# Configure SMACK and build
+cd ${SMACK_DIR}/build/
+${SMACK_DIR}/src/configure --with-llvmsrc=${LLVM_DIR}/src --with-llvmobj=${LLVM_DIR}/build --prefix=${SMACK_DIR}/install --enable-optimized
+make
+make install
+
+cd ${BASE_DIR}
+
+# Set required paths and environment variables
+export BOOGIE="mono ${BOOGIE_DIR}/Binaries/Boogie.exe"
+export CORRAL="mono ${CORRAL_DIR}/bin/Debug/corral.exe"
+export PATH=${LLVM_DIR}/install/bin:$PATH
+export PATH=${SMACK_DIR}/install/bin:$PATH
+
+# Run SMACK regressions
+cd ${SMACK_DIR}/src/test
+make
+./regtest.py
+./regtest-corral.py
+
+cd ${BASE_DIR}
+
+fi
+
+################################################################################
+

bin/build-linux.sh

@@ -54,6 +54,7 @@ sudo apt-get install -y git
 sudo apt-get install -y mercurial
 sudo apt-get install -y autoconf
 sudo apt-get install -y wget
+sudo apt-get install -y unzip
 
 fi
 
@@ -83,7 +84,7 @@ sudo make install
 
 # Install libgdiplus
 sudo apt-get install -y libglib2.0-dev libfontconfig1-dev libfreetype6-dev libxrender-dev 
-sudo apt-get install -y libtiff-dev libjpeg-dev libgif-dev libpng-dev
+sudo apt-get install -y libtiff-dev libjpeg-dev libgif-dev libpng-dev libcairo2-dev
 cd ${MONO_DIR}
 git clone git://github.com/mono/libgdiplus.git
 cd libgdiplus
@@ -132,7 +133,7 @@ if [ ${INSTALL_BOOGIE} -eq 1 ]; then
 mkdir -p ${BOOGIE_DIR}
 
 # Get Boogie
-hg clone -r f59ad49fc3a4 https://hg.codeplex.com/boogie ${BOOGIE_DIR}
+hg clone -r 661c32e8d5ca https://hg.codeplex.com/boogie ${BOOGIE_DIR}
 
 # Build Boogie
 cd ${BOOGIE_DIR}/Source
@@ -154,7 +155,7 @@ mkdir -p ${CORRAL_DIR}
 # Get Corral
 git clone https://git01.codeplex.com/corral ${CORRAL_DIR}
 cd ${CORRAL_DIR}
-git checkout 9311d7273384
+git checkout df4d2e2ace82
 
 # Build Corral
 cd ${CORRAL_DIR}/references