Skip to content

Commit edcbefa

Browse files
smowtonsmowton
committed
Merge commit 'f01d07a394ed0304c910e7c0527bbc5eaeb5ed52' as 'cbmc'
0 parents  commit edcbefa

File tree

6,685 files changed

+2653120
-0
lines changed

Some content is hidden

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

6,685 files changed

+2653120
-0
lines changed

‎.editorconfig

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
root = true
2+
3+
[*]
4+
charset = utf-8
5+
6+
indent_style = space
7+
indent_size = 2
8+
9+
trim_trailing_whitespace = true
10+
11+
max_line_length = 80
12+
end_of_line = lf
13+
insert_final_newline = true
14+
15+
[*patch]
16+
# Trailing spaces are significant in patch files
17+
trim_trailing_whitespace = false

‎.gitattributes

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
*.cpp text
2+
*.c text
3+
*.h text
4+
*.y text
5+
*.tex text
6+
*.shtml text
7+
*.html text
8+
*.css text
9+
*.inc text
10+
test.desc text
11+
Makefile text

‎.githooks/pre-commit

+51
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
#!/bin/bash
2+
# Runs scripts/cpplint.py on the modified files
3+
# Based on https://github.com/s0enke/git-hooks/
4+
#
5+
# @author Peter Schrammel <[email protected]>
6+
7+
gitRoot="$(dirname $0)/../.."
8+
9+
# this is the magic:
10+
# retrieve all files in staging area that are added, modified or renamed
11+
# but no deletions etc
12+
files=$(git diff-index --name-only --cached --diff-filter=ACMR HEAD -- )
13+
14+
if [ "$files" == "" ]; then
15+
exit 0
16+
fi
17+
18+
# create temporary copy of staging area and delete upon exit
19+
cleanup()
20+
{
21+
rm -rf $tmpStaging
22+
}
23+
24+
trap cleanup EXIT
25+
26+
tmpStaging=$(mktemp -d)
27+
touch $tmpStaging/.git
28+
29+
# Copy contents of staged version of files to temporary staging area
30+
# because we only want the staged version that will be commited and not
31+
# the version in the working directory
32+
stagedFiles=""
33+
for file in $files
34+
do
35+
id=$(git diff-index --cached HEAD $file | cut -d " " -f4)
36+
37+
# create staged version of file in temporary staging area with the same
38+
# path as the original file
39+
mkdir -p "$tmpStaging/$(dirname $file)"
40+
git cat-file blob $id > "$tmpStaging/$file"
41+
stagedFiles="$stagedFiles $tmpStaging/$file"
42+
done
43+
44+
output=$(cd $gitRoot; scripts/cpplint.py $stagedFiles 2>&1)
45+
retval=$?
46+
47+
if [ $retval -ne 0 ]
48+
then
49+
echo "$output"
50+
exit 1
51+
fi

‎.gitignore

