Skip to content

Commit e41b229

Browse files
committed
Merge branch 'release-2.5.0'
2 parents 212bbdb + c77b8ff commit e41b229

File tree

261 files changed

+4994
-2909
lines changed

Some content is hidden

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

261 files changed

+4994
-2909
lines changed

.travis.yml

Lines changed: 26 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -9,68 +9,70 @@ addons:
99
- cmake
1010
- python3-yaml
1111
- python3-psutil
12+
- python3-pip
1213
- unzip
13-
- libz-dev
14-
- libedit-dev
14+
- ninja-build
1515
- libboost-all-dev
1616

17-
cache:
18-
directories:
19-
- $HOME/build/smackers/boogie
20-
- $HOME/build/smackers/corral
21-
- $HOME/build/smackers/symbooglix
22-
- $HOME/build/smackers/lockpwn
23-
2417
env:
2518
global:
2619
- COMPILER_NAME=clang COMPILER=clang++ CXX=clang++ CC=clang
2720
jobs:
2821
- TRAVIS_ENV="--exhaustive --folder=c/basic"
2922
- TRAVIS_ENV="--exhaustive --folder=c/data"
3023
- TRAVIS_ENV="--exhaustive --folder=c/ntdrivers-simplified"
24+
- TRAVIS_ENV="--exhaustive --folder=c/ntdrivers"
3125
- TRAVIS_ENV="--exhaustive --folder=c/bits"
3226
- TRAVIS_ENV="--exhaustive --folder=c/float"
3327
- TRAVIS_ENV="--exhaustive --folder=c/locks"
3428
- TRAVIS_ENV="--exhaustive --folder=c/contracts"
3529
- TRAVIS_ENV="--exhaustive --folder=c/simd"
3630
- TRAVIS_ENV="--exhaustive --folder=c/memory-safety"
3731
- TRAVIS_ENV="--exhaustive --folder=c/pthread"
32+
- TRAVIS_ENV="--exhaustive --folder=c/pthread_extras"
3833
- TRAVIS_ENV="--exhaustive --folder=c/strings"
3934
- TRAVIS_ENV="--exhaustive --folder=c/special"
35+
- TRAVIS_ENV="--exhaustive --folder=rust/array --languages=rust"
4036
- TRAVIS_ENV="--exhaustive --folder=rust/basic --languages=rust"
37+
- TRAVIS_ENV="--exhaustive --folder=rust/box --languages=rust"
4138
- TRAVIS_ENV="--exhaustive --folder=rust/functions --languages=rust"
4239
- TRAVIS_ENV="--exhaustive --folder=rust/generics --languages=rust"
4340
- TRAVIS_ENV="--exhaustive --folder=rust/loops --languages=rust"
41+
- TRAVIS_ENV="--exhaustive --folder=rust/panic --languages=rust"
4442
- TRAVIS_ENV="--exhaustive --folder=rust/recursion --languages=rust"
4543
- TRAVIS_ENV="--exhaustive --folder=rust/structures --languages=rust"
4644
- TRAVIS_ENV="--exhaustive --folder=rust/vector --languages=rust"
4745

4846
before_install:
47+
- sudo rm -rf /usr/local/clang-7.0.0
48+
49+
install:
50+
- source ./bin/versions
4951
- wget -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
50-
- sudo add-apt-repository "deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-8 main"
51-
- sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF
52+
- sudo add-apt-repository "deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-${LLVM_SHORT_VERSION} main"
53+
- wget -q https://packages.microsoft.com/config/ubuntu/18.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb
54+
- sudo dpkg -i packages-microsoft-prod.deb
5255
- sudo apt-get install -y apt-transport-https
53-
- echo "deb https://download.mono-project.com/repo/ubuntu stable-bionic main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
5456
- sudo apt-get update
57+
- sudo apt-get install -y clang-${LLVM_SHORT_VERSION} clang-format-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev dotnet-sdk-3.1
58+
- pip3 install -U flake8
59+
- sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_SHORT_VERSION} 20
60+
- sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-${LLVM_SHORT_VERSION} 20
61+
- sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-${LLVM_SHORT_VERSION} 20
62+
- sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-${LLVM_SHORT_VERSION} 20
63+
- sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-${LLVM_SHORT_VERSION} 20
64+
- sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-${LLVM_SHORT_VERSION} 20
5565

56-
install:
57-
- sudo apt-get install -y clang-8 clang-format-8 llvm-8-dev mono-complete ca-certificates-mono ninja-build
58-
- sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-8 20
59-
- sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-8 20
60-
- sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-8 20
61-
- sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-8 20
62-
- sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-8 20
63-
- sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-8 20
64-
- sudo pip install pyyaml psutil
65-
66-
script:
67-
- python --version
66+
before_script:
6867
- python3 --version
6968
- $CXX --version
7069
- $CC --version
7170
- clang --version
7271
- clang++ --version
7372
- llvm-link --version
7473
- llvm-config --version
74+
75+
script:
7576
- ./format/run-clang-format.py -e test/c/basic/transform-out.c -r lib/smack include/smack share/smack/include share/smack/lib test examples
77+
- flake8 test/regtest.py share/smack/ --extend-exclude share/smack/svcomp/,share/smack/reach.py
7678
- INSTALL_RUST=1 ./bin/build.sh

CMakeLists.txt

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,11 @@ cmake_minimum_required(VERSION 3.4.3)
66
project(smack)
77

