diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index fffbf7b35..ef84e55f5 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -1624,20 +1624,36 @@ What can be supported without additional layout consideration is trivial casts b
requires lookupTy(TY_SOURCE) ==K lookupTy(TY_TARGET)
```
-Other `Transmute` casts that can be resolved are round-trip casts from type A to type B and then directly back from B to A.
-The first cast is reified as a `thunk`, the second one resolves it and eliminates the `thunk`:
+Transmuting a pointer to `usize` occurs in compiler-generated alignment checks.
+Since KMIR uses an abstract pointer model without real memory addresses, all pointers are
+properly aligned by construction. We return `Integer(0, 64, false)` as a maximally-aligned
+abstract address, which ensures the alignment check evaluates concretely (rather than remaining
+stuck as a `thunk`) and passes as expected.
```k
- rule #cast(
- thunk(#cast(DATA, castKindTransmute, TY_SRC_INNER, TY_DEST_INNER)),
- castKindTransmute,
- TY_SRC_OUTER,
- TY_DEST_OUTER
- ) => DATA
+ rule #cast(PtrLocal(_, _, _, _), castKindTransmute, _TY_SOURCE, TY_TARGET)
+ =>
+ Integer(0, 64, false)
...
-
- requires lookupTy(TY_SRC_INNER) ==K lookupTy(TY_DEST_OUTER) // cast is a round-trip
- andBool lookupTy(TY_DEST_INNER) ==K lookupTy(TY_SRC_OUTER) // and is well-formed (invariant)
+
+ requires lookupTy(TY_TARGET) ==K typeInfoPrimitiveType(primTypeUint(uintTyUsize))
+ [priority(45)]
+
+ rule #cast(Reference(_, _, _, _), castKindTransmute, _TY_SOURCE, TY_TARGET)
+ =>
+ Integer(0, 64, false)
+ ...
+
+ requires lookupTy(TY_TARGET) ==K typeInfoPrimitiveType(primTypeUint(uintTyUsize))
+ [priority(45)]
+
+ rule #cast(AllocRef(_, _, _), castKindTransmute, _TY_SOURCE, TY_TARGET)
+ =>
+ Integer(0, 64, false)
+ ...
+
+ requires lookupTy(TY_TARGET) ==K typeInfoPrimitiveType(primTypeUint(uintTyUsize))
+ [priority(45)]
```
Transmuting a value `T` into a single-field wrapper struct `G` (or vice versa) is sound when the struct
diff --git a/kmir/src/tests/integration/data/prove-rs/alignment-check.rs b/kmir/src/tests/integration/data/prove-rs/alignment-check.rs
new file mode 100644
index 000000000..0ef832c69
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/alignment-check.rs
@@ -0,0 +1,14 @@
+// Test for issue #638: alignment check in raw pointer dereference.
+// The compiler inserts an alignment check that transmutes a pointer to usize.
+// Verifies that the transmute cast evaluates concretely.
+
+struct Thing { payload: i16 }
+
+fn main() {
+ let a = [Thing { payload: 1 }, Thing { payload: 2 }, Thing { payload: 3 }];
+ let p = &a as *const Thing;
+ let p1 = unsafe { p.add(1) };
+
+ let two = unsafe { (*p1).payload };
+ assert!(two == 2);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/interior-mut3-fail.rs b/kmir/src/tests/integration/data/prove-rs/interior-mut3.rs
similarity index 100%
rename from kmir/src/tests/integration/data/prove-rs/interior-mut3-fail.rs
rename to kmir/src/tests/integration/data/prove-rs/interior-mut3.rs
diff --git a/kmir/src/tests/integration/data/prove-rs/local-raw-fail.rs b/kmir/src/tests/integration/data/prove-rs/local-raw.rs
similarity index 100%
rename from kmir/src/tests/integration/data/prove-rs/local-raw-fail.rs
rename to kmir/src/tests/integration/data/prove-rs/local-raw.rs
diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper.rs
similarity index 100%
rename from kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper-fail.rs
rename to kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper.rs
diff --git a/kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs b/kmir/src/tests/integration/data/prove-rs/raw-ptr-cast.rs
similarity index 69%
rename from kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs
rename to kmir/src/tests/integration/data/prove-rs/raw-ptr-cast.rs
index cf098c9c3..bf425e202 100644
--- a/kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs
+++ b/kmir/src/tests/integration/data/prove-rs/raw-ptr-cast.rs
@@ -5,6 +5,6 @@ fn main() {
let ptr_mut = &mut data as *mut i32;
unsafe {
(*ptr_mut) = 44;
- assert_eq!(44, *ptr); // FIXME: fails due to thunks on casts
+ assert_eq!(44, *ptr);
}
}
diff --git a/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset-fail.rs b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset.rs
similarity index 100%
rename from kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset-fail.rs
rename to kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset.rs
diff --git a/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-fail.rs b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem.rs
similarity index 100%
rename from kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-fail.rs
rename to kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem.rs
diff --git a/kmir/src/tests/integration/data/prove-rs/show/alignment-check.main.expected b/kmir/src/tests/integration/data/prove-rs/show/alignment-check.main.expected
new file mode 100644
index 000000000..025268690
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/alignment-check.main.expected
@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│ span: 0
+│
+│ (239 steps)
+├─ 3 (terminal)
+│ #EndProgram ~> .K
+│ function: main
+│
+┊ constraint: true
+┊ subst: ...
+└─ 2 (leaf, target, terminal)
+ #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected
deleted file mode 100644
index 32338a571..000000000
--- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected
+++ /dev/null
@@ -1,63 +0,0 @@
-
-┌─ 1 (root, init)
-│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
-│ span: 0
-│
-│ (154 steps)
-├─ 3
-│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
-│ function: main
-┃
-┃ (1 step)
-┣━━┓
-┃ │
-┃ ├─ 4
-┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
-┃ │ function: main
-┃ │
-┃ │ (1 step)
-┃ └─ 6 (stuck, leaf)
-┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
-┃ function: main
-┃
-┗━━┓
- │
- ├─ 5
- │ #execBlockIdx ( basicBlockIdx ( 8 ) ) ~> .K
- │ function: main
- │
- │ (111 steps)
- ├─ 7
- │ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
- │ function: main
- ┃
- ┃ (1 step)
- ┣━━┓
- ┃ │
- ┃ ├─ 8
- ┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
- ┃ │ function: main
- ┃ │
- ┃ │ (1 step)
- ┃ └─ 10 (stuck, leaf)
- ┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
- ┃ function: main
- ┃
- ┗━━┓
- │
- ├─ 9
- │ #execBlockIdx ( basicBlockIdx ( 7 ) ) ~> .K
- │ function: main
- │
- │ (66 steps)
- ├─ 11 (terminal)
- │ #EndProgram ~> .K
- │ function: main
- │
- ┊ constraint: true
- ┊ subst: ...
- └─ 2 (leaf, target, terminal)
- #EndProgram ~> .K
-
-
-
diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3.main.expected
new file mode 100644
index 000000000..fcef878cd
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3.main.expected
@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│ span: 0
+│
+│ (333 steps)
+├─ 3 (terminal)
+│ #EndProgram ~> .K
+│ function: main
+│
+┊ constraint: true
+┊ subst: ...
+└─ 2 (leaf, target, terminal)
+ #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected
deleted file mode 100644
index a9a6646e9..000000000
--- a/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected
+++ /dev/null
@@ -1,40 +0,0 @@
-
-┌─ 1 (root, init)
-│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
-│ span: 0
-│
-│ (106 steps)
-├─ 3
-│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
-│ function: main
-┃
-┃ (1 step)
-┣━━┓
-┃ │
-┃ ├─ 4
-┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
-┃ │ function: main
-┃ │
-┃ │ (1 step)
-┃ └─ 6 (stuck, leaf)
-┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
-┃ function: main
-┃
-┗━━┓
- │
- ├─ 5
- │ #execBlockIdx ( basicBlockIdx ( 1 ) ) ~> .K
- │ function: main
- │
- │ (16 steps)
- ├─ 7 (terminal)
- │ #EndProgram ~> .K
- │ function: main
- │
- ┊ constraint: true
- ┊ subst: ...
- └─ 2 (leaf, target, terminal)
- #EndProgram ~> .K
-
-
-
diff --git a/kmir/src/tests/integration/data/prove-rs/show/local-raw.main.expected b/kmir/src/tests/integration/data/prove-rs/show/local-raw.main.expected
new file mode 100644
index 000000000..4e5e5fc22
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/local-raw.main.expected
@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│ span: 0
+│
+│ (123 steps)
+├─ 3 (terminal)
+│ #EndProgram ~> .K
+│ function: main
+│
+┊ constraint: true
+┊ subst: ...
+└─ 2 (leaf, target, terminal)
+ #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper-fail.main.expected
deleted file mode 100644
index 6c000e5b0..000000000
--- a/kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper-fail.main.expected
+++ /dev/null
@@ -1,109 +0,0 @@
-
-┌─ 1 (root, init)
-│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
-│ span: 0
-│
-│ (106 steps)
-├─ 3
-│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
-│ function: main
-┃
-┃ (1 step)
-┣━━┓
-┃ │
-┃ ├─ 4
-┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
-┃ │ function: main
-┃ │
-┃ │ (1 step)
-┃ └─ 6 (stuck, leaf)
-┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
-┃ function: main
-┃
-┗━━┓
- │
- ├─ 5
- │ #execBlockIdx ( basicBlockIdx ( 12 ) ) ~> .K
- │ function: main
- │
- │ (113 steps)
- ├─ 7
- │ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
- │ function: main
- ┃
- ┃ (1 step)
- ┣━━┓
- ┃ │
- ┃ ├─ 8
- ┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
- ┃ │ function: main
- ┃ │
- ┃ │ (1 step)
- ┃ └─ 10 (stuck, leaf)
- ┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
- ┃ function: main
- ┃
- ┗━━┓
- │
- ├─ 9
- │ #execBlockIdx ( basicBlockIdx ( 11 ) ) ~> .K
- │ function: main
- │
- │ (115 steps)
- ├─ 11
- │ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
- │ function: main
- ┃
- ┃ (1 step)
- ┣━━┓
- ┃ │
- ┃ ├─ 12
- ┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
- ┃ │ function: main
- ┃ │
- ┃ │ (1 step)
- ┃ └─ 14 (stuck, leaf)
- ┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
- ┃ function: main
- ┃
- ┗━━┓
- │
- ├─ 13
- │ #execBlockIdx ( basicBlockIdx ( 10 ) ) ~> .K
- │ function: main
- │
- │ (117 steps)
- ├─ 15
- │ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
- │ function: main
- ┃
- ┃ (1 step)
- ┣━━┓
- ┃ │
- ┃ ├─ 16
- ┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
- ┃ │ function: main
- ┃ │
- ┃ │ (1 step)
- ┃ └─ 18 (stuck, leaf)
- ┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
- ┃ function: main
- ┃
- ┗━━┓
- │
- ├─ 17
- │ #execBlockIdx ( basicBlockIdx ( 9 ) ) ~> .K
- │ function: main
- │
- │ (25 steps)
- ├─ 19 (terminal)
- │ #EndProgram ~> .K
- │ function: main
- │
- ┊ constraint: true
- ┊ subst: ...
- └─ 2 (leaf, target, terminal)
- #EndProgram ~> .K
-
-
-
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper.main.expected
new file mode 100644
index 000000000..bddd16205
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper.main.expected
@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│ span: 0
+│
+│ (480 steps)
+├─ 3 (terminal)
+│ #EndProgram ~> .K
+│ function: main
+│
+┊ constraint: true
+┊ subst: ...
+└─ 2 (leaf, target, terminal)
+ #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected
deleted file mode 100644
index 7be3f4dd4..000000000
--- a/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected
+++ /dev/null
@@ -1,40 +0,0 @@
-
-┌─ 1 (root, init)
-│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
-│ span: 0
-│
-│ (120 steps)
-├─ 3
-│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
-│ function: main
-┃
-┃ (1 step)
-┣━━┓
-┃ │
-┃ ├─ 4
-┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
-┃ │ function: main
-┃ │
-┃ │ (1 step)
-┃ └─ 6 (stuck, leaf)
-┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
-┃ function: main
-┃
-┗━━┓
- │
- ├─ 5
- │ #execBlockIdx ( basicBlockIdx ( 3 ) ) ~> .K
- │ function: main
- │
- │ (124 steps)
- ├─ 7 (terminal)
- │ #EndProgram ~> .K
- │ function: main
- │
- ┊ constraint: true
- ┊ subst: ...
- └─ 2 (leaf, target, terminal)
- #EndProgram ~> .K
-
-
-
diff --git a/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast.main.expected b/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast.main.expected
new file mode 100644
index 000000000..6e7cad49f
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast.main.expected
@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│ span: 0
+│
+│ (245 steps)
+├─ 3 (terminal)
+│ #EndProgram ~> .K
+│ function: main
+│
+┊ constraint: true
+┊ subst: ...
+└─ 2 (leaf, target, terminal)
+ #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-fail.main.expected
deleted file mode 100644
index e6f0eec24..000000000
--- a/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-fail.main.expected
+++ /dev/null
@@ -1,40 +0,0 @@
-
-┌─ 1 (root, init)
-│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
-│ span: 0
-│
-│ (124 steps)
-├─ 3
-│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
-│ function: main
-┃
-┃ (1 step)
-┣━━┓
-┃ │
-┃ ├─ 4
-┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
-┃ │ function: main
-┃ │
-┃ │ (1 step)
-┃ └─ 6 (stuck, leaf)
-┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
-┃ function: main
-┃
-┗━━┓
- │
- ├─ 5
- │ #execBlockIdx ( basicBlockIdx ( 3 ) ) ~> .K
- │ function: main
- │
- │ (26 steps)
- ├─ 7 (terminal)
- │ #EndProgram ~> .K
- │ function: main
- │
- ┊ constraint: true
- ┊ subst: ...
- └─ 2 (leaf, target, terminal)
- #EndProgram ~> .K
-
-
-
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset-fail.main.expected
deleted file mode 100644
index 2d1468486..000000000
--- a/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset-fail.main.expected
+++ /dev/null
@@ -1,40 +0,0 @@
-
-┌─ 1 (root, init)
-│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
-│ span: 0
-│
-│ (185 steps)
-├─ 3
-│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
-│ function: main
-┃
-┃ (1 step)
-┣━━┓
-┃ │
-┃ ├─ 4
-┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
-┃ │ function: main
-┃ │
-┃ │ (1 step)
-┃ └─ 6 (stuck, leaf)
-┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
-┃ function: main
-┃
-┗━━┓
- │
- ├─ 5
- │ #execBlockIdx ( basicBlockIdx ( 4 ) ) ~> .K
- │ function: main
- │
- │ (26 steps)
- ├─ 7 (terminal)
- │ #EndProgram ~> .K
- │ function: main
- │
- ┊ constraint: true
- ┊ subst: ...
- └─ 2 (leaf, target, terminal)
- #EndProgram ~> .K
-
-
-
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset.main.expected
new file mode 100644
index 000000000..6439f47cc
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset.main.expected
@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│ span: 0
+│
+│ (212 steps)
+├─ 3 (terminal)
+│ #EndProgram ~> .K
+│ function: main
+│
+┊ constraint: true
+┊ subst: ...
+└─ 2 (leaf, target, terminal)
+ #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem.main.expected
new file mode 100644
index 000000000..34537f1e5
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem.main.expected
@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│ span: 0
+│
+│ (151 steps)
+├─ 3 (terminal)
+│ #EndProgram ~> .K
+│ function: main
+│
+┊ constraint: true
+┊ subst: ...
+└─ 2 (leaf, target, terminal)
+ #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index a0486027b..3470f2551 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -42,9 +42,9 @@
'spl-multisig-iter-eq-copied-next': ['repro'],
}
PROVE_SHOW_SPECS = [
- 'local-raw-fail',
+ 'local-raw',
'interior-mut-fail',
- 'interior-mut3-fail',
+ 'interior-mut3',
'iter_next_3',
'assert_eq_exp',
'bitwise-not-shift',
@@ -55,19 +55,20 @@
'pointer-cast-length-test-fail',
'niche-enum',
'assume-cheatcode-conflict-fail',
- 'raw-ptr-cast-fail',
+ 'raw-ptr-cast',
'transmute-u8-to-enum-fail',
'assert-inhabited-fail',
'iterator-simple',
'unions-fail',
'transmute-maybe-uninit-fail',
- 'ptr-through-wrapper-fail',
+ 'ptr-through-wrapper',
'test_offset_from-fail',
- 'ref-ptr-cast-elem-fail',
- 'ref-ptr-cast-elem-offset-fail',
+ 'ref-ptr-cast-elem',
+ 'ref-ptr-cast-elem-offset',
'volatile_store_static-fail',
'volatile_load_static-fail',
'box_heap_alloc-fail',
+ 'alignment-check',
]