Merge current cbmc/master into test-gen-support#762

Merged

peterschrammel merged 170 commits intodiffblue:test-gen-supportfrom

smowton:smowton/merge/master_2017_04_05

Apr 5, 2017

Commits on Nov 10, 2016

adjusted the command line for the pid controller case study with a better look output test suites
theyoucheng
committed

Commits on Jan 25, 2017

Turn "label: goto label;" or "while(cond);" into assume
tautschnig
committed

Commits on Mar 15, 2017

support class file loading limit in classpath
Matthias Güdemann
committed
add regression test for class path load limit
Matthias Güdemann
committed

Commits on Mar 16, 2017

Commits on Mar 17, 2017

Fix errors when -Wall -Werror flags are set
reuk
committed

Commits on Mar 21, 2017

Fix DEBUG blocks based on feedback
reuk
committed

Commits on Mar 24, 2017

Adding tests for function pointer removal
thk123
committed
Made remove_function_pointers inherit from messaget
thk123
committed
First implemention of the new approach
thk123
committed
Support for removing the typecast
thk123
committed
Adding support for top level pointers and typecasts
thk123
committed
Fixing arrays containing null pointers
thk123
committed
Correctly deal with const structures
thk123
committed
Fixing component access and const access
thk123
committed
Fixing todo to use separate array
thk123
committed
Corrected const-ness for components
thk123
committed
Handle failure to squash the value when getting out of an array
thk123
committed
Correcting const check for pointers
thk123
committed
Adding examples to tests of what the const prevents
thk123
committed
Corrected const check for no FP pointers
thk123
committed
Added tests to cover a couple of missed lines
thk123
committed
Fixed issue with structs with other components
thk123
committed
Adding test for another way the previous bug could be exhibited
thk123
committed
Adding a test variation of 44 without the consts that fails correctly
thk123
committed
Squash constant symbols first
thk123
committed
Fixed major bug with non const structs
thk123
committed
Removing redundant code
thk123
committed
Added logging for all the ways the FP removal might not complete
thk123
committed
Adding consistency checks for the output
thk123
committed
Adding comments to remove_const_function_pointers
thk123
committed
Renamed all the tests
thk123
committed
Tidied up tests

thk123
authored and
thk123
committed
Fixing compile errors for musketeer

thk123
authored and
thk123
committed
Refactored resolve_index_of_function_call

thk123
authored and
thk123
committed
Split out functions from try_resolve_function_call

thk123
authored and
thk123
committed
Made the behaviour of try_resolve_function_call clearer

thk123
authored and
thk123
committed
Split up try_resolve_expression into functions

thk123
authored and
thk123
committed
Made other try_resolve*_function_call use the normal method

thk123
authored and
thk123
committed
Extracted element dealing with calling resolve on each result

thk123
authored and
thk123
committed
Adding the pointer check flag

thk123
authored and
thk123
committed
Adding checks for NULL function pointers

thk123
authored and
thk123
committed
Renaming functions to more consistent name

thk123
authored and
thk123
committed
Swap to using an unorded set

thk123
authored and
thk123
committed
Added flag for goto-instrument to just remove const function pointers

thk123
authored and
thk123
committed
Check the GOTO program for loss of const

thk123
authored and
thk123
committed
Added a couple of missed test cases.

thk123
authored and
thk123
committed
Fixing tests to work with new test.pl

thk123
authored and
thk123
committed
Fixing missing new lines

thk123
authored and
thk123
committed
Split out the const check into own analysis
thk123
committed
Descend all children of the same base type
thk123
committed
PR Feedback implementation
thk123
committed
Use pointers in is_type_at_least_as_const_as
thk123
committed

Commits on Mar 27, 2017

Commits on Mar 28, 2017

Commits on Mar 29, 2017

Include --verbosity in help output of cbmc and symex
tautschnig
committed
fixup! Add json->irep deserialization routine
tautschnig
committed
Throw when -DNDEBUG would cause missing return values
tautschnig
committed
fixup! Add --drop-unused-functions option
tautschnig
committed
fixup! Option --no-built-in-assertions
tautschnig
committed
missing assert.h

Daniel Kroening
authored and
tautschnig
committed
Generalise witness as location numbers may vary
tautschnig
committed
Minor code cleanup of irep.h
tautschnig
committed
Generalise witness as location numbers may vary
tautschnig
committed
Rename _start to __CPROVER_start
tautschnig
committed
Fix really pedantic compiler errors
reuk
committed
Merge pull request #700 from lucasccordeiro/fix-full-slice-04
Daniel Kroening
authored
Merge pull request #714 from smowton/fix_lazy_methods_with_opaque_globals
Daniel Kroening
authored
String abstraction requires remove_returns
tautschnig
committed
Make rename_symbol a no-op if its maps are empty
tautschnig
committed
Merge pull request #718 from NlightNFotis/bugdemo/static_inline
Daniel Kroening
authored
Merge pull request #715 from smowton/fix_duplicate_virtual_dispatch_gotos
Daniel Kroening
authored
Merge pull request #723 from reuk/extra-errors
Daniel Kroening
authored
Merge pull request #724 from tautschnig/release-cleanup
Daniel Kroening
authored
use stat to determine whether a directory entry is a subdirectory; d_type is not POSIX
Daniel Kroening
committed
gcc_message_handlert must obey verbosity

