Skip to content

Commit 8faef3b

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #818 from NathanJPhillips/security-scanner-support
Merge master into Security scanner support
2 parents cdce3fa + 9c06fba commit 8faef3b

File tree

541 files changed

+11865
-1432
lines changed

Some content is hidden

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

541 files changed

+11865
-1432
lines changed

‎.gitignore

-2
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,6 @@ src/ansi-c/gcc_builtin_headers_ia32-2.inc
3131
src/ansi-c/gcc_builtin_headers_ia32.inc
3232
src/ansi-c/gcc_builtin_headers_mips.inc
3333
src/ansi-c/gcc_builtin_headers_power.inc
34-
src/util/irep_ids.h
35-
src/util/irep_ids.inc
3634

3735
# regression/test files
3836
*.out

‎.travis.yml

+95-20
Original file line numberDiff line numberDiff line change
@@ -7,30 +7,46 @@ matrix:
77
- os: linux
88
sudo: required
99
compiler: gcc
10+
cache: ccache
1011
services:
1112
- docker
1213
before_install:
13-
- docker pull diffblue/cbmc-builder:alpine
14+
- docker pull diffblue/cbmc-builder:alpine-0.0.1
1415
env:
15-
- PRE_COMMAND="docker run -v ${TRAVIS_BUILD_DIR}:/cbmc diffblue/cbmc-builder:alpine"
16-
- COMPILER=g++
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++"
1718

1819
# OS X using g++
1920
- os: osx
2021
sudo: false
2122
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
2230
env: COMPILER=g++
2331

2432
# OS X using clang++
2533
- os: osx
2634
sudo: false
2735
compiler: clang
28-
env: 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
2944

3045
# Ubuntu Linux with glibc using g++-5
3146
- os: linux
3247
sudo: false
3348
compiler: gcc
49+
cache: ccache
3450
addons:
3551
apt:
3652
sources:
@@ -42,12 +58,57 @@ matrix:
4258
before_install:
4359
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
4460
# env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
45-
env: COMPILER=g++-5
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."
4683

4784
# Ubuntu Linux with glibc using clang++-3.7
4885
- os: linux
4986
sudo: false
5087
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
51112
addons:
52113
apt:
53114
sources:
@@ -60,25 +121,39 @@ matrix:
60121
- libubsan0
61122
before_install:
62123
- mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
124+
- export CCACHE_CPP2=yes
63125
# env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
64-
env: COMPILER=clang++-3.7
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."
65131

66132
- env: NAME="CPP-LINT"
67-
script: scripts/travis_lint.sh || true
133+
install:
134+
script: scripts/travis_lint.sh
135+
before_cache:
136+
137+
allow_failures:
138+
- env: NAME="CPP-LINT"
139+
install:
140+
script: scripts/travis_lint.sh
141+
before_cache:
142+
143+
install:
144+
- COMMAND="make -C src minisat2-download" &&
145+
eval ${PRE_COMMAND} ${COMMAND}
146+
- COMMAND="make -C src boost-download" &&
147+
eval ${PRE_COMMAND} ${COMMAND}
148+
- COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DUSE_BOOST $EXTRA_CXXFLAGS\" -j2" &&
149+
eval ${PRE_COMMAND} ${COMMAND}
150+
- COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir" &&
151+
eval ${PRE_COMMAND} ${COMMAND}
68152