+118
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
1+
# Local files generated by IDEs
2+
.vs/*
3+
.vscode/*
4+
~AutoRecover.*
5+
*.sln
6+
*.vcxproj*
7+
scripts/__pycache__/*
8+
src/goto-analyzer/taint_driver_scripts/.idea/*
9+
/*.config
10+
/*.creator
11+
/*.creator.user
12+
/*.files
13+
/*.includes
14+
15+
# compilation files
16+
*.lo
17+
*.od
18+
*.d
19+
*.o
20+
*.obj
21+
*.a
22+
*.lib
23+
src/ansi-c/arm_builtin_headers.inc
24+
src/ansi-c/clang_builtin_headers.inc
25+
src/ansi-c/cprover_library.inc
26+
src/ansi-c/cw_builtin_headers.inc
27+
src/ansi-c/gcc_builtin_headers_alpha.inc
28+
src/ansi-c/gcc_builtin_headers_arm.inc
29+
src/ansi-c/gcc_builtin_headers_generic.inc
30+
src/ansi-c/gcc_builtin_headers_ia32-2.inc
31+
src/ansi-c/gcc_builtin_headers_ia32-3.inc
32+
src/ansi-c/gcc_builtin_headers_ia32-4.inc
33+
src/ansi-c/gcc_builtin_headers_ia32.inc
34+
src/ansi-c/gcc_builtin_headers_math.inc
35+
src/ansi-c/gcc_builtin_headers_mem_string.inc
36+
src/ansi-c/gcc_builtin_headers_omp.inc
37+
src/ansi-c/gcc_builtin_headers_tm.inc
38+
src/ansi-c/gcc_builtin_headers_mips.inc
39+
src/ansi-c/gcc_builtin_headers_power.inc
40+
src/ansi-c/gcc_builtin_headers_ubsan.inc
41+
42+
# regression/test files
43+
*.out
44+
regression/**/tests.log
45+
regression/**/*.gb
46+
regression/**/*.smt2
47+
48+
# regression/coverage file
49+
/regression/coverage_**
50+
51+
# files stored by editors
52+
*~
53+
54+
# libs downloaded by make [name]-download
55+
libzip/
56+
zlib/
57+
minisat*/
58+
glucose-syrup/
59+
boost-include/
60+
61+
# flex/bison generated files
62+
src/ansi-c/ansi_c_lex.yy.cpp
63+
src/ansi-c/ansi_c_y.output
64+
src/ansi-c/ansi_c_y.tab.cpp
65+
src/ansi-c/ansi_c_y.tab.h
66+
src/assembler/assembler_lex.yy.cpp
67+
src/jsil/jsil_lex.yy.cpp
68+
src/jsil/jsil_y.output
69+
src/jsil/jsil_y.tab.cpp
70+
src/jsil/jsil_y.tab.h
71+
src/json/json_lex.yy.cpp
72+
src/json/json_y.output
73+
src/json/json_y.tab.cpp
74+
src/json/json_y.tab.h
75+
src/xmllang/xml_lex.yy.cpp
76+
src/xmllang/xml_y.output
77+
src/xmllang/xml_y.tab.cpp
78+
src/xmllang/xml_y.tab.h
79+
src/memory-models/mm_lex.yy.cpp
80+
src/memory-models/mm_y.output
81+
src/memory-models/mm_y.tab.cpp
82+
src/memory-models/mm_y.tab.h
83+
84+
# binaries
85+
src/cbmc/cbmc
86+
src/cbmc/cbmc.exe
87+
src/cegis/cegis
88+
src/cegis/cegis.exe
89+
src/goto-analyzer/goto-analyzer
90+
src/goto-analyzer/goto-analyzer.exe
91+
src/goto-cc/goto-cc
92+
src/goto-cc/goto-cc.exe
93+
src/goto-cc/goto-cl.exe
94+
src/goto-instrument/goto-instrument
95+
src/goto-instrument/goto-instrument.exe
96+
src/musketeer/musketeer
97+
src/musketeer/musketeer.exe
98+
src/symex/symex
99+
src/symex/symex.exe
100+
src/goto-diff/goto-diff
101+
src/goto-diff/goto-diff.exe
102+
src/clobber/clobber
103+
src/clobber/clobber.exe
104+
src/big-int/test-bigint
105+
src/big-int/test-bigint.exe
106+
107+
# build tools
108+
src/ansi-c/file_converter
109+
src/ansi-c/file_converter.exe
110+
src/ansi-c/library/converter
111+
src/ansi-c/library/converter.exe
112+
src/util/irep_ids_convert
113+
src/util/irep_ids_convert.exe
114+
115+
*.pyc
116+
117+
# auto generated documentation
118+
doc/html/

‎.travis.yml

