Skip to content

Security scanner support #750

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 84 commits into from
Apr 3, 2017
Merged

Security scanner support #750

Changes from 1 commit
Commits
Show all changes
84 commits
Select commit Hold shift + click to select a range
60e2e0e
adjusted the command line for the pid controller case study with a be…
theyoucheng Nov 10, 2016
fbdf29a
Remove DEBUG ifdefs which broke the debug build
reuk Mar 16, 2017
0314b24
Remove the disable-runtime-checks flag for Java
cristina-david Mar 16, 2017
6c53036
Fix errors when -Wall -Werror flags are set
reuk Mar 17, 2017
0662dd0
Fix several test problems on Windows
forejtv Mar 8, 2017
1a5c69d
Fix DEBUG blocks based on feedback
reuk Mar 20, 2017
72052c7
Auxiliary function to check whether source location is in built-in
peterschrammel Mar 22, 2017
32fcbbc
Replace built-in checks by is_built_in
peterschrammel Mar 22, 2017
ff9d833
Merge pull request #622 from forejtv/master
Mar 23, 2017
c21d3ed
update instructions for g++ 6
Mar 23, 2017
2a95e59
Merge branch 'master' of github.com:diffblue/cbmc
Mar 23, 2017
903d243
Updates for GCC 6
Mar 23, 2017
e843b72
Correct pretty-printing of code_returnt
smowton Mar 20, 2017
4473f06
Fix Java multinewarray
smowton Mar 23, 2017
0a53fbb
Amend test-case to complete in acceptable time
smowton Mar 23, 2017
6550e2c
Merge pull request #658 from smowton/pretty_print_return
Mar 23, 2017
e8ec160
Add --drop-unused-functions option
peterschrammel Mar 22, 2017
a35731b
Remove -show-reachable-properties
peterschrammel Mar 23, 2017
5e5bbca
Correctly align description of option
peterschrammel Mar 22, 2017
5ecb15e
Merge pull request #671 from peterschrammel/cover-for-reachable-fun-only
Mar 23, 2017
85a7566
Option --no-built-in-assertions
peterschrammel Mar 22, 2017
2b09c0b
Remove unused variable and braces
Mar 24, 2017
a3f49a3
Move function comments to the right place
Mar 24, 2017
4c4ccc0
Remove variable that is always false
Mar 24, 2017
9a1dae0
Remove function that's only used once
Mar 24, 2017
27227cc
added support for array_copy in the full-slice option
lucasccordeiro Mar 24, 2017
e70aa7d
added two test cases into goto-instrument regression for checking arr…
lucasccordeiro Mar 24, 2017
727aea1
Merge pull request #694 from lucasccordeiro/fix-full-slice-03
Mar 24, 2017
96c9e65
Merge pull request #686 from smowton/fix_multinewarray
Mar 24, 2017
7e406cd
Merge pull request #682 from jgwilson42/compiling_update
Mar 24, 2017
83874c3
Release notes up to 5.6 from CProver Google group messages
tautschnig Mar 24, 2017
81470f4
Initial version of release notes for 5.7
tautschnig Mar 24, 2017
4ea27a3
Merge pull request #696 from tautschnig/user-visible-changes
Mar 25, 2017
cf17239
Merge pull request #693 from owen-jones-diffblue/cleanup/java-object-…
Mar 25, 2017
29af567
Merge pull request #681 from peterschrammel/no-assertions-for-user-only
Mar 25, 2017
ad384f1
kept consistency between parse options of cbmc and goto-instrument tools
lucasccordeiro Mar 27, 2017
13dfd5a
make_binary is not safe to use when types are mixed
tautschnig Mar 1, 2016
b4ae916
Enabled test cases in goto-instrument after fixes in the full-slice
lucasccordeiro Mar 27, 2017
e333f8d
Tolerate missing symbols in gather_needed_globals. Fixes #620
smowton Mar 28, 2017
a8a5eb1
Remove reserved identifier
reuk Mar 28, 2017
f9aac34
Avoid duplicate callee class-ids in virtual dispatch tables. Fixes #684
smowton Mar 28, 2017
da35d59
Merge pull request #713 from reuk/language-ui-cleanup
Mar 28, 2017
b1d0666
Merge pull request #703 from lucasccordeiro/cprover-library-message
Mar 28, 2017
02c77a4
Added tests that demonstrate the issue with static inline c functions.
NlightNFotis Mar 28, 2017
6824297
Include --verbosity in help output of cbmc and symex
tautschnig Jun 27, 2016
090dfce
fixup! Add json->irep deserialization routine
tautschnig Mar 27, 2017
d658c0c
Throw when -DNDEBUG would cause missing return values
tautschnig Mar 27, 2017
b5e97ae
fixup! Add --drop-unused-functions option
tautschnig Mar 27, 2017
5aef4f2
fixup! Option --no-built-in-assertions
tautschnig Mar 27, 2017
bfd57ba
missing assert.h
Jun 20, 2016
628d4e1
Generalise witness as location numbers may vary
tautschnig Dec 12, 2016
753e718
Minor code cleanup of irep.h
tautschnig Jun 25, 2016
6755ecf
Fix really pedantic compiler errors
reuk Mar 29, 2017
a79ea27
Merge pull request #700 from lucasccordeiro/fix-full-slice-04
Mar 29, 2017
55b5b7e
Merge pull request #714 from smowton/fix_lazy_methods_with_opaque_glo…
Mar 29, 2017
7300d07
String abstraction requires remove_returns
tautschnig Nov 5, 2016
80ba3cf
Make rename_symbol a no-op if its maps are empty
tautschnig Jun 26, 2016
39c26fb
Merge pull request #718 from NlightNFotis/bugdemo/static_inline
Mar 29, 2017
565faaf
Merge pull request #715 from smowton/fix_duplicate_virtual_dispatch_g…
Mar 29, 2017
7e24dca
Merge pull request #723 from reuk/extra-errors
Mar 29, 2017
556352d
Merge pull request #724 from tautschnig/release-cleanup
Mar 29, 2017
9c12efd
use stat to determine whether a directory entry is a subdirectory; d_…
Mar 29, 2017
cf42202
gcc_message_handlert must obey verbosity
tautschnig Feb 21, 2017
943bdc8
Ubuntu has new g++
Mar 29, 2017
2d26cb7
removed unnecessary newline
Mar 29, 2017
0983dbf
compile with Visual Studio 2017
Mar 29, 2017
610e9e4
use std::size_t for counters
Mar 29, 2017
7fd6180
Fix concurrent traces generated via --trace
tautschnig Mar 25, 2017
66481ab
Removed the dynamic_object_exprt's instance()
mariusmc92 Mar 14, 2017
d811f4d
update compilation instructions
Apr 2, 2017
0889178
Merge pull request #31 from tautschnig/make_binary-vs-pointers
Apr 3, 2017
4fc6633
Migrated all message clients to messaget, removing deprecated message…
tautschnig Jul 6, 2016
79a95f7
Merge pull request #300 from theyoucheng/case-study
Apr 3, 2017
ce147fb
removed legacy_typecheckt
Apr 3, 2017
7f0ae8b
Merge branch 'master' of github.com:diffblue/cbmc
Apr 3, 2017
b0778bf
Consistency: use messaget's error directly instead of throwing string…
tautschnig Jul 7, 2016
d13a056
use new messaging interface
Apr 3, 2017
767a373
Added location information to warning messages missing it
tautschnig Jul 11, 2016
f2f5e36
Completely remove cpp_typecheckt::check_template_restrictions
tautschnig Jul 11, 2016
384bd7c
Merge pull request #716 from mariusmc92/cleanup/type-safe-dynamic-object
Apr 3, 2017
cba259c
Merge pull request #647 from reuk/remove-broken-debug
Apr 3, 2017
11773eb
Merge pull request #649 from cristina-david/remove-disable-runtime-ch…
Apr 3, 2017
5679e90
Merge pull request #697 from tautschnig/concurrency-trace
Apr 3, 2017
3dc10b7
Merge master into security-scanner-support
NathanJPhillips Apr 3, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Ubuntu has new g++
  • Loading branch information
Daniel Kroening committed Mar 29, 2017
commit 943bdc8be4543145e6b29fd734e132e83ab8a9ae
8 changes: 7 additions & 1 deletion COMPILING
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,12 +44,18 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.

git clone https://github.com/diffblue/cbmc cbmc-git

2) On Debian/Ubuntu, do
2) On Debian, do

cd cbmc-git/src
make minisat2-download
make CXX=g++-6

On Ubuntu, or other distributions with recent g++, do

cd cbmc-git/src
make minisat2-download
make

On Redhat/Fedora etc., do

cd cbmc-git/src
Expand Down