tautschnig
authored and
Daniel Kroening
committed
Ubuntu has new g++
Daniel Kroening
committed
removed unnecessary newline
Daniel Kroening
committed
compile with Visual Studio 2017
Daniel Kroening
committed
use std::size_t for counters
Daniel Kroening
committed

Commits on Mar 30, 2017

Commits on Mar 31, 2017

Commits on Apr 2, 2017

update compilation instructions
Daniel Kroening
committed

Commits on Apr 3, 2017

Merge pull request #31 from tautschnig/make_binary-vs-pointers
Daniel Kroening
authored
Migrated all message clients to messaget, removing deprecated message_streamt

tautschnig
authored and
Daniel Kroening
committed
Merge pull request #300 from theyoucheng/case-study
Daniel Kroening
authored
removed legacy_typecheckt
Daniel Kroening
committed
Merge branch 'master' of github.com:diffblue/cbmc
Daniel Kroening
committed
Consistency: use messaget's error directly instead of throwing string/char*

tautschnig
authored and
Daniel Kroening
committed
use new messaging interface
Daniel Kroening
committed
Added location information to warning messages missing it

tautschnig
authored and
Daniel Kroening
committed
Completely remove cpp_typecheckt::check_template_restrictions

tautschnig
authored and
Daniel Kroening
committed
Merge pull request #716 from mariusmc92/cleanup/type-safe-dynamic-object
Daniel Kroening
authored
Merge pull request #647 from reuk/remove-broken-debug
Daniel Kroening
authored
Merge pull request #649 from cristina-david/remove-disable-runtime-checks
Daniel Kroening
authored
Merge pull request #697 from tautschnig/concurrency-trace
Daniel Kroening
authored
Enable ccache on Travis, plus travis.yml restructuring
forejtv
committed
Allow cpplint to fail on Travis.
forejtv
committed
Add XML and JSON output to the base of both ai domains and the ai analysis.

Martin Brain
authored and
Daniel Kroening
committed
Merge branch 'master' of github.com:diffblue/cbmc
Daniel Kroening
committed
Constant propagator and intervals regression tests

Martin Brain
authored and
Daniel Kroening
committed
Add utility function to tell if a program is threaded or not.

martin
authored and
Daniel Kroening
committed
Fixes and improvements to the constant and interval domain.

martin
authored and
Daniel Kroening
committed
camel case for json

danpoe
authored and
Daniel Kroening
committed
merge fixes

danpoe
authored and
Daniel Kroening
committed
Merge pull request #745 from forejtv/feature/travis-ccache
Daniel Kroening
authored
fix travis merge problem
forejtv
committed
Mark goto-analyzer tests as not working until the new version is merged in
forejtv
committed
Split Travis debug build to separate jobs, and run it only on Linux.
forejtv
committed

Commits on Apr 4, 2017

Merge pull request #753 from forejtv/bugfix/master-fixes
Daniel Kroening
authored
Merge pull request #747 from tautschnig/undefined-function-assume-false
Daniel Kroening
authored
Use versioned container of Alpine linux.
Vlastimil Zeman
committed
Merge pull request #358 from thk123/bug/typedef-structs-clean
Daniel Kroening
authored
Merge pull request #375 from tautschnig/trivial-loops
Daniel Kroening
authored
Merge pull request #519 from thk123/feature/clean-fp-removal
Daniel Kroening
authored
Merge pull request #566 from owen-jones-diffblue/feature/tests-for-sensitivity
Daniel Kroening
authored
Merge pull request #588 from smowton/sss_get_language_options
Daniel Kroening
authored
Merge pull request #639 from mgudemann/feature/limit_class_path_loading
Daniel Kroening
authored
Merge pull request #680 from tautschnig/coverage-fixes
Daniel Kroening
authored
Merge pull request #721 from tautschnig/rename-_start
Daniel Kroening
authored
Merge branch 'master' into reachability-slice
Daniel Kroening
authored
Merge pull request #732 from tautschnig/reachability-slice
Daniel Kroening
authored
Merge pull request #734 from tautschnig/sv-comp-support
Daniel Kroening
authored
Merge pull request #736 from zemanlx/feature/travis-use-versioned-container
Daniel Kroening
authored
Merge pull request #737 from smowton/java_null_checks
Daniel Kroening
authored
Merge pull request #740 from tautschnig/status-assume-false
Daniel Kroening
authored
Fix failing build on master.
forejtv
committed
Fix failing test's regexp.
forejtv
committed
Merge pull request #757 from forejtv/bugfix/master-fixes
Daniel Kroening
authored

Commits on Apr 5, 2017

Merge remote-tracking branch 'origin/master' into smowton/merge/master_2017_04_05
smowton
committed