+171
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,171 @@
1+
language: cpp
2+
3+
matrix:
4+
include:
5+
6+
# Alpine Linux with musl-libc using g++
7+
- os: linux
8+
sudo: required
9+
compiler: gcc
10+
cache: ccache
11+
services:
12+
- docker
13+
before_install:
14+
- docker pull diffblue/cbmc-builder:alpine-0.0.1
15+
env:
16+
- PRE_COMMAND="docker run -v ${TRAVIS_BUILD_DIR}:/cbmc -v ${HOME}/.ccache:/root/.ccache diffblue/cbmc-builder:alpine-0.0.1"
17+
- COMPILER="ccache g++"
18+
19+
# OS X using g++
20+
- os: osx
21+
sudo: false
22+
compiler: gcc
23+
cache: ccache
24+
before_install:
25+
#we create symlink to non-ccache gcc, to be used in tests
26+
- mkdir bin ; ln -s /usr/bin/gcc bin/gcc
27+
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
28+
- export PATH=/usr/local/opt/ccache/libexec:$PATH
29+
- ccache -M 1G
30+
env: COMPILER=g++
31+
32+
# OS X using clang++
33+
- os: osx
34+
sudo: false
35+
compiler: clang
36+
cache: ccache
37+
before_install:
38+
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
39+
- export PATH=/usr/local/opt/ccache/libexec:$PATH
40+
- ccache -M 1G
41+
env:
42+
- COMPILER="ccache clang++ -Qunused-arguments -fcolor-diagnostics"
43+
- CCACHE_CPP2=yes
44+
45+
# Ubuntu Linux with glibc using g++-5
46+
- os: linux
47+
sudo: false
48+
compiler: gcc
49+
cache: ccache
50+
addons:
51+
apt:
52+
sources:
53+
- ubuntu-toolchain-r-test
54+
packages:
55+
- libwww-perl
56+
- g++-5
57+
- libubsan0
58+
before_install:
59+
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
60+
# env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
61+
env: COMPILER="g++-5"
62+
63+
# Ubuntu Linux with glibc using g++-5, debug mode
64+
- os: linux
65+
sudo: false
66+
compiler: gcc
67+
cache: ccache
68+
addons:
69+
apt:
70+
sources:
71+
- ubuntu-toolchain-r-test
72+
packages:
73+
- libwww-perl
74+
- g++-5
75+
- libubsan0
76+
before_install:
77+
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
78+
# env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
79+
env:
80+
- COMPILER="g++-5"
81+
- EXTRA_CXXFLAGS="-DDEBUG"
82+
script: echo "Not running any tests for a debug build."
83+
84+
# Ubuntu Linux with glibc using clang++-3.7
85+
- os: linux
86+
sudo: false
87+
compiler: clang
88+
cache: ccache
89+
addons:
90+
apt:
91+
sources:
92+
- ubuntu-toolchain-r-test
93+
- llvm-toolchain-precise-3.7
94+
packages:
95+
- libwww-perl
96+
- clang-3.7
97+
- libstdc++-5-dev
98+
- libubsan0
99+
before_install:
100+
- mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
101+
- export CCACHE_CPP2=yes
102+
# env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
103+
env:
104+
- COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
105+
- CCACHE_CPP2=yes
106+
107+
# Ubuntu Linux with glibc using clang++-3.7, debug mode
108+
- os: linux
109+
sudo: false
110+
compiler: clang
111+
cache: ccache
112+
addons:
113+
apt:
114+
sources:
115+
- ubuntu-toolchain-r-test
116+
- llvm-toolchain-precise-3.7
117+
packages:
118+
- libwww-perl
119+
- clang-3.7
120+
- libstdc++-5-dev
121+
- libubsan0
122+
before_install:
123+
- mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
124+
- export CCACHE_CPP2=yes
125+
# env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
126+
env:
127+
- COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
128+
- CCACHE_CPP2=yes
129+
- EXTRA_CXXFLAGS="-DDEBUG"
130+
script: echo "Not running any tests for a debug build."
131+
132+
- env: NAME="CPP-LINT"
133+
install:
134+
script: scripts/travis_lint.sh
135+
before_cache:
136+
137+
- env: NAME="DOXYGEN-CHECK"
138+
addons:
139+
apt:
140+
packages:
141+
- doxygen
142+
install:
143+
script: scripts/travis_doxygen.sh
144+
before_cache:
145+
146+
allow_failures:
147+
- env: NAME="CPP-LINT"
148+
install:
149+
script: scripts/travis_lint.sh
150+
before_cache:
151+
152+
install:
153+
- COMMAND="make -C src minisat2-download" &&
154+
eval ${PRE_COMMAND} ${COMMAND}
155+
- COMMAND="make -C src boost-download" &&
156+
eval ${PRE_COMMAND} ${COMMAND}
157+
- COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g -DUSE_BOOST $EXTRA_CXXFLAGS\" -j2" &&
158+
eval ${PRE_COMMAND} ${COMMAND}
159+
- COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 clobber.dir memory-models.dir musketeer.dir" &&
160+
eval ${PRE_COMMAND} ${COMMAND}
161+
162+
script:
163+
- if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
164+
COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\"" &&
165+
eval ${PRE_COMMAND} ${COMMAND}
166+
- COMMAND="make -C unit CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
167+
eval ${PRE_COMMAND} ${COMMAND}
168+
- COMMAND="make -C unit test" && eval ${PRE_COMMAND} ${COMMAND}
169+
170+
before_cache:
171+
- ccache -s

0 commit comments

Comments
 (0)