Make two helper functions available #1611
Merged
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
mgudemann
requested review from
cesaro,
peterschrammel,
smowton and
thk123
as code owners
smowton
reviewed
Nov 22, 2017
mgudemann
force-pushed
the
enhancement/make_available_erase_type_arguments_gather_full_class_name
branch
from
05a088c to
4a5617b
Compare
|
@smowton making them accessible from the outside allows for using them in TG, the doxygen of the functions in |
mgudemann
force-pushed
the
enhancement/make_available_erase_type_arguments_gather_full_class_name
branch
3 times, most recently
from
64b5c8b to
77441c7
Compare
smowton
approved these changes
Nov 23, 2017
mgudemann
force-pushed
the
enhancement/make_available_erase_type_arguments_gather_full_class_name
branch
from
77441c7 to
550be1d
Compare
mgudemann
deleted the
enhancement/make_available_erase_type_arguments_gather_full_class_name
branch
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
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 functional change, required for TG-1606