Skip to content

Commit b0958c8

Browse files
zvonimirzvonimir
committed
Merge branch 'release-1.4.1'
2 parents 6316767 + 9200df5 commit b0958c8

File tree

146 files changed

+2660
-10503
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

146 files changed

+2660
-10503
lines changed

‎CMakeLists.txt‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -179,9 +179,9 @@ INSTALL(FILES ${CMAKE_CURRENT_SOURCE_DIR}/bin/boogie
179179
${CMAKE_CURRENT_SOURCE_DIR}/bin/corral
180180
${CMAKE_CURRENT_SOURCE_DIR}/bin/llvm2bpl.py
181181
${CMAKE_CURRENT_SOURCE_DIR}/bin/smackgen.py
182-
${CMAKE_CURRENT_SOURCE_DIR}/bin/smack-verify.py
182+
${CMAKE_CURRENT_SOURCE_DIR}/bin/smackverify.py
183183
PERMISSIONS OWNER_EXECUTE OWNER_WRITE OWNER_READ
184184
GROUP_EXECUTE GROUP_READ WORLD_EXECUTE WORLD_READ
185185
DESTINATION bin
186186
)
187-
187+

‎LICENSE‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
The MIT License
22

3-
Copyright (c) 2008-2013 Zvonimir Rakamaric (zvonimir@cs.utah.edu),
3+
Copyright (c) 2008-2014 Zvonimir Rakamaric (zvonimir@cs.utah.edu),
44
Michael Emmi (michael.emmi@gmail.com)
55

66
Permission is hereby granted, free of charge, to any person obtaining a copy

‎Makefile.common.in‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
# Set the name of the project here
22
PROJECT_NAME := smack
3-
PROJ_VERSION := 1.4.0
3+
PROJ_VERSION := 1.4.1
44

55
# Set this variable to the top of the LLVM source tree.
66
LLVM_SRC_ROOT = @LLVM_SRC@

