Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Browse files
Browse the repository at this point in the history
54f3731 Merge pull request diffblue#2610 from smowton/smowton/fix/ssa-trace-unreachable-values 6397f62 Merge pull request diffblue#2626 from qaphla/local_bitvector_analysis_fix 0c0e288 Merge pull request diffblue#2423 from tautschnig/vs-negation e90b61b Transform float_utils unit test to use CATCH and enable it 8b2bd7b Convert to signed type to make negation meaningful 7823d9c Merge pull request diffblue#2606 from diffblue/ms_cl_options 0f60b26 Merge pull request diffblue#2627 from diffblue/cleanup-ansi-c-scanner f33459f Merge pull request diffblue#2529 from tautschnig/debian1 1927fb2 remove bitvector and bitvector_u rules 1e07546 Fixed secondary issues arising from local_bitvector_analysis fix. 131e525 Fixed a bug in local_bitvector_analysis wherein an expression's ID was used in place of the expression's type's ID. 501546a SSA trace: don't concretise steps that will subsequently be dropped 709b45f Merge pull request diffblue#2591 from allredj/log-suffix-in-testpl f3630f0 Merge pull request diffblue#2612 from svorenova/multidim_arrays_tg3821_util c010edb Merge pull request diffblue#2623 from diffblue/cbmc-empty-message d5adef5 Merge pull request diffblue#2624 from diffblue/va_arg_mode 3e3303d symbols for va_args need a mode 398dd39 cbmc: avoid an empty message during result reporting 8bca5cd Merge pull request diffblue#2585 from smowton/smowton/admin/java-clean-deref-tests a0e339d Disable broken string test d0cf433 Strengthen local_safe_pointers to handle common Java operations e7b1a8a Merge pull request diffblue#2616 from smowton/smowton/admin/ai-unit-test 738ecad Merge pull request diffblue#2621 from diffblue/amazon-linux-instructions 4156283 Add test for ait framework 08bd1a8 Merge pull request diffblue#2596 from martin-cs/feature/context-sensitive-ait-merge-1 c572866 Use can_cast_type instead of raw type id check a1ab7a6 Improve documentation for java array types 745670b instructions for Amazon Linux 299417b Merge pull request diffblue#2614 from chrisr-diffblue/is_zero_bitfield_support 0c8eff6 Merge pull request diffblue#2598 from mmuesly/feature_posix_memalign fad7735 Merge pull request diffblue#2613 from NathanJPhillips/cleanup/irep_ids-def-not-h e34fc57 Merge pull request diffblue#2600 from peterschrammel/doxygen-graphviz 54cc818 clang-format fixups 9986ea1 Make exprt::is_zero() support bitfields dbf4384 Merge pull request diffblue#2605 from NathanJPhillips/feature/cast-for-code_typet 7798aaa Updated comment for the fact that IDs are defined in def files now b72b968 Remove unused function e66f76f Add a check functions for (multi-dimensional) array types f4f4190 Added can_cast_type implementation for code_typet f6c34f2 Merge pull request diffblue#2603 from smowton/smowton/fix/stub-string-lengths 9c9c375 two further Visual Studio CL options 05bebb7 Merge pull request diffblue#2595 from thk123/doc/use-can-cast 9a75c65 Merge pull request diffblue#2597 from allredj/update-jbmc-gitignore c98688b Fix stub string lengths 819560f Merge pull request diffblue#2601 from owen-jones-diffblue/owen-jones-diffblue/update-codeowners-3 39323e0 Remove code owners from low-risk files 8f8052a Make directories match from root 1a36a21 Install graphviz for doxygen job on travis 3e0b2a5 Doxygen the comments describing the abstract domain interface. 4f8d445 Upgrade from a warning in the comments to a protected constructor. 2b9c880 Clang format the domain files. 028d8b6 Add a method to convert the domain to a predicate to the basic domain API. 918e947 Expand the comments describing the base domain interface. f60027b Move the interface of domains to it's own header file. 15aa61f Adding support for posix_memalign from the stdlib in c. ba01589 Add guidelines for using irepts in the code base 37fc4e6 Update jbmc gitignore ec79bdd Merge pull request diffblue#2385 from polgreen/aggressive_slicer_v2 78b7119 Merge pull request diffblue#2491 from diffblue/std_code_constructors a99c4ff Merge pull request diffblue#2497 from diffblue/simplify_byte_extract_fix 8c7dc17 make comment // not /* ea085d3 move aggressive slicer options into macro aa4848d Apply clang format to includes in goto_instrument_parse_options 4ac9199 Aggressive slicer 2954205 aggressive slicer regression tests de7e1af call graph helper functions 357358d remove mistake in grapht c7457fb Merge pull request diffblue#2543 from tautschnig/vs-unsigned-byte-swap 0e72433 Merge pull request diffblue#2516 from polgreen/cbmc_trace_options 2e90035 Merge pull request diffblue#2590 from peterschrammel/use-proper-irep-ids a354235 Merge pull request diffblue#2592 from NathanJPhillips/cleanup/fix-typo-in-comment 59b1a9e Fix a small typo in a comment that I happened to come across 282468c Print log suffix when running tests c98c9df Merge branch 'develop' into cbmc_trace_options 12e970b Use irep ids for #comments 569c854 Merge pull request diffblue#2489 from diffblue/fix-empty-indexset 993735b Merge pull request diffblue#2507 from mgudemann/bugfix/java/keep-typecasts-on-stack a63212e Add regression test for stack variables with typecasts 6f63050 Simplify stack element replacement loop 731c69e Keep expressions unchanged when adding temporary variables d10e44d Merge pull request diffblue#2586 from hannes-steffenhagen-diffblue/fix-json_unit_test 8d6bfdd Merge pull request diffblue#2575 from nmanthey/upstream-ls_parse 2d14b22 Merge pull request diffblue#2545 from tautschnig/vs-unnecessary ff0414e Merge pull request diffblue#2546 from tautschnig/vs-wmm-int ed48122 Make json parser unit tests independent of working directory 14dc11e Merge pull request diffblue#2495 from diffblue/aws-codebuild-windows-jbmc-tests cefdc21 Merge pull request diffblue#2579 from peterschrammel/clean-up-java-options 64a63a0 Merge pull request diffblue#2584 from diffblue/fp-constant-folding 44cfeb9 Clean up redundant specification of CBMC option 38fe61e Trim JBMC help text width to 80 chars 080fc91 Break overlong lines in help text ebae090 Deactivate smt1 option in JBMC 04fcc5b Check that string options are used with strings turned on 0520732 Use default options in JBMC e4cfb04 Remove built-in-assertions option from JBMC 0d924ce Remove error-label option from JBMC 35f69f0 Remove GOTO_CHECK options from JBMC 86d4fec Remove --refine-strings from tests 7ef8a0e Remove obsolete string-max-length option e5e5e9e remove unneeded NOLINT 9449ac7 Encapsulate constraints for equals d74672b Use const references in string_constraintt fdf14f5 Add invariants on the sign of string_constraintt bounds 16052f8 Move string_constraintt constructor to cpp f01c03c Fix string_constraintt bound values 8edc5ee C front-end: constant folding for floating-point f795ef9 Remove trailing newlines that trip up regex on Windows 53d24e5 the jbmc tests now work on Windows f9c5faf adjust_float_expressions can now take a rounding mode argument 6ccce5b Merge pull request diffblue#2521 from svorenova/array_element_type_util 201ba8c Merge pull request diffblue#2581 from romainbrenguier/refactor/to_code e4b8c44 Clean-up in gen_nondet_instruction_info bb7ea78 Merge pull request diffblue#2528 from tautschnig/dev-null f10badb Add functions to retrieve a reference to the java array element type 7f8b2be Merge pull request diffblue#2582 from jeannielynnmoulton/jeannie/parse-bridge-flag-for-thk123 1f62596 Clean-up get_return_lhs 8966f09 Merge pull request diffblue#2560 from tautschnig/force-inline cb587a9 Adding unit test for checking bridge methods attribute is parsed correctly efadba2 Read the bride flag for methods 26781a6 Remove unnecessary cast to_code a18b32d Merge pull request diffblue#2571 from jeannielynnmoulton/jeannie/InnerClassAccessibility c959c3f Tests get_outer_class with deeply nested classes. 8201c19 Parse and capture outer class for inner classes. 87c2a68 Merge pull request diffblue#2577 from owen-jones-diffblue/owen-jones-diffblue/make-linter-happier a1b9e07 Fix whitespace errors and a typo from diffblue#2505 45eae64 Merge pull request diffblue#2505 from owen-jones-diffblue/owen-jones-diffblue/fix/convert-nondet 6d9e805 Make convert_java_nondet more general 70887e2 Merge pull request diffblue#2564 from tautschnig/vs-java-parse-tree 6c5ecec Merge pull request diffblue#2570 from johnnonweiler/doc-git-submodule-update d5ea306 ls_parse: improve debugging by printing a trace 17bc726 ls_parse: Allow handling unknown blocks aad1692 Add minisat download to jbmc/README.md f7ddb02 Remove --recursive from git submodule update 206f7fb Include submodule update in jbmc/README.md d5f3c32 Fix a typo JMBC->JBMC b5075d7 Document git submodule update in COMPILING.md 9b9aecf Remove unused macro BUFSIZE 0146874 Make all unicode operations use native endianness 8d93087 Move unicode unit test to CATCH and enable it 680227e Explicit unsigned -> uint16_t casts to avoid conversion warnings ea9dc15 goto-gcc: run original compiler even when output is /dev/null 0a990ef Do not (unnecessarily) require preprocessing for fixed 32/64 bit regression tests 0c15fed Cleanup java_bytecode_parse_treet: all members are public, no virtual tables required 36d13f7 Support Visual Studio's __forceinline 5953f6a goto-instrument/wmm: explicit conversion of bool to 0/1 6dc6ea9 Avoid unncessary signed/unsigned conversion 081f743 use proper constructor for code_assertt 8e44191 use proper constructor for code_expressiont 47f5405 use proper constructor for side_effect_expr_function_callt bf02ec7 use proper constructor for code_declt 9fa0733 use proper constructor for codet dbbd568 mark various 'partial constructors' as deprecated, and introduce complete ones 180e066 add option to show code in CBMC trace 4fbc10d Add option to show function calls and returns in CBMC trace f532b4b allow unsigned long instead of unsigned in regression test for hex_trace 94cacc6 represent numerical values in CBMC trace in hex fc4aab3 avoid non-termination of simplify_exprt::simplify_byte_extract when given array_of git-subtree-dir: cbmc git-subtree-split: 54f3731
- Loading branch information
