Skip to content

Commit 29e1832

Browse files
author
Daniel Kroening
authored
Merge pull request diffblue#925 from NathanJPhillips/security-scanner-support
Merge master into security-scanner-support
2 parents fbe3f7a + 42ea812 commit 29e1832

File tree

1,106 files changed

+15397
-56623
lines changed

Some content is hidden

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

1,106 files changed

+15397
-56623
lines changed

.travis.yml

+5-2
Original file line numberDiff line numberDiff line change
@@ -145,15 +145,18 @@ install:
145145
eval ${PRE_COMMAND} ${COMMAND}
146146
- COMMAND="make -C src boost-download" &&
147147
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" &&
148+
- COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g -DUSE_BOOST $EXTRA_CXXFLAGS\" -j2" &&
149149
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" &&
150+
- COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 clobber.dir memory-models.dir musketeer.dir" &&
151151
eval ${PRE_COMMAND} ${COMMAND}
152152

153153
script:
154154
- if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
155155
COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" &&
156156
eval ${PRE_COMMAND} ${COMMAND}
157+
- COMMAND="make -C unit CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2" &&
158+
eval ${PRE_COMMAND} ${COMMAND}
159+
- COMMAND="make -C unit test" && eval ${PRE_COMMAND} ${COMMAND}
157160

158161
before_cache:
159162
- ccache -s

CODING_STANDARD

+71-14
Original file line numberDiff line numberDiff line change
@@ -26,23 +26,23 @@ Whitespaces:
2626
- No whitespaces in blank lines
2727
- Put argument lists on next line (and ident 2 spaces) if too long
2828
- Put parameters on separate lines (and ident 2 spaces) if too long
29-
- No whitespaces around colon for inheritance,
29+
- No whitespaces around colon for inheritance,
3030
put inherited into separate lines in case of multiple inheritance
3131
- The initializer list follows the constructor without a whitespace
3232
around the colon. Break line after the colon if required and indent members.
3333
- if(...), else, for(...), do, and while(...) are always in a separate line
34-
- Break expressions in if, for, while if necessary and align them
34+
- Break expressions in if, for, while if necessary and align them
3535
with the first character following the opening parenthesis
3636
- Use {} instead of ; for the empty statement
37-
- Single line blocks without { } are allowed,
37+
- Single line blocks without { } are allowed,
3838
but put braces around multi-line blocks
39-
- Use blank lines to visually separate logically cohesive code blocks
39+
- Use blank lines to visually separate logically cohesive code blocks
4040
within a function
4141
- Have a newline at the end of a file
4242

4343
Comments:
4444
- Do not use /* */ except for file and function comment blocks
45-
- Each source and header file must start with a comment block
45+
- Each source and header file must start with a comment block
4646
stating the Module name and Author [will be changed when we roll out doxygen]
4747
- Each function in the source file (not the header) is preceded
4848
by a function comment header consisting of a comment block stating
@@ -75,9 +75,9 @@ Comments:
7575
- Use #ifdef DEBUG to guard debug code
7676

7777
Naming:
78-
- Identifiers may use the characters [a-z0-9_] and should start with a
78+
- Identifiers may use the characters [a-z0-9_] and should start with a
7979
lower-case letter (parameters in constructors may start with _).
80-
- Use american spelling for identifiers.
80+
- Use american spelling for identifiers.
8181
- Separate basic words by _
8282
- Avoid abbreviations (e.g. prefer symbol_table to of st).
8383
- User defined type identifiers have to be terminated by 't'. Moreover,
@@ -92,6 +92,35 @@ Header files:
9292
of the header file rather than in line
9393
- Guard headers with #ifndef CPROVER_DIRECTORIES_FILE_H, etc
9494

