Skip to content

Commit

Permalink
Merge pull request #799 from diffblue/bump-cbmc-6.4.0
Browse files Browse the repository at this point in the history 
Bump CBMC to 6.4.0
  • Loading branch information
@kroening
kroening authored Nov 6, 2024
2 parents daa2204 + 7df121a commit bbe56b6
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion lib/cbmc
Submodule cbmc updated 39 files
+6 −6 .github/workflows/pull-request-checks.yaml
+24 −0 CHANGELOG
+6 −3 regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c
+6 −3 regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c
+1 −1 regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/main.c
+4 −3 regression/contracts-dfcc/invar_loop-entry_check/main.c
+4 −4 regression/contracts-dfcc/invar_loop-entry_check/test.desc
+1 −1 regression/contracts-dfcc/invar_loop-entry_fail/main.c
+5 −5 regression/contracts-dfcc/loop_assigns_inference-01/test.desc
+1 −1 regression/contracts-dfcc/loop_assigns_inference-03/main.c
+22 −0 regression/contracts-dfcc/loop_assigns_inference-04/main.c
+14 −0 regression/contracts-dfcc/loop_assigns_inference-04/test.desc
+17 −0 regression/contracts-dfcc/loop_assigns_inference-05/main.c
+15 −0 regression/contracts-dfcc/loop_assigns_inference-05/test.desc
+22 −0 regression/contracts/loop_assigns_inference-04/main.c
+10 −0 regression/contracts/loop_assigns_inference-04/test.desc
+1 −1 src/config.inc
+47 −32 src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
+2 −0 src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h
+284 −11 src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
+21 −6 src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h
+2 −0 src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp
+61 −9 src/goto-instrument/loop_utils.cpp
+1 −1 src/libcprover-rust/Cargo.toml
+2 −0 src/solvers/flattening/boolbv.cpp
+5 −3 src/solvers/floatbv/float_bv.cpp
+4 −0 src/solvers/smt2/smt2_conv.cpp
+13 −0 src/solvers/smt2_incremental/convert_expr_to_smt.cpp
+16 −2 src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+30 −3 src/util/bitvector_expr.cpp
+44 −0 src/util/bitvector_expr.h
+6 −0 src/util/format_expr.cpp
+1 −0 src/util/irep_ids.def
+10 −9 src/util/lower_byte_operators.cpp
+4 −0 src/util/simplify_expr.cpp
+2 −0 src/util/simplify_expr_class.h
+12 −0 src/util/simplify_expr_int.cpp
+1 −0 unit/Makefile
+48 −0 unit/solvers/flattening/boolbv_update_bit.cpp

0 comments on commit bbe56b6

Please sign in to comment.