‎Makefile.llvm.config.in‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ PROJ_SRC_DIR := $(call realpath, $(PROJ_SRC_ROOT)/$(patsubst $(PROJ_OBJ_ROOT)%,%
5959
prefix := $(PROJ_INSTALL_ROOT)
6060
PROJ_prefix := $(prefix)
6161
ifndef PROJ_VERSION
62-
PROJ_VERSION := 1.4.0
62+
PROJ_VERSION := 1.4.1
6363
endif
6464

6565
PROJ_bindir := $(PROJ_prefix)/bin

‎README.md‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,9 @@ experience verifying C language programs is encouraging: SMACK is competitive
1111
in SV-COMP benchmarks, is able to translate large programs (100 KLOC), and is
1212
used in several verification research prototypes.
1313

14+
*Please drop us a note if using SMACK in your research or teaching. We would
15+
love to learn more about your experience.*
16+
1417
## A Quick Demo
1518

1619
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.
4952
While SMACK is designed to be a *modular* verifier, for our convenience, this
5053
whole process has also been wrapped into a single command in SMACK:
5154

52-
smack-verify.py simple.c -o simple.bpl
55+
smackverify.py simple.c -o simple.bpl
5356

5457
which equally reports that the program `simple.c` is verified.
5558

‎autoconf/configure.ac‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
dnl **************************************************************************
22
dnl * Initialize
33
dnl **************************************************************************
4-
AC_INIT([[SMACK]],[[1.4.0]],[smack-dev@googlegroups.com],[smack],[http://github.com/smackers/smack])
4+
AC_INIT([[SMACK]],[[1.4.1]],[smack-dev@googlegroups.com],[smack],[http://github.com/smackers/smack])
55

66
dnl Identify where LLVM source tree is
77
LLVM_SRC_ROOT="../.."

‎bin/build-linux-cmake.sh‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@ sudo apt-get install -y git
5555
sudo apt-get install -y mercurial
5656
sudo apt-get install -y autoconf
5757
sudo apt-get install -y wget
58+
sudo apt-get install -y unzip
5859

5960
fi
6061

@@ -96,7 +97,7 @@ sudo make install
9697

9798
# Install libgdiplus
9899
sudo apt-get install -y libglib2.0-dev libfontconfig1-dev libfreetype6-dev libxrender-dev
99-
sudo apt-get install -y libtiff-dev libjpeg-dev libgif-dev libpng-dev
100+
sudo apt-get install -y libtiff-dev libjpeg-dev libgif-dev libpng-dev libcairo2-dev
100101
cd ${MONO_DIR}
101102
git clone git://github.com/mono/libgdiplus.git
102103
cd libgdiplus
@@ -145,7 +146,7 @@ if [ ${INSTALL_BOOGIE} -eq 1 ]; then
145146
mkdir -p ${BOOGIE_DIR}
146147

147148
# Get Boogie
148-
hg clone -r f59ad49fc3a4 https://hg.codeplex.com/boogie ${BOOGIE_DIR}
149+
hg clone -r 661c32e8d5ca https://hg.codeplex.com/boogie ${BOOGIE_DIR}
149150

150151
# Build Boogie
151152
cd ${BOOGIE_DIR}/Source
@@ -167,7 +168,7 @@ mkdir -p ${CORRAL_DIR}
167168
# Get Corral
168169
git clone https://git01.codeplex.com/corral ${CORRAL_DIR}
169170
cd ${CORRAL_DIR}
170-
git checkout 9311d7273384
171+
git checkout df4d2e2ace82
171172

172173
# Build Corral
173174
cd ${CORRAL_DIR}/references

‎bin/build-linux-ubuntu_1404.sh‎

Lines changed: 225 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,225 @@
1+
#!/bin/bash
2+
3+
################################################################################
4+
#
5+
# Builds and installs SMACK in BASE_DIR (see shell var below in settings).
6+
#
7+
# Requirements (see "Install required packages" below):
8+
# - git
9+
# - mercurial
10+
# - python
11+
# - gcc
12+
# - g++
13+
# - make
14+
# - autoconf
15+
# - mono
16+
#
17+
################################################################################
18+
19+
# Exit on error
20+
set -e
21+
22+
################################################################################
23+
24+
# Settings
25+
26+
# Change this to the desired path (default uses working-dir/smack-project)
27+
BASE_DIR=`pwd`/smack-project
28+
29+
# Set these flags to control various installation options
30+
INSTALL_PACKAGES=1
31+
INSTALL_Z3=1
32+
INSTALL_BOOGIE=1
33+
INSTALL_CORRAL=1
34+
INSTALL_LLVM=1
35+
INSTALL_SMACK=1
36+
37+
# Other dirs
38+
Z3_DIR="${BASE_DIR}/z3"
39+
BOOGIE_DIR="${BASE_DIR}/boogie"
40+
CORRAL_DIR="${BASE_DIR}/corral"
41+
LLVM_DIR="${BASE_DIR}/llvm"
42+
SMACK_DIR="${BASE_DIR}/smack"
43+
44+
################################################################################
45+
46+
# Install required packages
47+
48+
if [ ${INSTALL_PACKAGES} -eq 1 ]; then
49+
50+
sudo apt-get install -y g++
51+
sudo apt-get install -y git
52+
sudo apt-get install -y mercurial
53+
sudo apt-get install -y autoconf
54+
sudo apt-get install -y wget
55+
sudo apt-get install -y unzip
56+
sudo apt-get install -y monodevelop
57+
58+
fi
59+
60+
################################################################################
61+
62+
# Set up base directory for everything
63+
mkdir -p ${BASE_DIR}
64+
cd ${BASE_DIR}
65+
66+
################################################################################
67+
68+
# Z3
69+
70+
if [ ${INSTALL_Z3} -eq 1 ]; then
71+
72+
mkdir -p ${Z3_DIR}/src
73+
mkdir -p ${Z3_DIR}/install
74+
75+
# Get Z3
76+
cd ${Z3_DIR}/src/
77+
wget "http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx?ProjectName=z3&changeSetId=89c1785b73225a1b363c0e485f854613121b70a7"
78+
unzip -o SourceControlFileDownload*
79+
rm -f SourceControlFileDownload*
80+
81+
# Configure Z3 and build
82+
cd ${Z3_DIR}/src/
83+
autoconf
84+
./configure --prefix=${Z3_DIR}/install
85+
python scripts/mk_make.py
86+
cd build
87+
make
88+
sudo make install
89+
90+
cd ${BASE_DIR}
91+
92+
fi
93+
94+
################################################################################
95+
96+
# Boogie
97+
98+
if [ ${INSTALL_BOOGIE} -eq 1 ]; then
99+
100+
mkdir -p ${BOOGIE_DIR}
101+
102+
# Get Boogie
103+
hg clone -r 661c32e8d5ca https://hg.codeplex.com/boogie ${BOOGIE_DIR}
104+
105+
# Build Boogie
106+
cd ${BOOGIE_DIR}/Source
107+
xbuild Boogie.sln
108+
ln -s ${Z3_DIR}/install/bin/z3 ${BOOGIE_DIR}/Binaries/z3.exe
109+
110+
cd ${BASE_DIR}
111+
112+
fi
113+
114+
################################################################################
115+
116+
# Corral
117+
118+
if [ ${INSTALL_CORRAL} -eq 1 ]; then
119+
120+
mkdir -p ${CORRAL_DIR}
121+
122+
# Get Corral
123+
git clone https://git01.codeplex.com/corral ${CORRAL_DIR}
124+
cd ${CORRAL_DIR}
125+
git checkout df4d2e2ace82
126+
127+
# Build Corral
128+
cd ${CORRAL_DIR}/references
129+
130+
cp ${BOOGIE_DIR}/Binaries/AbsInt.dll .
131+
cp ${BOOGIE_DIR}/Binaries/Basetypes.dll .
132+
cp ${BOOGIE_DIR}/Binaries/CodeContractsExtender.dll .
133+
cp ${BOOGIE_DIR}/Binaries/Concurrency.dll .
134+
cp ${BOOGIE_DIR}/Binaries/Core.dll .
135+
cp ${BOOGIE_DIR}/Binaries/ExecutionEngine.dll .
136+
cp ${BOOGIE_DIR}/Binaries/Graph.dll .
137+
cp ${BOOGIE_DIR}/Binaries/Houdini.dll .
138+
cp ${BOOGIE_DIR}/Binaries/Model.dll .
139+
cp ${BOOGIE_DIR}/Binaries/ParserHelper.dll .
140+
cp ${BOOGIE_DIR}/Binaries/Provers.SMTLib.dll .
141+
cp ${BOOGIE_DIR}/Binaries/VCExpr.dll .
142+
cp ${BOOGIE_DIR}/Binaries/VCGeneration.dll .
143+
cp ${BOOGIE_DIR}/Binaries/Boogie.exe .
144+
cp ${BOOGIE_DIR}/Binaries/BVD.exe .
145+
cp ${BOOGIE_DIR}/Binaries/Doomed.dll .
146+
cp ${BOOGIE_DIR}/Binaries/Predication.dll .
147+
148+
cd ${CORRAL_DIR}
149+
xbuild cba.sln
150+
ln -s ${Z3_DIR}/install/bin/z3 ${CORRAL_DIR}/bin/Debug/z3.exe
151+
152+
cd ${BASE_DIR}
153+
154+
fi
155+
156+
################################################################################
157+
158+
# LLVM
159+
160+
if [ ${INSTALL_LLVM} -eq 1 ]; then
161+
162+
mkdir -p ${LLVM_DIR}/src
163+
mkdir -p ${LLVM_DIR}/build
164+
mkdir -p ${LLVM_DIR}/install
165+
166+
# Get llvm and extract
167+
wget http://llvm.org/releases/3.4/llvm-3.4.src.tar.gz
168+
wget http://llvm.org/releases/3.4/clang-3.4.src.tar.gz
169+
wget http://llvm.org/releases/3.4/compiler-rt-3.4.src.tar.gz
170+
171+
tar -C ${LLVM_DIR}/src -xzvf llvm-3.4.src.tar.gz --strip 1
172+
mkdir -p ${LLVM_DIR}/src/tools/clang
173+
tar -C ${LLVM_DIR}/src/tools/clang -xzvf clang-3.4.src.tar.gz --strip 1
174+
mkdir -p ${LLVM_DIR}/src/projects/compiler-rt
175+
tar -C ${LLVM_DIR}/src/projects/compiler-rt -xzvf compiler-rt-3.4.src.tar.gz --strip 1
176+
177+
# Configure llvm and build
178+
cd ${LLVM_DIR}/build/
179+
${LLVM_DIR}/src/configure --prefix=${LLVM_DIR}/install --enable-optimized
180+
make
181+
make install
182+
183+
cd ${BASE_DIR}
184+
185+
fi
186+
187+
################################################################################
188+
189+
# SMACK
190+
191+
if [ ${INSTALL_SMACK} -eq 1 ]; then
192+
193+
mkdir -p ${SMACK_DIR}/src
194+
mkdir -p ${SMACK_DIR}/build
195+
mkdir -p ${SMACK_DIR}/install
196+
197+
# Get SMACK
198+
git clone git://github.com/smackers/smack.git ${SMACK_DIR}/src/
199+
200+
# Configure SMACK and build
201+
cd ${SMACK_DIR}/build/
202+
${SMACK_DIR}/src/configure --with-llvmsrc=${LLVM_DIR}/src --with-llvmobj=${LLVM_DIR}/build --prefix=${SMACK_DIR}/install --enable-optimized
203+
make
204+
make install
205+
206+
cd ${BASE_DIR}
207+
208+
# Set required paths and environment variables
209+
export BOOGIE="mono ${BOOGIE_DIR}/Binaries/Boogie.exe"
210+
export CORRAL="mono ${CORRAL_DIR}/bin/Debug/corral.exe"
211+
export PATH=${LLVM_DIR}/install/bin:$PATH
212+
export PATH=${SMACK_DIR}/install/bin:$PATH
213+
214+
# Run SMACK regressions
215+
cd ${SMACK_DIR}/src/test
216+
make
217+
./regtest.py
218+
./regtest-corral.py
219+
220+
cd ${BASE_DIR}
221+
222+
fi
223+
224+
################################################################################
225+

‎bin/build-linux.sh‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,7 @@ sudo apt-get install -y git
5454
sudo apt-get install -y mercurial
5555
sudo apt-get install -y autoconf
5656
sudo apt-get install -y wget
57+
sudo apt-get install -y unzip
5758

5859
fi
5960

@@ -83,7 +84,7 @@ sudo make install
8384

8485
# Install libgdiplus
8586
sudo apt-get install -y libglib2.0-dev libfontconfig1-dev libfreetype6-dev libxrender-dev
86-
sudo apt-get install -y libtiff-dev libjpeg-dev libgif-dev libpng-dev
87+
sudo apt-get install -y libtiff-dev libjpeg-dev libgif-dev libpng-dev libcairo2-dev
8788
cd ${MONO_DIR}
8889
git clone git://github.com/mono/libgdiplus.git
8990
cd libgdiplus
@@ -132,7 +133,7 @@ if [ ${INSTALL_BOOGIE} -eq 1 ]; then
132133
mkdir -p ${BOOGIE_DIR}
133134

134135
# Get Boogie
135-
hg clone -r f59ad49fc3a4 https://hg.codeplex.com/boogie ${BOOGIE_DIR}
136+
hg clone -r 661c32e8d5ca https://hg.codeplex.com/boogie ${BOOGIE_DIR}
136137

137138
# Build Boogie
138139
cd ${BOOGIE_DIR}/Source
@@ -154,7 +155,7 @@ mkdir -p ${CORRAL_DIR}
154155
# Get Corral
155156
git clone https://git01.codeplex.com/corral ${CORRAL_DIR}
156157
cd ${CORRAL_DIR}
157-
git checkout 9311d7273384
158+
git checkout df4d2e2ace82
158159

159160
# Build Corral
160161
cd ${CORRAL_DIR}/references

0 commit comments

Comments
 (0)