Squashed 'cbmc/' changes from 720200398..768e8a6

REVERT: 720200398 Merge branch 'develop' of github.com:diffblue/cbmc into CBMC_subtree_2018-04-10
REVERT: e2d4b09dd Updates for merge
REVERT: 1ab596d0e Merge commit '3b8120f3a8c9ed3a343493a44ac454ae265946c1' into develop
REVERT: f7602af Merge commit 'bb88574aaa4043f0ebf0ad6881ccaaeb1f0413ff' into merge-develop-20180327
REVERT: 207b801 Merge branch 'develop' into merge_2018-03-26
REVERT: 906aeb3 Merge pull request diffblue#349 from diffblue/owen-jones-diffblue/fix-compilation-for-release
REVERT: 3d8423c Merge pull request diffblue#350 from diffblue/owen-jones-diffblue/skip-duplicate-callsites-in-lazy-methods
REVERT: 73fb488 bugfix from upstream repo for generic crash
REVERT: fd76555 Speed up resolution of virtual callsites in lazy loading
REVERT: 3fd28f3 Replace assert(X) by UNREACHABLE/INVARIANT(X)
REVERT: 557158e Merge pull request diffblue#334 from diffblue/pull-support-20180216
REVERT: 1e48132 Merge from master, 20180216
REVERT: ad7b28e Updates requsted in the PR: mostly rename 'size -> length'.
REVERT: e3fcb9b Introducing MAX_FILE_NAME_SIZE constant.
REVERT: 40b8c03 Updates requested in PR - mainly rename of functions.
REVERT: 7f868e2 Reused private code in 'remove_virtual_functions.cpp' by making it public.
REVERT: 1e0ac30 Turn get_may, set_may, etc into irep_ids
REVERT: bf7ed1a Merge pull request diffblue#313 from diffblue/owen-jones-diffblue/add-structured-lhs-to-value-set
REVERT: 1f06d35 Merge pull request diffblue#312 from diffblue/pull-support-20180112
REVERT: e42e97a Merge commit '23666e3af35673c734c9816ffc131b6b9a379e86' into pull-support-20180112
REVERT: 53f1a41 Populate structured_lhs in all `entryt`s
REVERT: 574101c Add `structured_lhs` field to entryt
REVERT: 3d492fe Add documentation of return values
REVERT: d190fd8 Merge remote-tracking branch 'upstream/develop' into pull-support-20180112
REVERT: 092df69 Switch from custom file / path routines to Boost-filesystem
REVERT: faf8f00 Merge commit 'a83b52cddbed22304372c276512c63701eb3aedb' into pull-support-20180104
REVERT: 67ec6f2 Merge remote-tracking branch 'upstream/develop' into pull-support-20180104
REVERT: 5266ba2 Merge commit 'ac4756fc3bb0e853f04de2b69f300d65cfbfc553' into pull-support-20171212
REVERT: ca5aa95 Merge remote-tracking branch 'upstream/develop' into merge-develop-20171212
REVERT: ed5f719 Move of alias code from VSA to LVSA.
REVERT: a44becc Requests in the PR (structure of comments).
REVERT: ef51720 Updates requested in the PR (added comments).
REVERT: 377a515 Introducing function 'get_may_alias_values'.
REVERT: c0de6fb Merge pull request diffblue#273 from diffblue/smowton/fix/end_to_end_tests
REVERT: 37e5b80 Add `override` in a few places
REVERT: 653dcb6 Fix taint instrumenter handling array initalisers
REVERT: 523f60e Change template of value_set_analysis_baset
REVERT: 4f45985 Merge pull request diffblue#271 from diffblue/smowton/merge_develop_2017_11_16
REVERT: 7619d15 Rename ID_lvsa_mode to ID_lvsa_evs_type
REVERT: 471180d Adapt to upstream CBMC changes
REVERT: e8b3cb9 Merge remote-tracking branch 'upstream/develop' into smowton/merge/develop_20171116
REVERT: f653f85 Merge pull request diffblue#263 from diffblue/owen/fix-memory-bug
REVERT: 599a2f9 Merge pull request diffblue#264 from diffblue/smowton/fix/slice24_include
REVERT: de905e7 slice24 test: switch from malloc.h to stdlib.h
REVERT: c8efb6f Fix bug that can cause segfault
REVERT: fac9dea Rename "#lva_mode" to "lvsa_mode"
REVERT: 72c8533 Make two irep IDs
REVERT: 93ebb84 Merge commit '356aed461b387a8ae815a9901a16d26f32f102be' into develop
REVERT: 4820601 Merge remote-tracking branch 'diffblue/develop' into merge-dev-to-ss
REVERT: b03ec16 Merge pull request diffblue#239 from diffblue/bugfix/value_sets_fi_and_reaching_defs_retrievals_of_dynamic_objects
REVERT: 739c7f5 Merge remote-tracking branch 'upstream/develop' into merge-develop-20171026
REVERT: 37b868a Merge pull request diffblue#251 from diffblue/feature/revert-recording-symbol-table
REVERT: c4ed1ae Revert security-scanner version of recording symbol table
REVERT: e83e307 Fixed scope of moved symbol
REVERT: a6adb19 Fix more catch std::string occurances
REVERT: d115b4e catch by const ref instead of by value or non-const ref
REVERT: 912ee38 Improve symbol table style
REVERT: 6b1a49d Add missing goto-statistics file to Makefile
REVERT: d512204 Add cbmc and jbmc as install targets
REVERT: bc887c5 Merge commit '93e2d7626046f90e14de76abbaf16c57a0425d8a' into pull-support-20171019
REVERT: 64d81f1 Merge remote-tracking branch 'upstream/develop' into pull-support-20171019
REVERT: 9a59fb9 Renamed DiffBlue -> Diffblue
REVERT: db79106 Added explanatory comment for the introduced condition.
REVERT: dfc6a20 Fixing C++ code-style issues.
REVERT: 7989831 Added regression test for the fixed bug.
REVERT: 00b4af2 Bugfix: Explicit retrievals of DOs from value_set amd reaching_defs.
REVERT: 19858f9 Fix zeroing of arrays in value set analysis
REVERT: 12fd5fe Fix identifying arrays in value set analysis
REVERT: 89341da Merge pull request diffblue#227 from diffblue/feature/adding_goto_statistics_to_goto-instrument
REVERT: 9cf47a2 Updates requested in the PR.
REVERT: 4c4a267 Adding computation and save of goto program statistics.
REVERT: 48b154a Bugfix: Exclude functions without bodies from GOTO statistics.
REVERT: 6bc86e1 Merge pull request diffblue#222 from diffblue/feature/lexicographical_ordered_dump_of_functions_and_symbols
REVERT: a73ee46 Merge pull request diffblue#224 from diffblue/feature/file_utils_add_parsing_of_file_extension
REVERT: 421f4eb Merge pull request diffblue#226 from diffblue/feature/goto_statistics
REVERT: 6d9f029 Updates requested in the PR.
REVERT: 6f8ebe4 Updates requested in the PR.
REVERT: d4a04ac Added support of Windows platform to parsing file extension.
REVERT: 1884d67 Merge pull request diffblue#221 from diffblue/bugfix/INVARIANT_while(0)_to_while(false)
REVERT: 39a774f Introducing GOTO program statistics.
REVERT: 821ba1c Updates requested in the PR.
REVERT: 9266de0 Add parsing of file extension from file path-name.
REVERT: 632ae4b Updates to recording_symbol_tablet
REVERT: 56b0b26 Added lexicographical order to textual dump of functions and symbols.
REVERT: 79324b3 INVARIANT: while(0) -> while(false)
REVERT: 733f7b2 Added is_success and is_error helpers
REVERT: 5e7f3f7 Added implicit constructors to main_function_resultt to make code in get_main_symbol even briefer
REVERT: 3317a3a Tidied up code in get_main_symbol
REVERT: 47fe36f Changed main_function_resultt to use an enum instead of a collection of bools
REVERT: a084a6a Reverting indentation in order to make the compiler silent.
REVERT: e4b5e12 Merge pull request diffblue#218 from diffblue/cleanup/typo
REVERT: 5fecceb Added recording_symbol_tablet
REVERT: 4d65951 Split storage for symbol_tablet into a concrete derived type
REVERT: 7b254e2 Made move constructor strong exception safe
REVERT: d66c0bc Changed interface to symbol_tablet::insert
REVERT: 6dc1213 Typo in reachable
REVERT: db9a0a7 Updates requested in the PR.
REVERT: d00c03d Introducing "enable_ccache" switch (default on) into our build system.
REVERT: f079156 Merge pull request diffblue#205 from diffblue/feature/restrict-symbol-table
REVERT: 2462077 Misc review requests
REVERT: 98d0082 Made lookup return optional
REVERT: db69023 Restricted interface of current symbol_tablet
REVERT: ea74c6d Updated comment
REVERT: 909b557 Added INVARIANT to symbol_tablet::remove
REVERT: bd3ee6e Add move insert to symbol_table
REVERT: 18aacc0 Add full JSON-structured output for value-set analysis
REVERT: 0cdd9c6 Improve structure of JSON static-analysis dump
REVERT: 7df9f15 Add LVSA summary dump-to-JSON
REVERT: d0d3620 Merge remote-tracking branch 'upstream/develop' into security-scanner-support
REVERT: ae83e4e Added install command for required projects.
REVERT: c48170e Merge pull request diffblue#192 from diffblue/smowton/feature/split_frontend_final_stage
REVERT: f4df5c6 Add tests for mixed GOTO and C input
REVERT: 215d5bf Split the entry-point-generation phase into two parts
REVERT: ab347d5 Merge pull request diffblue#195 from diffblue/bugfix/missing-const_cast
REVERT: 73fba6e Fixed missing const_cast
REVERT: eaf97f6 Simplify remove_instanceof logic
REVERT: 4969295 Tidy up remove_instanceof
REVERT: 2716410 Update linter to cope with CBMC subtree
REVERT: da91319 Adapt to upstream change in write_goto_binary interface and languaget
REVERT: 08f269c Merge pull request diffblue#1388 from smowton/merge-develop-20170914
REVERT: e3f3abd Merge remote-tracking branch 'upstream/develop' into merge-develop-20170914
REVERT: f25db0a Merge pull request diffblue#189 from diffblue/smowton/fix/remove_debug_code
REVERT: 1fae64c Remove stray use of overlay_map
REVERT: a2834d0 Map wrappers: forward more of the std::map interface
REVERT: 0a668ae Merge commit '6f386e5eeffa223e7213b596403085f8b497023e' into pull-support-20170908-2
REVERT: 04b4f63 Merge pull request diffblue#186 from diffblue/cleanup/misc
REVERT: 577fa6c Tightened up usage of maps
REVERT: 40557df Used range iterators
REVERT: d4e89fd Tidy up symbol_tablet::move
REVERT: 5a58539 Merge pull request diffblue#1354 from NathanJPhillips/merge-develop-to-sss
REVERT: 498718f Code readability
REVERT: 5648db1 Merge latest changes from develop to Security Scanner Support
REVERT: 52eb7ed Merge pull request diffblue#1347 from NathanJPhillips/sss/merge-develop
REVERT: 660f804 Merge develop into SSS
REVERT: 281e384 Workaround for travis performing shallow clones with wrong branch
REVERT: 33d8af7 Merge pull request diffblue#1296 from NathanJPhillips/merge-master
REVERT: c043179 Applied doxygen style to all new comments
REVERT: 3ab10aa Merge branch 'master' into security-scanner-support
REVERT: 29e1832 Merge pull request diffblue#925 from NathanJPhillips/security-scanner-support
REVERT: 42ea812 Fix missing += in Makefile that causes issues in building unit test
REVERT: d016980 Merge master into security-scanner-support
REVERT: fbe3f7a Merge pull request diffblue#845 from NathanJPhillips/security-scanner-support
REVERT: 1e919d1 Merge branch 'master' into security-scanner-support
REVERT: 5159ef1 Merge pull request diffblue#830 from mariusmc92/cleanup/move-singularity-in-vsa
REVERT: 606a5ab Added singularity check method as virtual in VSA
REVERT: 8faef3b Merge pull request diffblue#818 from NathanJPhillips/security-scanner-support
REVERT: 9c06fba Merge master into security-scanner-support
REVERT: cdce3fa Merge pull request diffblue#779 from mariusmc92/cleanup/replace-plain-string-dynamic-object
REVERT: 42f12f1 Added usages of the dynamic-object prefix's string
REVERT: 8a7fbb7 Added global string for dynamic-object prefix
REVERT: 55b3640 Merge pull request diffblue#756 from mariusmc92/feature/recency-analysis
REVERT: 9b728a7 Propagated changes of dynamic-objects' recency
REVERT: 72694d1 Added usage of dynamic-objects with recency
REVERT: 28dc578 Merge pull request diffblue#750 from NathanJPhillips/security-scanner-support
REVERT: 3dc10b7 Merge master into security-scanner-support
REVERT: 33693d8 Merge pull request diffblue#725 from smowton/boost_download
REVERT: e16f583 Switch to using Boost header-only tarball
REVERT: 36851e1 Merge pull request diffblue#706 from smowton/remove_boost_fs_dependency
REVERT: 037da22 Replace boost dependency with simple mkdir -p implementation
REVERT: 3f87bb2 Merge pull request diffblue#704 from NathanJPhillips/feature/serialization-improvements
REVERT: ad18aa9 Use shared_ptr for traits
REVERT: ca0b983 Use explicitly sized integer types
REVERT: 1ab6a25 Undid accidental config.inc change
REVERT: 29cf00c Extension of the call-graph and call-graph-based algorithms (diffblue#641)
REVERT: c694703 Added output in DOT format for class hierarchy. (diffblue#642)
REVERT: ef04e12 Merge pull request diffblue#663 from NathanJPhillips/feature/serialization
REVERT: 0764707 Used assert instead of logic_error as requested in review
REVERT: 74aea8f Added section headings
REVERT: 87a6ff5 Added serialization of irept and dstringt
REVERT: a39da77 Merge pull request diffblue#673 from NathanJPhillips/security-scanner-support
REVERT: 0bd91b5 Merge branch 'master' into security-scanner-support
REVERT: 43caa75 Merge pull request diffblue#667 from NathanJPhillips/security-scanner-support
REVERT: da9fe29 Merged master to get update to delete_directory and linter
REVERT: 08487ad Merge pull request diffblue#634 from smowton/sss_pretty_printing
REVERT: ebf7b78 Merge pull request diffblue#643 from NathanJPhillips/bugfix/file_util_sss
REVERT: ff0f281 Document pretty-printing mechanism
REVERT: 208b2e8 Add pretty-printer extension mechanism
REVERT: c4c75da Merge pull request diffblue#656 from NathanJPhillips/security-scanner-support
REVERT: 8723d57 Merge master into SSS
REVERT: e4ee8e5 Handle path doesn't exist in fileutl_absolute_path
REVERT: 749264b Call get_value_set via a base-class reference
REVERT: a5ccbd9 Add irep IDs used by the security module
REVERT: 7789d01 Add dynamic-object-expr recency
REVERT: dcd058a Comment and slightly reformat strip_casts
REVERT: c6196c3 Lint value-sets
REVERT: 9a811f7 Templatize and virtualize value-set analysis
REVERT: 3cd62e0 Value set: add declared-on-type entry member
REVERT: 53f9cd1 Add function id to value-set.
REVERT: 92ce232 Value set: avoid potential infinite expression
REVERT: 8cbf554 Trim and rename namespace-utils
REVERT: e9205e6 Style namespace-utils
REVERT: a69d950 Add namespace-utils to utils Makefile
REVERT: 229bd5b Add symbol parsing utilities.
REVERT: 116d994 Windows fileutl builds need shlwapi
REVERT: 4bd055b Style and document call graph
REVERT: af7599f Style call_graph
REVERT: 9bfa1ee Amend function documentation style
REVERT: 1095e99 Add call-graph invert and gather-leaves
REVERT: c92564f call_graph: add is-(indirect)-parent functions
REVERT: 0d862d8 Add call-graph topo sort on goto_functionst
REVERT: 85df6db Add call graph sorting and output functions
REVERT: b40dc2b Add option for simplify-expr to keep identical structs
REVERT: 885bedf Add irep IDs
REVERT: 7d57fda Add get-underlying-object utility
REVERT: db44fce Add get_this utility function
REVERT: 5150eca Add parameter-indices to util Makefile
REVERT: 998cc63 Add parameter-indexing utility
REVERT: d895844 Call get_language_options from get_goto_model
REVERT: 554f796 Static analysis: print instructions in dumps
REVERT: 37aa2de Record number of static analysis steps taken
REVERT: 32fd50f Permit static analysis to recurse
REVERT: 8157141 Use function stub behaviour in single-function mode
REVERT: 1c79841 Add static analysis hook for unavailable functions
REVERT: 09937e4 Add overlay-map
REVERT: afe9f5f Make _start optional
REVERT: da72f88 Disable Windows.h min/max define
REVERT: 8bb0fe4 Disable Boost on non-Linux platforms
REVERT: 03eeb47 Style file-util
REVERT: ba470e9 File-util: Windows compatibility fixes
REVERT: b7c00a6 Enable Boost per default
REVERT: c7e65e5 Install boost in test environment
REVERT: be43409 File-util-normalise-path: don't throw
REVERT: fc2d511 Improve path normalization logic
REVERT: a2ff638 Use boost instead of mkdir -p if available
REVERT: a7022f1 Improve file-util code style
REVERT: 82ace0f Add basic file utilities
REVERT: df36049 Add json->irep deserialization routine
REVERT: 938d739 Java checkcast: fix stack when check disabled
REVERT: dda9efb Add string-infix utility
REVERT: ca45a2b Add goto-program instruction iterator hasher
REVERT: 7428ee5 Merge pull request diffblue#583 from diffblue/master

git-subtree-dir: cbmc
git-subtree-split: 768e8a6

Author: smowton

.gitignore

@@ -65,7 +65,6 @@ libzip/
 zlib/
 minisat*/
 glucose-syrup/
-boost-include/
 
 # flex/bison generated files
 src/ansi-c/ansi_c_lex.yy.cpp

.travis.yml

@@ -267,9 +267,8 @@ install:
   - ccache -z
   - ccache --max-size=1G
   - make -C src minisat2-download
-  - make -C src boost-download
   - make -C src/ansi-c library_check
-  - make -C src "CXX=${COMPILER} -DUSE_BOOST ${EXTRA_CXXFLAGS}" -j3
+  - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
   - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 clobber.dir memory-models.dir
 
 script:

CMakeLists.txt

@@ -1,13 +1,10 @@
 cmake_minimum_required(VERSION 3.2)
 
-set(enable_ccache on CACHE BOOL "Whether CCACHE should be used or not when building targets (applies only for Makefile and Ninja generators).")
 find_program(CCACHE_PROGRAM ccache)
-if(CCACHE_PROGRAM AND enable_ccache)
+if(CCACHE_PROGRAM)
     set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "${CCACHE_PROGRAM}")
     message(STATUS "Rule launch compile: ${CCACHE_PROGRAM}")
-else()
-    set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "")
-endif()
+ endif()
 
 set(CMAKE_EXPORT_COMPILE_COMMANDS true)
 

regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/readme.txt

@@ -1,2 +1,2 @@
 Source of benchmark:
-https://github.com/Diffblue-benchmarks/java-test
+https://github.com/DiffBlue-benchmarks/java-test