Siemens fix258 #271
Closed
Siemens fix258 #271
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
Signed-off-by: Lucas Cordeiro <[email protected]>
|
May I ask for some suitable squashing here as well, please? |
smowton
added a commit
to smowton/cbmc
that referenced
this pull request
Dec 12, 2017
…017_11_16 Merge latest cbmc-develop
NathanJPhillips
pushed a commit
to NathanJPhillips/cbmc
that referenced
this pull request
Jan 16, 2018
…017_11_16 Merge latest cbmc-develop
smowton
added a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
…017_11_16 Merge latest cbmc-develop
smowton
added a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
ca5aa95 Merge remote-tracking branch 'upstream/develop' into merge-develop-20171212 c545369 Merge pull request diffblue#1663 from smowton/smowton/fix/guarded_gotos a2e2f74 Merge pull request diffblue#1636 from svorenova/inner_classes_tg1190_part2 2b835c6 Ensure guarded_gotos is cleared after converting each function 2fd9300 Adding a unit test for specialisation of implicitly generic classes 9617a41 Moving a utility function to utility function file 90a8230 Adding specialisation for implicitly generic classes 98017ce Merge pull request diffblue#1662 from janmroczkowski/janmroczkowski/unified_difft-iterator-check-fix-more ec89991 Merge pull request diffblue#1572 from romainbrenguier/refactor/expr_cast_to_util 5cd0f2f Merge pull request diffblue#1659 from reuk/reuk/jmp_buf-sym e324de6 Merge pull request diffblue#1656 from tautschnig/double-preproc 479e6cf Extra fix for lcss needed 9a811d8 Change type of size to std::size_t 77b7d77 Change length argument type to size_t 898f965 Remove solvers/refinement/expr_cast.h 5683fb5 Use numeric_cast instead of other conversion fc294f8 Use numeric_cast instead of refinement/expr_cast 946b6e2 Extend numeric_cast for constant expressions 20b5366 Add validate and can_cast method to string_exprt cf187c8 Merge pull request diffblue#1654 from NlightNFotis/fotis/pb10_develop 18f9079 Type consistent string preprocessing for floating-point expressions a61ea38 Merge pull request diffblue#1655 from diffblue/bugfix/string-last-index-of#TG592 b5faf52 Fix the handling of recursive data types. cd60782 Fix for the constant arrays marked as nondet issue. 3ab853e Test comparing jbmc lastIndexOf with loop version 985684a Prevent overflow with argument of lastIndexOf 04766b2 Merge pull request diffblue#1658 from tautschnig/fix-appveyor ed5f719 Move of alias code from VSA to LVSA. a44becc Requests in the PR (structure of comments). ef51720 Updates requested in the PR (added comments). 377a515 Introducing function 'get_may_alias_values'. bf4d2c5 Include setjmp.h if the jmp_buf symbol is used 65a3545 Overwrite files when unpacking unconditionally a3e19f7 Merge pull request diffblue#1644 from NathanJPhillips/feature/string-functions-on-demand 9b1ef1a Merge pull request diffblue#1645 from martin-cs/goto-analyzer-6-part3 1cc22f5 Merge pull request diffblue#1651 from thk123/bugfix/TG-1157/store-generic-info-in-specialized-class ea7646b Collect string solver function calls 0393027 Merge pull request diffblue#1639 from reuk/reuk/windows-fixes 3a46525 Renaming generic_tag to generic_name since not a tag 58f8482 Add the generic type arguments to the specalised type 7310281 Tidying of java_specialized_generic_class_typet 1667307 Merge pull request diffblue#1469 from antlechner/antonia/fix/ci_lazy_method_exception_types 6c3fb17 Update appveyor config 33d71aa Disable use of unistd in flex outputs adb7f55 Add Windows dependency information to the COMPILING file 6388940 Fix 'missing return statement' errors in miniBDD_new 23711d7 Print exported attribute in expr2c 0e71658 Initialise string solver function parameter names d556380 Make string solver functions get converted correctly first time ada4475 Replace map to pair with a more specialized type 0ac4d28 Don't store pointers to symbols in map 4b245f8 Use optionalt instead of safe_pointer c69b00d Rename things to better reflect true meaning 94a6ad4 Add test for NegativeArraySizeException 9cc3192 Rename test to NegativeArraySizeException1 51b1d38 Add test for ClassCastException 200017a Add test for ArrayIndexOutOfBoundsException 379e415 Add regression test for NullPointerException 41d77f4 Add regression test for ArithmeticException 4c472e9 Always load classes with throw_runtime_exceptions 2f7ee60 Store list of runtime exceptions in new variable da379bd Update and extend the regression tests for goto-analyse. db75611 Convert returned numbers to the appropriate symbolic exit codes and correct a few cases. 27304c0 Update the use of assert in unreachable_instructions. 1275983 Convert --unreachable-instructions, --unreachable-functions and --reachable-functions from specific to general tasks. e936c50 Convert --intervals and --non-null from being specific to general analysis. f79b73e Refactor doit() in goto analyzer to catch exceptions thrown during analysis. 9e02d7f Add a new set of options that allow task, abstract interpreter and domain to be picked independently. 71d2053 Refactor the command line handling of specific analyses. 396adaf Fix include statements in java_bytecode_instrument c99c2e4 Merge pull request diffblue#1650 from owen-jones-diffblue/owen-jones-diffblue/remove-unneeded-code a708711 Merge pull request diffblue#1648 from janmroczkowski/janmroczkowski/unified_difft-iterator-check-fix 7176f49 Remove unneeded code ae368b8 Fix to unified_difft::lcss for it not to error on iterator check 7660a98 Merge pull request diffblue#1627 from romainbrenguier/bugfix/string-last-index-of#TG-592 9749321 Merge pull request diffblue#1588 from polgreen/freezing_fix aa0e2e3 fix iterator in freeze_lazy_contraints ab9e585 Merge pull request diffblue#1218 from reuk/reuk/master-static-init-order 038ed78 Merge pull request diffblue#1625 from karkhaz/kk-symext-is-messaget b9372f1 Merge pull request diffblue#1516 from andreast271/mingw-D__int64-workaround 0f32076 Make string_container static init more resilient 9ebdc88 Test for String.lastIndexOf with empty argument 707ed94 Refactoring in axioms for lastIndexOf(char) e1f30e1 Fix bounds in axioms for lastIndexOf(char) 9437fa0 Fix special case of empty string in (last)IndexOf 6c6f873 Make goto_symext a subtype of messaget 9940370 Merge pull request diffblue#1633 from diffblue/enhancement/load_important_library_classes f8ca7e2 Remove quotes inside preprocessor defines to avoid problems with shell quote. c0de6fb Merge pull request diffblue#273 from diffblue/smowton/fix/end_to_end_tests 49fc50e Merge pull request diffblue#1586 from polgreen/get_source_location_for_property 14f6721 Merge pull request diffblue#1629 from owen-jones-diffblue/owen-jones-diffblue/refactor-vsa-objectt 92bec6c Add force loading parameter `--java-load-class` cd86eb8 Merge pull request diffblue#1477 from andreast271/travis-NDEBUG-build c543892 Replace objectt in value_set_fivrns.* cc8495a Replace objectt in value_set_fivr.* 5ecee62 Replace objectt in value_set_fi.* 1a51d67 Replace objectt with optional<mp_integer> 821403d Merge pull request diffblue#1640 from owen-jones-diffblue/owen-jones-diffblue/replace-unsigned-with-number-type 2200ac9 Replace unsigned with more precise type dd7ebd3 Merge pull request diffblue#1626 from tautschnig/fix-same_set 2935028 Merge pull request diffblue#1635 from reuk/patch-2 1019be2 Update Windows dependencies in Compiling.md db8f52d Fix copy&paste error in same_set 51cef3c Fix escape analysis 5c65731 Merge pull request diffblue#1612 from reuk/reuk/more-iterator-fixes 48ee475 Merge pull request diffblue#1616 from svorenova/inner_classes_tg1190_part1 37e5b80 Add `override` in a few places 0163362 Adding a unit test for implicitly generic classes ba05f18 Introducing a new type for implicitly generic classes 263fef4 Merge pull request diffblue#1628 from owen-jones-diffblue/owen-jones-diffblue/doc/fix-typos-in-vsa-docs 82b25c4 Fix a few typos in function comments d423c65 Mark tests which fail due to invariant violations 21439f4 Merge pull request diffblue#1614 from polgreen/cegis_cbmc 91ef19e Merge pull request diffblue#1593 from diffblue/chrisr-diffblue/parallel-regression-tests dfeccfd Merge pull request diffblue#1617 from NlightNFotis/fotis/pretty_print_bugfix ff1cf5d Run regression test directories in parallel during CI 24b3f75 Merge pull request diffblue#1618 from romainbrenguier/bugfix/string-equals#TG1619 8a9aa0f Move the pretty printing function from generate_java_generic_type to java_utils. 0dd029d Prevent use of CharSequence as a class_identifier f4c9719 Test for String.equals with class identifier check 17d230f Fix String.equals to check for class identifier 02e7b4a Merge pull request diffblue#1499 from smowton/smowton/feature/vsa_take_two 6ebceca Document value_sett 8bcca68 Add unit tests for value-set-analysis customisation 34dc4a9 Enable value-set to handle DEAD statements 8fb6da2 Templatize and virtualize value-set analysis 991d2b7 Fix goto program hash function ef929ea Fix iterator equality check bug in constant_propagator.cpp 47933cb Fix heap use-after-free in string_refinement.cpp 194ac7c Fix null dereference bug in cpp_typecheck_compound_type.cpp c44ed8c Avoid dereferencing past-the-end iterator in cover.cpp 18656b2 Fix iterator equality check bug in graphml_witness.cpp 60ef5aa Fix use-after-free in c_typecheck_initializer.cpp 82d42e5 Fix expr iterator mutation bug 8de0ea3 Fix iterator equality check bug in ai.h 6297085 Fix iterator comparison bug in expr_iterator af314f5 Fix iterator equality check bug in custom_bitvector_analysis.cpp e0605b7 Fix iterator equality check bug in dependence_graph.cpp 394c42d Fix iterator comparison bug in reaching_definitions.cpp 386a3bc Merge pull request diffblue#1621 from tautschnig/fix-1620 54f987b Use stable data structure for BV refinement approximations 0a0fa08 Fixed the pretty printing type function and fix the tests failing, and introduce test for the pretty printing function. 653dcb6 Fix taint instrumenter handling array initalisers 79defb5 Merge pull request diffblue#1605 from romainbrenguier/bugfix/failed-tests-printer-removed 134c77d Find source location from a property irep_idt 8a389f9 Hook for cegis to freeze program variables 8b1f65e Added range-based symex operations 1a33c87 refactoring bmc.cpp a6af95d Use -p option of test.pl instead of printer script 1821b1a Merge pull request diffblue#1615 from romainbrenguier/bugfix/string-allocation#TG1619 008b8d5 Merge pull request diffblue#1611 from mgudemann/enhancement/make_available_erase_type_arguments_gather_full_class_name dc769f1 Merge pull request diffblue#1583 from polgreen/debug_code_fix 550be1d Make two helper functions available 03c86a8 change #if0 to #ifdef DEBUG 7d37272 Fix the pretty printing routine to pp types that have java:: as their prefix only ea0c70a Remove redundant pointer to array association 89c123e Adapt unit test for allocation of string data 2e760b3 Add invariant on array to pointer association 2a22a2e Fix allocation of infinite char arrays 1957426 Merge pull request diffblue#1607 from mgudemann/fix/add_missing_class_file_awrapper f8e38fb Add edge type parameter to ai transform method a1bc2a2 Merge pull request diffblue#1606 from NlightNFotis/fotis_tg1157/pretty_printing 9091faa Use stdlib debug mode in Travis cbb2eff Changes in the generics concretisation tests to correspond to the new class signatures. f390795 Add a class to represent specialised generic classes, and change concretisation functions to use that. edc75fa Merge pull request diffblue#1604 from romainbrenguier/bugfix/string-nondet-init#TG1581 3d16d36 Merge pull request diffblue#1608 from smowton/smowton/fix/msvc14_headers 9829a58 Add headers needed to build under MSVC14 / Visual Studio 2015 558cb7a Add AWrapper.class which was missing from regression test 523f60e Change template of value_set_analysis_baset ac2a599 Correct unit test for gen_nondet_string 10d3857 Add test for instanceof String 12ca989 Document class_identifier argument of root class 5524078 Correct class_id of nondet strings efae909 Merge pull request diffblue#1603 from romainbrenguier/feature/cproverValidate#TG1313 4fd14b2 Adapt cproverNondetInitialize call for static case 4f45985 Merge pull request diffblue#271 from diffblue/smowton/merge_develop_2017_11_16 6d2d6c4 Test for cproverNondetInitialize with lazy-methods bf9a8c2 Load cproverNondetInitialize with lazy-methods 54d943d Test for the cproverNondetInitialize feature a1acecb Add call to cproverNondetInitialize in nondet-init aa88e27 Merge pull request diffblue#1590 from reuk/reuk/numbering-api-update bff25c5 Object numbering: Remove duplication e3e5e48 Object numbering: Remove function call operator c4b3335 Object numbering: Add trailing underscores for data members ad17a85 Object numbering: Switch typedef to using 7619d15 Rename ID_lvsa_mode to ID_lvsa_evs_type da6fa5d Don't mutate parameters in numbering class 161787b Merge pull request diffblue#1597 from diffblue/bugfix/add_generic_type_args_to_dependencies e707be3 Merge pull request diffblue#1591 from diffblue/print_assignment 645f631 Merge pull request diffblue#1600 from diffblue/chrisr-diffblue/ccache-fixups 62b52ba Merge pull request diffblue#1598 from peterschrammel/simplify-string-const-equalities a656e7b Remove obsolete equal/notequal cases in simplify_expr c7d8ea6 Tests for simplifying ID_string equalities ddf6c92 Simplify equalities of constants 81cc65f Merge pull request diffblue#1599 from NathanJPhillips/move-show-symbol-table-from-module-pass e8f5e08 Add regression tests for generic type arg dependencies fae14fc Add type parameters in signatures as dependencies fb493da Fixups for ccache configuration in travis 1a7dfdf Fix location of show-symbol-table 471180d Adapt to upstream CBMC changes 0da026b Merge pull request diffblue#1596 from NlightNFotis/bugfix/TG-1422/remove_evaluator_precondition c93dd78 Remove too tight precondition in evaluator that was causing an invariant violation in some cases. 5a0dcc7 boolbvt::print_assignment should call the print_assignment of the base class 10131ed make debug code compile in value_set.cpp 2177bbc Remove extra build with NDEBUG that compiles but doesn't test. Instead, add NDEBUG to a linux clang build that runs regression. 4fa3ba5 Create separate clang build with NDEBUG and CPROVER_INVARIANT_DO_NOT_CHECK Fix INVARIANT macros for CPROVER_INVARIANT_DO_NOT_CHECK and CPROVER_INVARIANT_ASSERT In NDEBUG build, disable known warnings caused by the disabled versions of the INVARIANT macros. git-subtree-dir: cbmc git-subtree-split: ca5aa95
smowton
added a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
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
chrisr-diffblue
added a commit
to chrisr-diffblue/cbmc
that referenced
this pull request
Aug 24, 2018
…ll-control-dependencies Unconditional control dependency fix
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.