Commit 73db3ab
authored
Updated mir-semantics submodule (#142)
- Python tool updates
runtimeverification/mir-semantics#893 ,
runtimeverification/mir-semantics#892
- Function pointer support
runtimeverification/mir-semantics#894
- Stable-MIR-JSON update
runtimeverification/mir-semantics#896,
runtimeverification/mir-semantics#898
- [update spl/p-token.md to use
#execTerminatorCall](runtimeverification/mir-semantics@39ce2a6)
- Add --fail-fast and --maintainence-rate pyk flags (Add --fail-fast and
--maintainence-rate pyk flags #900)1 parent 9099e12 commit 73db3ab
1 file changed
+1
-1
lines changedSubmodule mir-semantics updated 50 files
- deps/pyproject-build-systems+1-1
- deps/stable-mir-json+1-1
- deps/stable-mir-json_release+1-1
- deps/uv2nix+1-1
- deps/uv_release+1-1
- flake.lock+18-18
- flake.nix+3-3
- kmir/src/kmir/__main__.py+16
- kmir/src/kmir/kdist/mir-semantics/kmir.md+25-17
- kmir/src/kmir/kdist/mir-semantics/rt/data.md+11
- kmir/src/kmir/kdist/mir-semantics/rt/value.md+2
- kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md+36-47
- kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md+30-43
- kmir/src/kmir/kmir.py+6-1
- kmir/src/kmir/options.py+10
- kmir/src/kmir/smir.py+32-9
- kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::a_module::twice.expected+1-1
- kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::main.expected+1-1
- kmir/src/tests/integration/data/crate-tests/single-dylib/small_test_dylib::add.expected+1-1
- kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected+3-3
- kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected+1-1
- kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected+1-1
- kmir/src/tests/integration/data/prove-rs/488-support-function-pointer-calls.rs+26
- kmir/src/tests/integration/data/prove-rs/show/assert-inhabited-fail.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-custom-printer.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-default-printer.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/niche-enum.smir.foo.cli-stats-leaves.expected+5-5
- kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected+4-4
- kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected+3-3
- kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected+2-2
- kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected+6-6
- kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-fail.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-fail.main.expected+1-1
- kmir/src/tests/integration/data/prove-rs/show/unions-fail.main.expected+1-1
- kmir/src/tests/integration/test_integration.py+5-5
- kmir/uv.lock+266-187
0 commit comments