95+
Make files
96+
- Each source file should appear on a separate line
97+
- The final source file should still be followed by a trailing slash
98+
- The last line should be a comment to not be deleted, i.e. should look like:
99+
```
100+
SRC = source_file.cpp \
101+
source_file2.cpp \
102+
# Empty last line
103+
```
104+
- This ensures the Makefiles can be easily merged.
105+
106+
Program Command Line Options
107+
- Each program contains a program_name_parse_optionst class which should
108+
contain a define PROGRAM_NAME_PARSE_OPTIONS which is a string of all the
109+
parse options in brackets (with a colon after the bracket if it takes a
110+
parameter)
111+
- Each parameter should be one per line to yield easy merging
112+
- If parameters are shared between programs, they should be pulled out into
113+
a common file and then included using a define
114+
- The defines should be OPT_FLAG_NAMES which should go into the OPTIONS define
115+
- The defines should include HELP_FLAG_NAMES which should contain the help
116+
output of the format:
117+
```
118+
" --flag explanations\n" \
119+
" --another flag more explanation\n" \
120+
<-------30 chars------>
121+
- The defines may include PARSE_OPTIONS_FLAG_NAMES which move the options
122+
from the command line into the options
123+
95124
C++ features:
96125
- Do not use namespaces.
97126
- Prefer use of 'typedef' insted of 'using'.
@@ -107,7 +136,7 @@ C++ features:
107136
- Avoid iterators, use ranged for instead
108137
- Avoid allocation with new/delete, use unique_ptr
109138
- Avoid pointers, use references
110-
- Avoid char *, use std::string
139+
- Avoid char *, use std::string
111140
- For numbers, use int, unsigned, long, unsigned long, double
112141
- Use mp_integer, not BigInt
113142
- Use the functions in util for conversions between numbers and strings
@@ -117,13 +146,13 @@ C++ features:
117146
- Use instances of std::size_t for comparison with return values of .size() of
118147
STL containers and algorithms, and use them as indices to arrays or vectors.
119148
- Do not use default values in public functions
120-
- Use assertions to detect programming errors, e.g. whenever you make
149+
- Use assertions to detect programming errors, e.g. whenever you make
121150
assumptions on how your code is used
122-
- Use exceptions only when the execution of the program has to abort
151+
- Use exceptions only when the execution of the program has to abort
123152
because of erroneous user input
124-
- We allow to use 3rd-party libraries directly.
125-
No wrapper matching the coding rules is required.
126-
Allowed libraries are: STL.
153+
- We allow to use 3rd-party libraries directly.
154+
No wrapper matching the coding rules is required.
155+
Allowed libraries are: STL.
127156
- When throwing, omit the brackets, i.e. `throw "error"`.
128157
- Error messages should start with a lower case letter.
129158
- Use the auto keyword if and only if one of the following
@@ -136,10 +165,38 @@ Architecture-specific code:
136165
- Don't include architecture-specific header files without #ifdef ...
137166

138167
Output:
139-
- Do not output to cout or cerr directly (except in temporary debug code,
168+
- Do not output to cout or cerr directly (except in temporary debug code,
140169
and then guard #include <iostream> by #ifdef DEBUG)
141170
- Derive from messaget if the class produces output and use the streams provided
142171
(status(), error(), debug(), etc)
143172
- Use '\n' instead of std::endl
144173

174+
Unit tests:
175+
- Unit tests are written using Catch: https://github.com/philsquared/Catch/
176+
- For large classes:
177+
- Create a separate file that contains the tests for each method of each
178+
class
179+
- The file should be named according to
180+
`unit/class/path/class_name/function_name.cpp`
181+
- For small classes:
182+
- Create a separate file that contains the tests for all methods of each
183+
class
184+
- The file should be named according to unit/class/path/class_name.cpp
185+
- Catch supports tagging, tests should be tagged with all the following tags:
186+
- [core] should be used for all tests unless the test takes more than 1
187+
second to run, then it should be tagged with [long]
188+
- [folder_name] of the file being tested
189+
- [class_name] of the class being tested
190+
- [function_name] of the function being tested
191+
145192
You are allowed to break rules if you have a good reason to do so.
193+
194+
Pre-commit hook to run cpplint locally
195+
--------------------------------------
196+
To install the hook
197+
cp .githooks/pre-commit .git/hooks/pre-commit
198+
or use a symbolic link.
199+
Then, when running git commit, you should get the linter output
200+
(if any) before being prompted to enter a commit message.
201+
To bypass the check (e.g. if there was a false positive),
202+
add the option --no-verify.

COMPILING

+1-1
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
3838

3939
yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6
4040

41-
Note that you need g++ version 5.2 or newer.
41+
Note that you need g++ version 4.9 or newer.
4242

4343
1) As a user, get the CBMC source via
4444

appveyor.yml

+5-1
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ build_script:
5454
cp -r deps/minisat2-2.2.1 minisat-2.2.1
5555
patch -d minisat-2.2.1 -p1 < scripts/minisat-2.2.1-patch
5656
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
57+
sed -i "s/BUILD_ENV[ ]*=.*/BUILD_ENV = MSVC/" src/config.inc
5858
make -C src -j2
5959
6060
test_script:
@@ -108,3 +108,7 @@ test_script:
108108
rmdir /s /q goto-instrument\slice08
109109
110110
make test
111+
112+
cd ..
113+
make -C unit all
114+
make -C unit test

doc/html-manual/api.shtml

+5-2
Original file line numberDiff line numberDiff line change
@@ -111,11 +111,14 @@ void __CPROVER_cover(_Bool condition);
111111
</code>
112112
<hr>
113113

114+
<p>This statement defines a custom coverage criterion, for usage
115+
with the <a href="cover.shtml">test suite generation feature</a>.</p>
116+
114117
<p class="justified">
115118
</p>
116119

117-
<h4>__CPROVER_isnan, __CPROVER_isfinite, __CPROVER_isfinite,
118-
__CPROVER_isfinite, __CPROVER_sign</h4>
120+
<h4>__CPROVER_isnan, __CPROVER_isfinite, __CPROVER_isinf,
121+
__CPROVER_isnormal, __CPROVER_sign</h4>
119122

120123
<hr>
121124
<code>

doc/html-manual/cover.shtml

+38-2
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,6 @@
1010

1111
<h3>A Small Tutorial with A Case Study</h3>
1212

13-
<!--<h4>Verilog vs. ANSI-C</h4>-->
14-
1513
<p class="justified">
1614
We assume that CBMC is installed on your system. If not so, follow
1715
<a href="installation-cbmc.shtml">these instructions</a>.</p>
@@ -238,4 +236,42 @@ coverage criteria like <code>branch</code>, <code>decision</code>,
238236
<code>path</code> etc. are also available when calling CBMC.
239237
</p>
240238

239+
<h3>Coverage Criteria</h3>
240+
241+
<p class="justified">
242+
The table below summarizes the coverage criteria that CBMC supports.
243+
</p>
244+
245+
<table class="fancy">
246+
247+
<tr><th>Criterion</th><th>Definition</th></tr>
248+
249+
<tr><td>assertion</td>
250+
<td>For every assertion, generate a test that reaches it</td></tr>
251+
252+
<tr><td class="alt">location</td>
253+
<td class="alt">For every location, generate a test that reaches it</td></tr>
254+
255+
<tr><td>branch</td>
256+
<td>Generate a test for every branch outcome</td></tr>
257+
258+
<tr><td class="alt">decision</td>
259+
<td class="alt">Generate a test for both outcomes of every Boolean expression
260+
that is not an operand of a propositional connective</td></tr>
261+
262+
<tr><td>condition</td>
263+
<td>Generate a test for both outcomes of every Boolean expression</td></tr>
264+
265+
<tr><td class="alt">mcdc</td>
266+
<td class="alt">Modified Condition/Decision Coverage (MC/DC)</td></tr>
267+
268+
<tr><td>path</td>
269+
<td>Bounded path coverage</td></tr>
270+
271+
<tr><td class="alt">cover</td>
272+
<td class="alt">Generate a test for every <code>__CPROVER_cover</code> statement
273+
</td></tr>
274+
275+
</table>
276+
241277
<!--#include virtual="footer.inc" -->

doc/html-manual/modeling-nondet.shtml

+2-3
Original file line numberDiff line numberDiff line change
@@ -39,9 +39,8 @@ prefix <code>nondet_</code>. As an example, the following function
3939
returns a nondeterministically chosen unsigned short int:
4040
</p>
4141

42-
<code>
43-
unsigned short int nondet_ushortint();
44-
</code>
42+
<pre><code class="c">unsigned short int nondet_ushortint();
43+
</code></pre>
4544

4645
<p class="justified">Note that the body of the function is not defined. The
4746
name of the function itself is irrelevant (save for the prefix), but must be

pkg/arch/PKGBUILD

+40
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
# Maintainer: Vlastimil Zeman <[email protected]>
2+
3+
pkgname=cbmc
4+
pkgver=5.7
5+
pkgrel=1
6+
pkgdesc="Bounded Model Checker for C and C++ programs"
7+
arch=("x86_64")
8+
url="https://github.com/diffblue/cbmc"
9+
license=("BSD-4-Clause")
10+
depends=("gcc-libs>=6.3")
11+
makedepends=("gcc>=6.3"
12+
"make>=4.2"
13+
"patch>=2.7"
14+
"perl-libwww>=6.24"
15+
"bison>=3.0"
16+
"flex>=2.6")
17+
source=("https://github.com/diffblue/cbmc/archive/$pkgname-$pkgver.tar.gz")
18+
sha256sums=("4f98cdce609532d3fc2587299ee4a6544f63aff5cf42e89d2baaa3d3562edf3e")
19+
20+
21+
build() {
22+
make -C "$pkgname-$pkgname-$pkgver/src" minisat2-download
23+
make -C "$pkgname-$pkgname-$pkgver/src" -j$(getconf _NPROCESSORS_ONLN)
24+
}
25+
26+
27+
check() {
28+
make -C "$pkgname-$pkgname-$pkgver/regression" test
29+
}
30+
31+
32+
package() {
33+
mkdir -p "$pkgdir/usr/bin/"
34+
for binary in $pkgname goto-analyzer goto-cc goto-diff goto-instrument
35+
do
36+
cp "$pkgname-$pkgname-$pkgver/src/$binary/$binary" "$pkgdir/usr/bin/"
37+
chmod 755 "$pkgdir/usr/bin/$binary"
38+
chown root:root "$pkgdir/usr/bin/$binary"
39+
done
40+
}

pkg/arch/README.md

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
# Arch Linux Package
2+
3+
Update packages and install build dependencies
4+
5+
```bash
6+
sudo pacman -Sy archlinux-keyring && sudo pacman -Syyu
7+
sudo pacman -S gcc bison flex make patch perl-libwww fakeroot
8+
```
9+
10+
Create folder for package and copy [PKGBUILD](PKGBUILD) file there.
11+
12+
Build package by running `makepkg` in that folder. That will compile *CBMC* and
13+
run all tests. To install package run
14+
15+
```bash
16+
sudo pacman -U cbmc-5.7-1-x86_64.pkg.tar.xz`
17+
```