69153
script:
70-
- if [ -L bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
71-
COMMAND="make -C src minisat2-download" &&
72-
eval ${PRE_COMMAND} ${COMMAND} &&
73-
COMMAND="make -C src boost-download" &&
74-
eval ${PRE_COMMAND} ${COMMAND} &&
75-
COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DUSE_BOOST\" -j2" &&
76-
eval ${PRE_COMMAND} ${COMMAND} &&
154+
- if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
77155
COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" &&
78-
eval ${PRE_COMMAND} ${COMMAND} &&
79-
COMMAND="make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir" &&
80-
eval ${PRE_COMMAND} ${COMMAND} &&
81-
COMMAND="make -C src clean" &&
82-
eval ${PRE_COMMAND} ${COMMAND} &&
83-
COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O0 -ggdb3 -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DDEBUG\" -j2" &&
84156
eval ${PRE_COMMAND} ${COMMAND}
157+
158+
before_cache:
159+
- ccache -s

‎CHANGELOG

+11
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,14 @@
1+
5.8
2+
===
3+
4+
* GOTO-INSTRUMENT: --reachability-slice can be used with --property to slice
5+
down to a single property only.
6+
* GOTO-INSTRUMENT: New option --list-calls-args
7+
* GOTO-INSTRUMENT: New option --print-path-lenghts
8+
* GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions
9+
* GOTO-INSTRUMENT: New option --undefined-function-is-assume-false
10+
11+
112
5.7
213
===
314

‎README.md

+4-2
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
[![Build Status][build_img]][travis]
1+
[![Build Status][travis_img]][travis] [![Build Status][appveyor_img]][appveyor]
22

33
[CProver Wiki](http://www.cprover.org/wiki)
44

@@ -19,5 +19,7 @@ License
1919
=======
2020
4-clause BSD license, see `LICENSE` file.
2121

22-
[build_img]: https://travis-ci.org/diffblue/cbmc.svg?branch=master
2322
[travis]: https://travis-ci.org/diffblue/cbmc
23+
[travis_img]: https://travis-ci.org/diffblue/cbmc.svg?branch=master
24+
[appveyor]: https://ci.appveyor.com/project/diffblue/cbmc/
25+
[appveyor_img]: https://ci.appveyor.com/api/projects/status/github/diffblue/cbmc?svg=true&branch=master

‎appveyor.yml

+110
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
version: 1.0.{build}
2+
image: Visual Studio 2013
3+
clone_depth: 50
4+
environment:
5+
BUILD_ENV: MSVC
6+
PATH: C:\projects\cbmc\deps\bin;%PATH%
7+
INCLUDE: C:\projects\cbmc\deps\include
8+
install:
9+
- ps: |
10+
#check if dependencies were copied from cache, if not, download them.
11+
if (!(Test-Path deps)) {
12+
md deps
13+
}
14+
cd deps
15+
if (!(Test-Path bin\bison.exe)) {
16+
& appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/bison-2.4.1-bin.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=JAPFzNPMJDI4IViAVlJAEc6l8aHB3k17NpZRdoWDMLbALaJNX88vfwocuezU1tfhyrSJxfo2fTK4rgP5OULkikJs7MBZI9ovp2V%2BMT6yg87KDdH9EIOlMgltGfbP%2BoZkwBY7kXb3W5puSlt4OTE%2Bw7CRlHF9MNqFXVBqVBfa%2BGw0gXDe5Jd9qV%2BvUXZzRuBl9ERSQkSD%2B%2B%2BxFo24FZoOeYkgBHJz03%2BHuIMnlmcLgneTB2aiZZU3%2B6UTPceUxLus9%2Bksb5UbqEVaVE06TIXl76VKwqAgXM2LWaNyeJDog%2BT%2BhjW4v4ypxh6mIBo5KRNXVLPc1MxSPFQB3ITlIXv9Zg%3D%3D"
17+
& 7z x bison-2.4.1-bin.zip
18+
}
19+
if (!(Test-Path bin\flex.exe)) {
20+
& appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/flex-2.5.4a-1-bin.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=WriP8S047Mmq271ZHWL0MCPGx1gEFsuc%2BKMmChoXhXFRkn0GlIgCxZEiOu52ke9fT1kAvycWXePNBFAyCHjpF%2BJkXCwisQ6FLIf3NL%2F92849YgQKdJkDUOcZ%2Bh82XVTwNBrljKIkExkak7QEyhOf3buTC1oeuatCUV5Ez42RZjgtRiJaqcFW6xLbhfuVONr39KxH5hGx%2FDUi2RRXPbgoKDwavc9s56NP1rNbWMTE6NdNHzJeaf43E%2BSMemlVO%2BhhIY6W0f%2FtaQ7fYF%2F6YaqxdQ0sB8W5DnG4Hb%2F0CyQlrTZpGDXGr301rV0M4WBkYLmfauq4IyJsBaR095tXGW%2BzmA%3D%3D"
21+
& 7z x flex-2.5.4a-1-bin.zip
22+
}
23+
if (!(Test-Path include\FlexLexer.h)) {
24+
& appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/flex-2.5.4a-1-lib.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=H%2FLeKGv2QqKAGDTP%2F6TYPhDzuL6K%2F5dFOt61HfYBm1vUWVUNmAYVGvUAcvnUqBnhEHwZgtc8vZt1H7k3W8azxCUc7l6ZhlCDbqQ6Mg2VhfpBaQMbL1V%2BjSq5ePpWcuLMBntKk2br38PF1NtiAwCCpRTRPptaYPeGs%2BOjAH%2BN8aIIxjvj45QAgt9mcg6dfBsyfj5fdJmpHRQFuJ7%2FnsG50fmN5JDvdvmBWloB6rjxVWaN4XO6VTWZFZ34JWFyOqgWNEw9aDN3HdsSuJ0Uz19AbdwZBIWe5Elrl71rRJjn1lijCknDB7D4sAmP33k71e%2BB0qvsNl1Shuh9FkY8Z6y05Q%3D%3D"
25+
& 7z x flex-2.5.4a-1-lib.zip
26+
}
27+
if (!(Test-Path bin\iconv.exe)) {
28+
& appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/libiconv-1.9.2-1-bin.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=sS3Y2lC1oWOhBDsL8C9ASuO4LOM%2BpB%2F8PwG5w5CdB9JnPfLqhb3FnA1zkkZJoSNuIYS3DM6CN2qxoWjpJbLEtVQe0PpxziQZjLpJw2MpxXdJiJHRDu8x9THgzwuZ3ze5BWHzPoCBQPdRkKzVPezf1HwptUsm3Y9c2jlWljQjhc8NVsI4iPmjEOwT8E%2BYpR5fsLs2GsRjuoyqKa%2Bi4JJ6MbpXVX1IgR4fzp1Li9SnE39ujHDb%2FyI3c96eCdVm1Oa6jNxzSJNfq%2FgOZM8BIxlR55a%2BtM3oBQhU0voEtDOABwuO7ZBay8dLt%2FG5vz1%2Bi%2FIlRLFxQfICaprPLzw6pXRm8Q%3D%3D"
29+
& 7z x libiconv-1.9.2-1-bin.zip
30+
}
31+
if (!(Test-Path bin\libintl3.dll)) {
32+
& appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/libintl-0.14.4-bin.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=lJViGr6bl%2F4i%2B6nIfeYChreq%2FKfgid9QqGSq7Ie%2FMG%2Fmr9nPyPUA%2BLtT7jn1ogunTzQLZP%2FNxVFcYqyd8gyuT%2Bn2MF80Ds4Whw4cRYnXPb2LZg4%2FiEqZV6wgBMIQfq5v2l3lAsglISVErOik%2BQAHec5gZe2%2BKaVjRnJnhPRziZkQyzF9Xdf2xsPi28hBaX4RQx8XqSLcY1kQpY13PDBZDi9lmdKHf0pBKu%2F0WXspmRAU02HtleMk6Zeg5vEDFcwoe8C3fb4vwtpwGwN9TX5ddaq56yUVn70zh%2BH2KgKIsRl26avnrCpeWF9M5lLck0ngaqFX84w%2BgxmZu40IVU%2Ff0A%3D%3D"
33+
& 7z x libintl-0.14.4-bin.zip
34+
}
35+
if (!(Test-Path bin\make.exe)) {
36+
& appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/make-3.81-bin.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=PRC97AWzJ2ZAyjEK4p7eCbA3RAEr8sTf8TUK5zoMBcrXPUHWYjnCwXRMnIxUUufBYjsAx8t1XnOQdlTuAPJYpcha%2FFJRlcxMmfQjNbpNEQFJuqEpA5c%2FGhFYxSD3a26vjpgReUW5MuQXeLeNh7PziLB0GP0sdRHN%2B1eDiHeCJWYNMYhrEY9BAkf5rXeRQWr1ZG0Hzq%2FxZEHceypx8xyaT%2BFzREYQOyKjGdre1QXtI%2FXo4ImA1xWt%2F8TnlGcAnCEaTltxuSRVB%2F7s1ShMr9KoagCb%2BjBWq6BgbcNGxyzyOZfi2Sjjo39mhudF9DNbKbkczes9Kp3ySgXmrXSWjIG4Iw%3D%3D"
37+
& 7z x make-3.81-bin.zip
38+
}
39+
if (!(Test-Path bin\regex2.dll)) {
40+
& appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/regex-2.7-bin.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=bXRvFV%2Be4Dpm8vzp%2F1bJWwgkERE6WakcPTBN57n9vNh0dr42jDTXv8JF%2BWCmTIb%2Fy4XzxYl0faggt3g6TqTLYn5UDVUBYx%2FMLmNVVNEv%2BaBlDd87UAZGLi6fkEV5oAP4W4FYsqEnKRDfGPOBoL7D7CuW9Kcxy3Moubxdl%2Bmes%2BMI%2FzWJ6BgLD3Oj04GyD42zLCYVtAzkeDAX0UADoh06ExhpTjI4BNnQ%2FhzSlPtPG7mon4q81%2F2tDNskKVJS466eR%2F8XV6H4QT3LoCkh6dxQ9%2B9ZnkWJplundRbiIlpj43vmdvjIChczl4jbAgL6zFj5Gz6u58uvCV%2FbOuyx3Sw1fg%3D%3D"
41+
& 7z x regex-2.7-bin.zip
42+
}
43+
if (!(Test-Path minisat2-2.2.1)) {
44+
& appveyor DownloadFile http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
45+
& 7z x minisat2_2.2.1.orig.tar.gz
46+
&7z x minisat2_2.2.1.orig.tar
47+
}
48+
cd ..
49+
50+
cache: deps
51+
52+
build_script:
53+
- cmd: |
54+
cp -r deps/minisat2-2.2.1 minisat-2.2.1
55+
patch -d minisat-2.2.1 -p1 < scripts/minisat-2.2.1-patch
56+
call "C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\vcvarsall.bat" x64
57+
sed -i "s/BUILD_ENV.*/BUILD_ENV = MSVC/" src/config.inc
58+
make -C src -j2
59+
60+
test_script:
61+
- cmd: |
62+
cd regression
63+
sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" ansi-c/Makefile
64+
sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" cpp/Makefile
65+
sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-instrument/chain.sh
66+
sed -i "15s/.*/$goto_cc $name.c/" goto-instrument/chain.sh
67+
sed -i "16i mv $name.exe $name.gb" goto-instrument/chain.sh
68+
sed -i "23s/.*/ $goto_cc ${name}-mod.c/" goto-instrument/chain.sh
69+
sed -i "24i mv ${name}-mod.exe $name-mod.gb" goto-instrument/chain.sh
70+
cat goto-instrument/chain.sh
71+
72+
sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-instrument-typedef/chain.sh || true
73+
sed -i "12s/.*/$GC $NAME.c --function fun/" goto-instrument-typedef/chain.sh || true
74+
sed -i "13i mv $NAME.exe $NAME.gb" goto-instrument-typedef/chain.sh || true
75+
cat goto-instrument-typedef/chain.sh || true
76+
77+
rem HACK disable failing tests
78+
rmdir /s /q ansi-c\Forward_Declaration2
79+
rmdir /s /q ansi-c\Incomplete_Type1
80+
rmdir /s /q ansi-c\Union_Padding1
81+
rmdir /s /q ansi-c\Universal_characters1
82+
rmdir /s /q ansi-c\function_return1
83+
rmdir /s /q ansi-c\gcc_attributes7
84+
rmdir /s /q ansi-c\struct6
85+
rmdir /s /q ansi-c\struct7
86+
rmdir /s /q cbmc\Malloc23
87+
rmdir /s /q cbmc\byte_update2
88+
rmdir /s /q cbmc\byte_update3
89+
rmdir /s /q cbmc\byte_update4
90+
rmdir /s /q cbmc\byte_update5
91+
rmdir /s /q cbmc\byte_update6
92+
rmdir /s /q cbmc\byte_update7
93+
rmdir /s /q cbmc\pipe1
94+
rmdir /s /q cbmc\unsigned___int128
95+
rmdir /s /q cpp\Decltype1
96+
rmdir /s /q cpp\Decltype2
97+
rmdir /s /q cpp\Function_Overloading1
98+
rmdir /s /q cpp\enum2
99+
rmdir /s /q cpp\enum7
100+
rmdir /s /q cpp\enum8
101+
rmdir /s /q cpp\nullptr1
102+
rmdir /s /q cpp\sizeof1
103+
rmdir /s /q cpp\static_assert1
104+
rmdir /s /q cbmc-java\VarLengthArrayTrace1
105+
rmdir /s /q cbmc-java\classpath1
106+
rmdir /s /q cbmc-java\jar-file3
107+
rmdir /s /q cbmc-java\tableswitch2
108+
rmdir /s /q goto-instrument\slice08
109+
110+
make test

‎regression/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ DIRS = ansi-c \
55
cbmc-java \
66
goto-analyzer \
77
goto-instrument \
8+
goto-instrument-typedef \
89
test-script \
910
# Empty last line
1011

‎regression/acceleration/Makefile

+2-2
Original file line numberDiff line numberDiff line change
@@ -14,5 +14,5 @@ show:
1414
done;
1515

1616
clean:
17-
rm -f tests.log
18-
rm -f */main.out
17+
$(RM) tests.log
18+
$(RM) */main.out

‎regression/acceleration/array_unsafe1/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
CORE
22
main.c
33
--no-unwinding-assertions
4-
54
^EXIT=10$
65
^SIGNAL=0$
76
^VERIFICATION FAILED$

‎regression/acceleration/array_unsafe2/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
CORE
22
main.c
33
--no-unwinding-assertions
4-
54
^EXIT=10$
65
^SIGNAL=0$
76
^VERIFICATION FAILED$

‎regression/acceleration/array_unsafe3/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
CORE
22
main.c
33
--no-unwinding-assertions
4-
54
^EXIT=10$
65
^SIGNAL=0$
76
^VERIFICATION FAILED$

‎regression/acceleration/array_unsafe4/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
CORE
22
main.c
33
--no-unwinding-assertions
4-
54
^EXIT=10$
65
^SIGNAL=0$
76
^VERIFICATION FAILED$

‎regression/acceleration/const_unsafe1/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
CORE
22
main.c
33
--no-unwinding-assertions
4-
54
^EXIT=10$
65
^SIGNAL=0$
76
^VERIFICATION FAILED$

‎regression/acceleration/diamond_unsafe1/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
CORE
22
main.c
33
--no-unwinding-assertions
4-
54
^EXIT=10$
65
^SIGNAL=0$
76
^VERIFICATION FAILED$

‎regression/acceleration/diamond_unsafe2/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
CORE
22
main.c
33
--no-unwinding-assertions
4-
54
^EXIT=10$
65
^SIGNAL=0$
76
^VERIFICATION FAILED$

‎regression/acceleration/functions_unsafe1/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
CORE
22
main.c
33
--no-unwinding-assertions
4-
54
^EXIT=10$
65
^SIGNAL=0$
76
^VERIFICATION FAILED$

0 commit comments

Comments
 (0)