88
if (NOT WIN32 OR MSYS OR CYGWIN)
9-
find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-8 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
9+
10+
file(STRINGS "bin/versions" LLVM_VERSION_STR REGEX "LLVM_SHORT_VERSION=[0-9]+")
11+
string(REGEX MATCH "[0-9]+" LLVM_SHORT_VERSION "${LLVM_VERSION_STR}")
12+
13+
find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-${LLVM_SHORT_VERSION} llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
1014

1115
if (LLVM_CONFIG_EXECUTABLE STREQUAL "LLVM_CONFIG_EXECUTABLE-NOTFOUND")
1216
message(FATAL_ERROR "llvm-config could not be found!")
@@ -112,6 +116,7 @@ add_library(smackTranslator STATIC
112116
include/smack/BplFilePrinter.h
113117
include/smack/BplPrinter.h
114118
include/smack/DSAWrapper.h
119+
include/smack/InitializePasses.h
115120
include/smack/Naming.h
116121
include/smack/Regions.h
117122
include/smack/SmackInstGenerator.h
@@ -167,7 +172,7 @@ if (Boost_FOUND)
167172
endif ()
168173
# We have to import LLVM's cmake definitions to build sea-dsa
169174
# Borrowed from sea-dsa's CMakeLists.txt
170-
find_package (LLVM 8.0.1 EXACT CONFIG)
175+
find_package (LLVM ${LLVM_SHORT_VERSION} CONFIG)
171176
list(APPEND CMAKE_MODULE_PATH "${LLVM_CMAKE_DIR}")
172177
include(AddLLVM)
173178
include(HandleLLVMOptions)
@@ -176,7 +181,7 @@ include(HandleLLVMOptions)
176181
# The following solution is from: https://stackoverflow.com/questions/30985215/passing-variables-down-to-subdirectory-only
177182
set(SMACK_BUILD_TYPE "${CMAKE_BUILD_TYPE}")
178183
set(CMAKE_BUILD_TYPE "Release")
179-
add_subdirectory(sea-dsa/src)
184+
add_subdirectory(sea-dsa/lib/seadsa)
180185
set(CMAKE_BUILD_TYPE ${SMACK_BUILD_TYPE})
181186

182187
target_link_libraries(smackTranslator ${LLVM_LIBS} ${LLVM_SYSTEM_LIBS} ${LLVM_LDFLAGS})

Doxyfile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
#---------------------------------------------------------------------------
66
DOXYFILE_ENCODING = UTF-8
77
PROJECT_NAME = smack
8-
PROJECT_NUMBER = 2.4.1
8+
PROJECT_NUMBER = 2.5.0
99
PROJECT_BRIEF = "A bounded software verifier."
1010
PROJECT_LOGO =
1111
OUTPUT_DIRECTORY = docs

LICENSE

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
The MIT License
22

3-
Copyright (c) 2008-2019 Zvonimir Rakamaric ([email protected]),
3+
Copyright (c) 2008-2020 Zvonimir Rakamaric ([email protected]),
44
Michael Emmi ([email protected])
5-
Modified work Copyright (c) 2013-2019 Marek Baranowski,
5+
Modified work Copyright (c) 2013-2020 Marek Baranowski,
66
Montgomery Carter,
77
Pantazis Deligiannis,
88
Jack J. Garzella,
@@ -44,10 +44,7 @@ licenses, and/or restrictions:
4444

4545
Program Directories License
4646
------- ----------- -------
47-
poolalloc include/assistDS lib/DSA/LICENSE
48-
include/dsa
49-
lib/AssistDS
50-
lib/DSA
47+
sea-dsa sea-dsa sea-dsa/license.txt
5148
run-clang-format format format/LICENSE
5249

5350
In addition, a binary distribution of SMACK contains at least the following

README.md

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
1-
| **master** | [![Build Status](https://travis-ci.com/smackers/smack.svg?branch=master)](https://travis-ci.com/smackers/smack) | **develop** | [![Build Status](https://travis-ci.com/smackers/smack.svg?branch=develop)](https://travis-ci.com/smackers/smack) |
2-
| --- | --- | --- | --- |
1+
2+
[![Build Status](https://travis-ci.com/smackers/smack.svg?branch=master)](https://travis-ci.com/smackers/smack)
3+
[![Build Status](https://travis-ci.com/smackers/smack.svg?branch=develop)](https://travis-ci.com/smackers/smack)
34

45
<img src="docs/smack-logo.png" width=400 alt="SMACK Logo" align="right">
56

@@ -47,10 +48,10 @@ See below for system requirements, installation, usage, and everything else.
4748

4849
### Acknowledgements
4950

50-
SMACK project is partially supported by NSF award CCF 1346756 and Microsoft
51-
Research SEIF award. We also rely on University of Utah's
52-
[Emulab](http://www.emulab.net/) infrastructure for extensive benchmarking of
53-
SMACK.
51+
SMACK project has been partially supported by funding from the National Science
52+
Foundation, VMware, and Microsoft Research. We also rely on University of
53+
Utah's [Emulab](http://www.emulab.net/) infrastructure for extensive
54+
benchmarking of SMACK.
5455

5556

5657
### Table of Contents

Vagrantfile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ Vagrant.configure(2) do |config|
2525
# opensuse_config.vm.box = "chef/opensuse-13.1"
2626
# end
2727

28-
config.vm.provision "shell", binary: true, inline: <<-SHELL
28+
config.vm.provision "shell", binary: true, privileged: false, inline: <<-SHELL
2929
apt-get update
3030
apt-get install -y software-properties-common
3131
cd /home/vagrant

0 commit comments

Comments
 (0)