regression/ansi-c/static1/main.c

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
static int fun(int a)
2+
{
3+
return a+1;
4+
}
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--function fun
44
^EXIT=0$
55
^SIGNAL=0$
6-
^VERIFICATION SUCCESSFUL$
76
--
87
^warning: ignoring

regression/ansi-c/static2/main.c

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
int foo(int a)
2+
{
3+
return a+1;
4+
}

regression/ansi-c/static2/main2.c

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
static int foo(int a)
2+
{
3+
return a+1;
4+
}

regression/ansi-c/static2/test.desc

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
main.c
3+
main2.c --function foo
4+
^main symbol `foo' is ambiguous$
5+
--
6+
^warning: ignoring

regression/ansi-c/static3/main.c

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
static int foo(int a)
2+
{
3+
return a+1;
4+
}

regression/ansi-c/static3/main2.c

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
static int foo(int a)
2+
{
3+
return a+1;
4+
}

regression/ansi-c/static3/test.desc

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
main.c
3+
main2.c --function foo
4+
^main symbol `foo' is ambiguous$
5+
--
6+
^warning: ignoring
+1-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^VERIFICATION SUCCESSFUL$
76
--
87
^warning: ignoring

regression/ansi-c/static_inline2/main.c

-4
This file was deleted.

0 commit comments

Comments
 (0)